---

Step * 1 of Lemma type-with-y=n

.....assertion..... 
1. n : ℤ
2. m : ℤ
3. ¬(n = m ∈ ℤ)
4. y : Base
⊢ EquivRel({z:Base| (z = n ∈ Base) ∨ (z = m ∈ Base) ∨ (z = y ∈ Base)} ;a,b.(y = m ∈ Base)
∨ (a = b ∈ Base)
∨ ((a = n ∈ Base) ∧ (b = y ∈ Base))
∨ ((a = y ∈ Base) ∧ (b = n ∈ Base)))
BY
{ (RepUR ``equiv_rel refl sym trans`` 0 THEN Auto) }

1
1. n : ℤ
2. m : ℤ
3. ¬(n = m ∈ ℤ)
4. y : Base
5. ∀a:{z:Base| (z = n ∈ Base) ∨ (z = m ∈ Base) ∨ (z = y ∈ Base)} 
     ((y = m ∈ Base) ∨ (a = a ∈ Base) ∨ ((a = n ∈ Base) ∧ (a = y ∈ Base)) ∨ ((a = y ∈ Base) ∧ (a = n ∈ Base)))
6. a : {z:Base| (z = n ∈ Base) ∨ (z = m ∈ Base) ∨ (z = y ∈ Base)} 
7. b : {z:Base| (z = n ∈ Base) ∨ (z = m ∈ Base) ∨ (z = y ∈ Base)} 
8. (y = m ∈ Base) ∨ (a = b ∈ Base) ∨ ((a = n ∈ Base) ∧ (b = y ∈ Base)) ∨ ((a = y ∈ Base) ∧ (b = n ∈ Base))
⊢ (y = m ∈ Base) ∨ (b = a ∈ Base) ∨ ((b = n ∈ Base) ∧ (a = y ∈ Base)) ∨ ((b = y ∈ Base) ∧ (a = n ∈ Base))

2
1. n : ℤ
2. m : ℤ
3. ¬(n = m ∈ ℤ)
4. y : Base
5. ∀a:{z:Base| (z = n ∈ Base) ∨ (z = m ∈ Base) ∨ (z = y ∈ Base)} 
     ((y = m ∈ Base) ∨ (a = a ∈ Base) ∨ ((a = n ∈ Base) ∧ (a = y ∈ Base)) ∨ ((a = y ∈ Base) ∧ (a = n ∈ Base)))
6. ∀a,b:{z:Base| (z = n ∈ Base) ∨ (z = m ∈ Base) ∨ (z = y ∈ Base)} .
     (((y = m ∈ Base) ∨ (a = b ∈ Base) ∨ ((a = n ∈ Base) ∧ (b = y ∈ Base)) ∨ ((a = y ∈ Base) ∧ (b = n ∈ Base)))
     ⇒ ((y = m ∈ Base) ∨ (b = a ∈ Base) ∨ ((b = n ∈ Base) ∧ (a = y ∈ Base)) ∨ ((b = y ∈ Base) ∧ (a = n ∈ Base))))
7. a : {z:Base| (z = n ∈ Base) ∨ (z = m ∈ Base) ∨ (z = y ∈ Base)} 
8. b : {z:Base| (z = n ∈ Base) ∨ (z = m ∈ Base) ∨ (z = y ∈ Base)} 
9. c : {z:Base| (z = n ∈ Base) ∨ (z = m ∈ Base) ∨ (z = y ∈ Base)} 
10. (y = m ∈ Base) ∨ (a = b ∈ Base) ∨ ((a = n ∈ Base) ∧ (b = y ∈ Base)) ∨ ((a = y ∈ Base) ∧ (b = n ∈ Base))
11. (y = m ∈ Base) ∨ (b = c ∈ Base) ∨ ((b = n ∈ Base) ∧ (c = y ∈ Base)) ∨ ((b = y ∈ Base) ∧ (c = n ∈ Base))
⊢ (y = m ∈ Base) ∨ (a = c ∈ Base) ∨ ((a = n ∈ Base) ∧ (c = y ∈ Base)) ∨ ((a = y ∈ Base) ∧ (c = n ∈ Base))

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  \mneg{}(n  =  m)
4.  y  :  Base
\mvdash{}  EquivRel(\{z:Base|  (z  =  n)  \mvee{}  (z  =  m)  \mvee{}  (z  =  y)\}  ;a,b.(y  =  m)
\mvee{}  (a  =  b)
\mvee{}  ((a  =  n)  \mwedge{}  (b  =  y))
\mvee{}  ((a  =  y)  \mwedge{}  (b  =  n)))


By

---

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

---

Home Index