### Nuprl Lemma : cat-square-commutes_wf

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

Proof

Definitions occuring in Statement :  cat-square-commutes: `x_y1 o y1_z = x_y2 o 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: `f a`
Definitions unfolded in proof :  cat-square-commutes: `x_y1 o y1_z = x_y2 o 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