### Nuprl Lemma : cat-isomorphic_inversion

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

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]` cat-isomorphism: `cat-isomorphism(C;x;y;f)` and: `P ∧ Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` cand: `A c∧ B`
Lemmas referenced :  cat-isomorphic_wf cat-ob_wf small-category_wf cat-inverse_wf cat-isomorphism_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin cut introduction extract_by_obid isectElimination hypothesisEquality hypothesis dependent_pairFormation independent_pairFormation productEquality

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

Date html generated: 2017_01_09-AM-09_11_32
Last ObjectModification: 2017_01_08-PM-01_18_53

Theory : small!categories

Home Index