Nuprl Lemma : groupoid-square1_wf

[G:Groupoid]. ∀[x00,x10,x01,x11:cat-ob(cat(G))]. ∀[a:cat-arrow(cat(G)) x00 x10]. ∀[b:cat-arrow(cat(G)) x10 x11].
[c:cat-arrow(cat(G)) x00 x01].
  (groupoid-square1(G;x00;x10;x01;x11;a;b;c) ∈ {d:cat-arrow(cat(G)) x01 x11| d} )


Proof




Definitions occuring in Statement :  groupoid-square1: groupoid-square1(G;x00;x10;x01;x11;a;b;c) groupoid-cat: cat(G) groupoid: Groupoid cat-square-commutes: x_y1 y1_z x_y2 y2_z cat-arrow: cat-arrow(C) cat-ob: cat-ob(C) uall: [x:A]. B[x] member: t ∈ T set: {x:A| B[x]}  apply: a
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T groupoid-square1: groupoid-square1(G;x00;x10;x01;x11;a;b;c) prop: cat-square-commutes: x_y1 y1_z x_y2 y2_z true: True implies:  Q squash: T all: x:A. B[x] and: P ∧ Q uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) uimplies: supposing a
Lemmas referenced :  groupoid-right-cancellation cat-comp-ident groupoid_inv cat-comp-assoc true_wf squash_wf uiff_transitivity3 cat-id_wf equal_wf groupoid_wf cat-ob_wf cat-arrow_wf cat-square-commutes_wf groupoid-inv_wf groupoid-cat_wf cat-comp_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule dependent_set_memberEquality applyEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache natural_numberEquality independent_functionElimination lambdaEquality imageElimination universeEquality dependent_functionElimination productElimination imageMemberEquality baseClosed independent_isectElimination

Latex:
\mforall{}[G:Groupoid].  \mforall{}[x00,x10,x01,x11:cat-ob(cat(G))].  \mforall{}[a:cat-arrow(cat(G))  x00  x10].
\mforall{}[b:cat-arrow(cat(G))  x10  x11].  \mforall{}[c:cat-arrow(cat(G))  x00  x01].
    (groupoid-square1(G;x00;x10;x01;x11;a;b;c)  \mmember{}  \{d:cat-arrow(cat(G))  x01  x11|  a  o  b  =  c  o  d\}  )



Date html generated: 2016_05_18-AM-11_56_06
Last ObjectModification: 2016_01_17-PM-02_16_56

Theory : small!categories


Home Index