Nuprl Lemma : groupoid-inv_wf
∀[G:Groupoid]. ∀[x,y:cat-ob(cat(G))]. ∀[x_y:cat-arrow(cat(G)) x y]. (groupoid-inv(G;x;y;x_y) ∈ cat-arrow(cat(G)) y x)
Proof
Definitions occuring in Statement :
groupoid-inv: groupoid-inv(G;x;y;x_y),
groupoid-cat: cat(G),
groupoid: Groupoid,
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
uall: ∀[x:A]. B[x],
member: t ∈ T,
apply: f a
Definitions unfolded in proof :
pi2: snd(t),
pi1: fst(t),
groupoid-cat: cat(G),
groupoid: Groupoid,
groupoid-inv: groupoid-inv(G;x;y;x_y),
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,
isect_memberEquality,
isectElimination,
lemma_by_obid,
equalitySymmetry,
equalityTransitivity,
axiomEquality,
hypothesis,
hypothesisEquality,
rename,
setElimination,
applyEquality,
thin,
productElimination,
sqequalHypSubstitution,
sqequalRule,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[G:Groupoid]. \mforall{}[x,y:cat-ob(cat(G))]. \mforall{}[x$_{y}$:cat-arrow(cat(G)) x y].
(groupoid-inv(G;x;y;x$_{y}$) \mmember{} cat-arrow(cat(G)) y x)
Date html generated:
2020_05_20-AM-07_55_14
Last ObjectModification:
2015_12_28-PM-02_22_52
Theory : small!categories
Home
Index