---

Step * 2 of Lemma type-with-x=0-y=1


1. x : Base
2. y : Base
3. EquivRel({z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} ;a,b.((x = y ∈ Base)
                                                                                ∨ (y = 0 ∈ Base)
                                                                                ∨ (x = 1 ∈ Base))
∨ (a = b ∈ Base)
∨ ((a = 0 ∈ Base) ∧ (b = x ∈ Base))
∨ ((a = x ∈ Base) ∧ (b = 0 ∈ Base))
∨ ((a = 1 ∈ Base) ∧ (b = y ∈ Base))
∨ ((a = y ∈ Base) ∧ (b = 1 ∈ Base)))
⊢ ∃T:Type. ((x = 0 ∈ T) ∧ (y = 1 ∈ T) ∧ ((0 = 1 ∈ T) ⇒ (↓(x = y ∈ Base) ∨ (x = 1 ∈ Base) ∨ (y = 0 ∈ Base))))
BY
{ (D 0 With ⌜a,b:{z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} //(((x = y ∈ Base)
                                                                                 ∨ (y = 0 ∈ Base)
                                                                                 ∨ (x = 1 ∈ Base))
   ∨ (a = b ∈ Base)
   ∨ ((a = 0 ∈ Base) ∧ (b = x ∈ Base))
   ∨ ((a = x ∈ Base) ∧ (b = 0 ∈ Base))
   ∨ ((a = 1 ∈ Base) ∧ (b = y ∈ Base))
   ∨ ((a = y ∈ Base) ∧ (b = 1 ∈ Base)))⌝ 
   THEN Auto
   THEN Try ((EqTypeCD THEN Auto))) }

1
1. x : Base
2. y : Base
3. EquivRel({z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} ;a,b.((x = y ∈ Base)
                                                                                ∨ (y = 0 ∈ Base)
                                                                                ∨ (x = 1 ∈ Base))
∨ (a = b ∈ Base)
∨ ((a = 0 ∈ Base) ∧ (b = x ∈ Base))
∨ ((a = x ∈ Base) ∧ (b = 0 ∈ Base))
∨ ((a = 1 ∈ Base) ∧ (b = y ∈ Base))
∨ ((a = y ∈ Base) ∧ (b = 1 ∈ Base)))
4. x
= 0
∈ (a,b:{z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} //(((x = y ∈ Base)
                                                                                ∨ (y = 0 ∈ Base)
                                                                                ∨ (x = 1 ∈ Base))
  ∨ (a = b ∈ Base)
  ∨ ((a = 0 ∈ Base) ∧ (b = x ∈ Base))
  ∨ ((a = x ∈ Base) ∧ (b = 0 ∈ Base))
  ∨ ((a = 1 ∈ Base) ∧ (b = y ∈ Base))
  ∨ ((a = y ∈ Base) ∧ (b = 1 ∈ Base))))
5. y
= 1
∈ (a,b:{z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} //(((x = y ∈ Base)
                                                                                ∨ (y = 0 ∈ Base)
                                                                                ∨ (x = 1 ∈ Base))
  ∨ (a = b ∈ Base)
  ∨ ((a = 0 ∈ Base) ∧ (b = x ∈ Base))
  ∨ ((a = x ∈ Base) ∧ (b = 0 ∈ Base))
  ∨ ((a = 1 ∈ Base) ∧ (b = y ∈ Base))
  ∨ ((a = y ∈ Base) ∧ (b = 1 ∈ Base))))
6. 0
= 1
∈ (a,b:{z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} //(((x = y ∈ Base)
                                                                                ∨ (y = 0 ∈ Base)
                                                                                ∨ (x = 1 ∈ Base))
  ∨ (a = b ∈ Base)
  ∨ ((a = 0 ∈ Base) ∧ (b = x ∈ Base))
  ∨ ((a = x ∈ Base) ∧ (b = 0 ∈ Base))
  ∨ ((a = 1 ∈ Base) ∧ (b = y ∈ Base))
  ∨ ((a = y ∈ Base) ∧ (b = 1 ∈ Base))))
⊢ ↓(x = y ∈ Base) ∨ (x = 1 ∈ Base) ∨ (y = 0 ∈ Base)

---

Latex:

---

Latex:

1.  x  :  Base
2.  y  :  Base
3.  EquivRel(\{z:Base|  (z  =  0)  \mvee{}  (z  =  1)  \mvee{}  (z  =  x)  \mvee{}  (z  =  y)\}  ;a,b.((x  =  y)  \mvee{}  (y  =  0)  \mvee{}  (x  =  1))
\mvee{}  (a  =  b)
\mvee{}  ((a  =  0)  \mwedge{}  (b  =  x))
\mvee{}  ((a  =  x)  \mwedge{}  (b  =  0))
\mvee{}  ((a  =  1)  \mwedge{}  (b  =  y))
\mvee{}  ((a  =  y)  \mwedge{}  (b  =  1)))
\mvdash{}  \mexists{}T:Type.  ((x  =  0)  \mwedge{}  (y  =  1)  \mwedge{}  ((0  =  1)  {}\mRightarrow{}  (\mdownarrow{}(x  =  y)  \mvee{}  (x  =  1)  \mvee{}  (y  =  0))))


By

---

Latex:
(D  0  With  \mkleeneopen{}a,b:\{z:Base|  (z  =  0)  \mvee{}  (z  =  1)  \mvee{}  (z  =  x)  \mvee{}  (z  =  y)\}  //(((x  =  y)  \mvee{}  (y  =  0)  \mvee{}  (x  =  1))
  \mvee{}  (a  =  b)
  \mvee{}  ((a  =  0)  \mwedge{}  (b  =  x))
  \mvee{}  ((a  =  x)  \mwedge{}  (b  =  0))
  \mvee{}  ((a  =  1)  \mwedge{}  (b  =  y))
  \mvee{}  ((a  =  y)  \mwedge{}  (b  =  1)))\mkleeneclose{} 
  THEN  Auto
  THEN  Try  ((EqTypeCD  THEN  Auto)))

---

Home Index