---

Step * of Lemma exists-type-equating-ints

∀x,y,n,m:ℤ.
  ((¬(x = y ∈ ℤ))
  ⇒ (¬(n = m ∈ ℤ))
  ⇒ (¬(x = m ∈ ℤ))
  ⇒ (¬(y = n ∈ ℤ))
  ⇒ (∃T:Type. ((x = n ∈ T) ∧ (y = m ∈ T) ∧ (¬(x = y ∈ T)))))
BY
{ Auto }

1
1. x : ℤ
2. y : ℤ
3. n : ℤ
4. m : ℤ
5. ¬(x = y ∈ ℤ)
6. ¬(n = m ∈ ℤ)
7. ¬(x = m ∈ ℤ)
8. ¬(y = n ∈ ℤ)
⊢ ∃T:Type. ((x = n ∈ T) ∧ (y = m ∈ T) ∧ (¬(x = y ∈ T)))

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index