Nuprl Lemma : EquatePairs-equality
∀[x,y,n,m:Base].
(∀a,b:Base.
(a = b ∈ EquatePairs(x;n;y;m)
⇐⇒ ↓(a = b ∈ Base)
∨ (((x = a ∈ Base) ∧ (n = b ∈ Base)) ∨ ((x = b ∈ Base) ∧ (n = a ∈ Base)))
∨ (((y = a ∈ Base) ∧ (m = b ∈ Base)) ∨ ((y = b ∈ Base) ∧ (m = a ∈ Base)))
∨ ((x = y ∈ Base) ∧ (((n = a ∈ Base) ∧ (m = b ∈ Base)) ∨ ((n = b ∈ Base) ∧ (m = a ∈ Base)))))) supposing
((¬(n = m ∈ Base)) and
(¬(x = m ∈ Base)) and
(¬(y = n ∈ Base)))
Proof
Definitions occuring in Statement :
EquatePairs: EquatePairs(x;n;y;m),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
squash: ↓T,
or: P ∨ Q,
and: P ∧ Q,
base: Base,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
squash: ↓T,
prop: ℙ,
rev_implies: P ⇐ Q,
or: P ∨ Q,
EquatePairs: EquatePairs(x;n;y;m),
so_lambda: λ2x y.t[x; y],
subtype_rel: A ⊆r B
Lemmas referenced :
equal_wf,
not_wf,
base_wf,
or_wf,
squash_wf,
EquatePairs_wf,
equal-wf-base
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lambdaFormation,
independent_pairFormation,
hypothesis,
sqequalHypSubstitution,
imageElimination,
sqequalRule,
imageMemberEquality,
hypothesisEquality,
thin,
baseClosed,
lemma_by_obid,
isectElimination,
independent_isectElimination,
because_Cache,
productEquality,
lambdaEquality,
dependent_functionElimination,
productElimination,
independent_pairEquality,
axiomEquality,
isect_memberEquality,
equalityTransitivity,
equalitySymmetry,
pertypeElimination,
applyEquality,
pertypeMemberEquality
Latex:
\mforall{}[x,y,n,m:Base].
(\mforall{}a,b:Base.
(a = b
\mLeftarrow{}{}\mRightarrow{} \mdownarrow{}(a = b)
\mvee{} (((x = a) \mwedge{} (n = b)) \mvee{} ((x = b) \mwedge{} (n = a)))
\mvee{} (((y = a) \mwedge{} (m = b)) \mvee{} ((y = b) \mwedge{} (m = a)))
\mvee{} ((x = y) \mwedge{} (((n = a) \mwedge{} (m = b)) \mvee{} ((n = b) \mwedge{} (m = a)))))) supposing
((\mneg{}(n = m)) and
(\mneg{}(x = m)) and
(\mneg{}(y = n)))
Date html generated:
2016_05_15-PM-03_15_45
Last ObjectModification:
2016_01_16-AM-10_47_28
Theory : general
Home
Index