---

Step * of Lemma type-with-y=n

∀n,m:ℤ.  ((¬(n = m ∈ ℤ)) ⇒ (∀y:Base. ∃T:Type. ((y = n ∈ T) ∧ (m = m ∈ T) ∧ ((n = m ∈ T) ⇒ (y = m ∈ Base)))))
BY
{ (Auto
   THEN Assert ⌜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)))⌝⋅
   ) }

1
.....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)))

2
1. n : ℤ
2. m : ℤ
3. ¬(n = m ∈ ℤ)
4. y : Base
5. 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)))
⊢ ∃T:Type. ((y = n ∈ T) ∧ (m ∈ T) ∧ ((n = m ∈ T) ⇒ (y = m ∈ Base)))

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbZ{}.    ((\mneg{}(n  =  m))  {}\mRightarrow{}  (\mforall{}y:Base.  \mexists{}T:Type.  ((y  =  n)  \mwedge{}  (m  =  m)  \mwedge{}  ((n  =  m)  {}\mRightarrow{}  (y  =  m)))))


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}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)))\mkleeneclose{}\mcdot{}
  )

---

Home Index