Step * 1 2 of Lemma exists-type-equating-ints


1. : ℤ
2. : ℤ
3. : ℤ
4. : ℤ
5. ¬(x y ∈ ℤ)
6. ¬(n m ∈ ℤ)
7. ¬(x m ∈ ℤ)
8. ¬(y n ∈ ℤ)
⊢ m ∈ (⇃({z:ℤ(z x ∈ ℤ) ∨ (z n ∈ ℤ)} ) ⋃ ⇃({z:ℤ(z y ∈ ℤ) ∨ (z m ∈ ℤ)} ))
BY
((BUnionRight THENA Auto) THEN EqTypeCD THEN Auto) }


Latex:


Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  n  :  \mBbbZ{}
4.  m  :  \mBbbZ{}
5.  \mneg{}(x  =  y)
6.  \mneg{}(n  =  m)
7.  \mneg{}(x  =  m)
8.  \mneg{}(y  =  n)
\mvdash{}  y  =  m


By


Latex:
((BUnionRight  THENA  Auto)  THEN  EqTypeCD  THEN  Auto)




Home Index