---

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


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)))
BY
{ ((D 0 With ⌜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)))⌝ 
    THENA Auto
    )
   THEN SplitAndConcl
   THEN Try ((MemTypeCD THEN Auto))
   THEN Try ((D 0 THENA Auto))) }

1
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)))
6. n
= m
∈ (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

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  \mneg{}(n  =  m)
4.  y  :  Base
5.  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)))
\mvdash{}  \mexists{}T:Type.  ((y  =  n)  \mwedge{}  (m  \mmember{}  T)  \mwedge{}  ((n  =  m)  {}\mRightarrow{}  (y  =  m)))


By

---

Latex:
((D  0  With  \mkleeneopen{}a,b:\{z:Base|  (z  =  n)  \mvee{}  (z  =  m)  \mvee{}  (z  =  y)\}  //((y  =  m)
    \mvee{}  (a  =  b)
    \mvee{}  ((a  =  n)  \mwedge{}  (b  =  y))
    \mvee{}  ((a  =  y)  \mwedge{}  (b  =  n)))\mkleeneclose{} 
    THENA  Auto
    )
  THEN  SplitAndConcl
  THEN  Try  ((MemTypeCD  THEN  Auto))
  THEN  Try  ((D  0  THENA  Auto)))

---

Home Index