Nuprl Lemma : cat-isomorphic_transitivity

`∀C:SmallCategory. ∀a,b,c:cat-ob(C).  (cat-isomorphic(C;a;b) `` cat-isomorphic(C;b;c) `` cat-isomorphic(C;a;c))`

Proof

Definitions occuring in Statement :  cat-isomorphic: `cat-isomorphic(C;x;y)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` all: `∀x:A. B[x]` implies: `P `` Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` cat-isomorphic: `cat-isomorphic(C;x;y)` exists: `∃x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ`
Lemmas referenced :  cat-comp_wf cat-comp-isomorphism cat-isomorphism_wf cat-isomorphic_wf cat-ob_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin dependent_pairFormation applyEquality cut introduction extract_by_obid isectElimination hypothesisEquality hypothesis dependent_functionElimination independent_functionElimination

Latex:
\mforall{}C:SmallCategory.  \mforall{}a,b,c:cat-ob(C).
(cat-isomorphic(C;a;b)  {}\mRightarrow{}  cat-isomorphic(C;b;c)  {}\mRightarrow{}  cat-isomorphic(C;a;c))

Date html generated: 2017_01_09-AM-09_11_33
Last ObjectModification: 2017_01_08-PM-01_40_04

Theory : small!categories

Home Index