tyex Show Code edit
## One-Digit Inequality
thm (tyex ((A z)) () (E. z (= z A))
x (top A) z.tyex
(z.E. x (z.= x (top A)))
y (bottom A) z.tyex
(z.E. y (z.= y (bottom A)))
pm3.2i
(/\ (z.E. x (z.= x (top A))) (z.E. y (z.= y (bottom A))))
## <d 'Combine Existence Quantifiers '>
x (z.= x (top A)) y (z.= y (bottom A)) z.doubleex
(-> (/\ (z.E. x (z.= x (top A))) (z.E. y (z.= y (bottom A)))) (z.E. x (z.E. y (/\ (z.= x (top A)) (z.= y (bottom A))))))
ax-mp
(z.E. x (z.E. y (/\ (z.= x (top A)) (z.= y (bottom A)))))
## </d 'Combine Existence Quantifiers '>
x (top A) y (bottom A) fraczeq12
(-> (/\ (z.= x (top A)) (z.= y (bottom A))) (= (</> x y) (</> (top A) (bottom A))))
y z.19.22i
(-> (z.E. y (/\ (z.= x (top A)) (z.= y (bottom A)))) (z.E. y (= (</> x y) (</> (top A) (bottom A)))))
x z.19.22i
(-> (z.E. x (z.E. y (/\ (z.= x (top A)) (z.= y (bottom A))))) (z.E. x (z.E. y (= (</> x y) (</> (top A) (bottom A))))))
ax-mp
(z.E. x (z.E. y (= (</> x y) (</> (top A) (bottom A)))))
z (</> x y) eqeqq
(-> (z.= z (</> x y)) (= z (</> x y)))
z (</> x y) (</> (top A) (bottom A)) eqqeqq1
(-> (= z (</> x y)) (<-> (= z (</> (top A) (bottom A))) (= (</> x y) (</> (top A) (bottom A)))))
syl
(-> (z.= z (</> x y)) (<-> (= z (</> (top A) (bottom A))) (= (</> x y) (</> (top A) (bottom A)))))
z.ceqsex bicomi
(<-> (= (</> x y) (</> (top A) (bottom A))) (z.E. z (/\ (z.= z (</> x y)) (= z (</> (top A) (bottom A))))))
z (/\ (z.= z (</> x y)) (= z (</> (top A) (bottom A)))) zexex
(<-> (z.E. z (/\ (z.= z (</> x y)) (= z (</> (top A) (bottom A))))) (E. z (/\ (z.= z (</> x y)) (= z (</> (top A) (bottom A))))))
bitri
(<-> (= (</> x y) (</> (top A) (bottom A))) (E. z (/\ (z.= z (</> x y)) (= z (</> (top A) (bottom A))))))
## <d 'Remove Left Side of AND '>
(z.= z (</> x y)) (= z (</> (top A) (bottom A))) pm3.27
(-> (/\ (z.= z (</> x y)) (= z (</> (top A) (bottom A)))) (= z (</> (top A) (bottom A))))
ImpReplaceBi1Ex1
(-> (= (</> x y) (</> (top A) (bottom A))) (E. z (= z (</> (top A) (bottom A)))))
## </d 'Remove Left Side of AND '>
y z.19.22i
(-> (z.E. y (= (</> x y) (</> (top A) (bottom A)))) (z.E. y (E. z (= z (</> (top A) (bottom A))))))
x z.19.22i
(-> (z.E. x (z.E. y (= (</> x y) (</> (top A) (bottom A))))) (z.E. x (z.E. y (E. z (= z (</> (top A) (bottom A)))))))
ax-mp
(z.E. x (z.E. y (E. z (= z (</> (top A) (bottom A))))))
## <d 'Quantified Non-free Variable '>
x (z.E. y (E. z (= z (</> (top A) (bottom A))))) z.19.9
(<-> (z.E. x (z.E. y (E. z (= z (</> (top A) (bottom A)))))) (z.E. y (E. z (= z (</> (top A) (bottom A))))))
mpbi
(z.E. y (E. z (= z (</> (top A) (bottom A)))))
## </d 'Quantified Non-free Variable '>
## <d 'Quantified Non-free Variable '>
y (E. z (= z (</> (top A) (bottom A)))) z.19.9
(<-> (z.E. y (E. z (= z (</> (top A) (bottom A))))) (E. z (= z (</> (top A) (bottom A)))))
mpbi
(E. z (= z (</> (top A) (bottom A))))
## </d 'Quantified Non-free Variable '>
A fracExpand A (</> (top A) (bottom A)) eqcom mpbi
(= (</> (top A) (bottom A)) A)
z eqqeqq2i
(<-> (= z (</> (top A) (bottom A))) (= z A))
exbiii
(E. z (= z A))
)
edit