Nuprl Lemma : groupoid_inv

[G:Groupoid]
  ∀x,y:cat-ob(cat(G)). ∀f:cat-arrow(cat(G)) y.
    (((cat-comp(cat(G)) groupoid-inv(G;x;y;f)) (cat-id(cat(G)) x) ∈ (cat-arrow(cat(G)) x))
    ∧ ((cat-comp(cat(G)) groupoid-inv(G;x;y;f) f) (cat-id(cat(G)) y) ∈ (cat-arrow(cat(G)) y)))


Proof




Definitions occuring in Statement :  groupoid-inv: groupoid-inv(G;x;y;x_y) groupoid-cat: cat(G) groupoid: Groupoid cat-comp: cat-comp(C) cat-id: cat-id(C) cat-arrow: cat-arrow(C) cat-ob: cat-ob(C) uall: [x:A]. B[x] all: x:A. B[x] and: P ∧ Q apply: a equal: t ∈ T
Definitions unfolded in proof :  guard: {T} pi2: snd(t) groupoid-inv: groupoid-inv(G;x;y;x_y) pi1: fst(t) groupoid-cat: cat(G) groupoid: Groupoid cand: c∧ B and: P ∧ Q all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  groupoid_wf cat-ob_wf groupoid-cat_wf cat-arrow_wf
Rules used in proof :  because_Cache axiomEquality independent_pairEquality dependent_functionElimination lambdaEquality hypothesisEquality isectElimination lemma_by_obid applyEquality independent_pairFormation hypothesis sqequalRule rename setElimination thin productElimination sqequalHypSubstitution lambdaFormation cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[G:Groupoid]
    \mforall{}x,y:cat-ob(cat(G)).  \mforall{}f:cat-arrow(cat(G))  x  y.
        (((cat-comp(cat(G))  x  y  x  f  groupoid-inv(G;x;y;f))  =  (cat-id(cat(G))  x))
        \mwedge{}  ((cat-comp(cat(G))  y  x  y  groupoid-inv(G;x;y;f)  f)  =  (cat-id(cat(G))  y)))



Date html generated: 2020_05_20-AM-07_55_16
Last ObjectModification: 2015_12_28-PM-02_23_11

Theory : small!categories


Home Index