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:
2016_05_18-AM-11_54_25
Last ObjectModification:
2015_12_28-PM-02_22_52
Theory : small!categories
Home
Index