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: supposing a uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q not: ¬A squash: T or: P ∨ Q and: P ∧ Q base: Base equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q squash: T prop: rev_implies:  Q or: P ∨ Q EquatePairs: EquatePairs(x;n;y;m) so_lambda: λ2y.t[x; y]
Lemmas referenced :  equal-wf-base EquatePairs_wf squash_wf or_wf base_wf not_wf equal_wf and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation independent_pairFormation hypothesis sqequalHypSubstitution imageElimination sqequalRule imageMemberEquality hypothesisEquality thin baseClosed extract_by_obid isectElimination independent_isectElimination because_Cache productEquality lambdaEquality dependent_functionElimination productElimination independent_pairEquality axiomEquality isect_memberEquality equalityTransitivity equalitySymmetry pertypeElimination lemma_by_obid 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: 2018_05_21-PM-01_12_44
Last ObjectModification: 2018_05_01-PM-04_53_41

Theory : num_thy_1


Home Index