Nuprl Lemma : cat-square-commutes_wf

[C:SmallCategory]. ∀[x,y1,y2,z:cat-ob(C)]. ∀[x_y1:cat-arrow(C) y1]. ∀[y1_z:cat-arrow(C) y1 z]. ∀[x_y2:cat-arrow(C) 
                                                                                                         y2].
[y2_z:cat-arrow(C) y2 z].
  (x_y1 y1_z x_y2 y2_z ∈ ℙ)


Proof




Definitions occuring in Statement :  cat-square-commutes: x_y1 y1_z x_y2 y2_z cat-arrow: cat-arrow(C) cat-ob: cat-ob(C) small-category: SmallCategory uall: [x:A]. B[x] prop: member: t ∈ T apply: a
Definitions unfolded in proof :  cat-square-commutes: x_y1 y1_z x_y2 y2_z member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  small-category_wf cat-ob_wf cat-comp_wf cat-arrow_wf equal_wf
Rules used in proof :  because_Cache isect_memberEquality equalitySymmetry equalityTransitivity axiomEquality hypothesis hypothesisEquality applyEquality thin isectElimination sqequalHypSubstitution lemma_by_obid sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[x,y1,y2,z:cat-ob(C)].  \mforall{}[x$_{y1}$:cat-arrow(C)  x  y1].  \mforall{}[y1\mbackslash{}\000Cff24_{z}$:cat-arrow(C)  y1  z].
\mforall{}[x$_{y2}$:cat-arrow(C)  x  y2].  \mforall{}[y2$_{z}$:cat-arrow(C)  y2  z]\000C.
    (x$_{y1}$  o  y1$_{z}$  =  x$_{y2}$  o  y2\mbackslash{}f\000Cf24_{z}$  \mmember{}  \mBbbP{})



Date html generated: 2016_05_18-AM-11_54_12
Last ObjectModification: 2015_12_28-PM-02_23_09

Theory : small!categories


Home Index