### Nuprl Lemma : cat-id-isomorphism

`∀C:SmallCategory. ∀x:cat-ob(C).  cat-isomorphism(C;x;x;cat-id(C) x)`

Proof

Definitions occuring in Statement :  cat-isomorphism: `cat-isomorphism(C;x;y;f)` cat-id: `cat-id(C)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` all: `∀x:A. B[x]` apply: `f a`
Definitions unfolded in proof :  all: `∀x:A. B[x]` cat-isomorphism: `cat-isomorphism(C;x;y;f)` exists: `∃x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` and: `P ∧ Q` cand: `A c∧ B` cat-inverse: `fg=1` prop: `ℙ`
Lemmas referenced :  cat-id_wf cat-comp-ident cat-inverse_wf cat-ob_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation dependent_pairFormation applyEquality cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis dependent_functionElimination because_Cache productElimination independent_pairFormation productEquality

Latex:
\mforall{}C:SmallCategory.  \mforall{}x:cat-ob(C).    cat-isomorphism(C;x;x;cat-id(C)  x)

Date html generated: 2017_01_09-AM-09_11_17
Last ObjectModification: 2017_01_08-PM-01_15_23

Theory : small!categories

Home Index