---

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

.....assertion..... 
1. x : Base
2. y : Base
⊢ 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)))
BY
{ (RepUR ``equiv_rel refl sym trans`` 0 THEN Auto) }

1
1. x : Base
2. y : Base
3. ∀a:{z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} 
     (((x = y ∈ Base) ∨ (y = 0 ∈ Base) ∨ (x = 1 ∈ Base))
     ∨ (a = a ∈ Base)
     ∨ ((a = 0 ∈ Base) ∧ (a = x ∈ Base))
     ∨ ((a = x ∈ Base) ∧ (a = 0 ∈ Base))
     ∨ ((a = 1 ∈ Base) ∧ (a = y ∈ Base))
     ∨ ((a = y ∈ Base) ∧ (a = 1 ∈ Base)))
4. a : {z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} 
5. b : {z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} 
6. ((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) ∨ (y = 0 ∈ Base) ∨ (x = 1 ∈ Base))
∨ (b = a ∈ Base)
∨ ((b = 0 ∈ Base) ∧ (a = x ∈ Base))
∨ ((b = x ∈ Base) ∧ (a = 0 ∈ Base))
∨ ((b = 1 ∈ Base) ∧ (a = y ∈ Base))
∨ ((b = y ∈ Base) ∧ (a = 1 ∈ Base))

2
1. x : Base
2. y : Base
3. ∀a:{z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} 
     (((x = y ∈ Base) ∨ (y = 0 ∈ Base) ∨ (x = 1 ∈ Base))
     ∨ (a = a ∈ Base)
     ∨ ((a = 0 ∈ Base) ∧ (a = x ∈ Base))
     ∨ ((a = x ∈ Base) ∧ (a = 0 ∈ Base))
     ∨ ((a = 1 ∈ Base) ∧ (a = y ∈ Base))
     ∨ ((a = y ∈ Base) ∧ (a = 1 ∈ Base)))
4. ∀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) ∨ (y = 0 ∈ Base) ∨ (x = 1 ∈ Base))
        ∨ (b = a ∈ Base)
        ∨ ((b = 0 ∈ Base) ∧ (a = x ∈ Base))
        ∨ ((b = x ∈ Base) ∧ (a = 0 ∈ Base))
        ∨ ((b = 1 ∈ Base) ∧ (a = y ∈ Base))
        ∨ ((b = y ∈ Base) ∧ (a = 1 ∈ Base))))
5. a : {z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} 
6. b : {z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} 
7. c : {z:Base| (z = 0 ∈ Base) ∨ (z = 1 ∈ Base) ∨ (z = x ∈ Base) ∨ (z = y ∈ Base)} 
8. ((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))
9. ((x = y ∈ Base) ∨ (y = 0 ∈ Base) ∨ (x = 1 ∈ Base))
∨ (b = c ∈ Base)
∨ ((b = 0 ∈ Base) ∧ (c = x ∈ Base))
∨ ((b = x ∈ Base) ∧ (c = 0 ∈ Base))
∨ ((b = 1 ∈ Base) ∧ (c = y ∈ Base))
∨ ((b = y ∈ Base) ∧ (c = 1 ∈ Base))
⊢ ((x = y ∈ Base) ∨ (y = 0 ∈ Base) ∨ (x = 1 ∈ Base))
∨ (a = c ∈ Base)
∨ ((a = 0 ∈ Base) ∧ (c = x ∈ Base))
∨ ((a = x ∈ Base) ∧ (c = 0 ∈ Base))
∨ ((a = 1 ∈ Base) ∧ (c = y ∈ Base))
∨ ((a = y ∈ Base) ∧ (c = 1 ∈ Base))

---

Latex:

---

Latex:
.....assertion..... 
1.  x  :  Base
2.  y  :  Base
\mvdash{}  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)))


By

---

Latex:
(RepUR  ``equiv\_rel  refl  sym  trans``  0  THEN  Auto)

---

Home Index