NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax11indalem GIF version

Theorem ax11indalem 2197
Description: Lemma for ax11inda2 2199 and ax11inda 2200. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
ax11indalem.1 x x = y → (x = y → (φx(x = yφ))))
Assertion
Ref Expression
ax11indalem y y = z → (¬ x x = y → (x = y → (zφx(x = yzφ)))))

Proof of Theorem ax11indalem
StepHypRef Expression
1 ax-1 6 . . . . . . . . 9 (xφ → (x = yxφ))
21a5i-o 2150 . . . . . . . 8 (xφx(x = yxφ))
32a1i 10 . . . . . . 7 (z z = x → (xφx(x = yxφ)))
4 biidd 228 . . . . . . . 8 (z z = x → (φφ))
54dral1-o 2154 . . . . . . 7 (z z = x → (zφxφ))
65imbi2d 307 . . . . . . . 8 (z z = x → ((x = yzφ) ↔ (x = yxφ)))
76dral2-o 2181 . . . . . . 7 (z z = x → (x(x = yzφ) ↔ x(x = yxφ)))
83, 5, 73imtr4d 259 . . . . . 6 (z z = x → (zφx(x = yzφ)))
98aecoms-o 2152 . . . . 5 (x x = z → (zφx(x = yzφ)))
109a1d 22 . . . 4 (x x = z → (x = y → (zφx(x = yzφ))))
1110a1d 22 . . 3 (x x = z → (¬ x x = y → (x = y → (zφx(x = yzφ)))))
1211adantr 451 . 2 ((x x = z ¬ y y = z) → (¬ x x = y → (x = y → (zφx(x = yzφ)))))
13 simplr 731 . . . . 5 ((((¬ x x = z ¬ y y = z) ¬ x x = y) x = y) → ¬ x x = y)
14 aecom-o 2151 . . . . . . . . 9 (z z = xx x = z)
1514con3i 127 . . . . . . . 8 x x = z → ¬ z z = x)
16 aecom-o 2151 . . . . . . . . 9 (z z = yy y = z)
1716con3i 127 . . . . . . . 8 y y = z → ¬ z z = y)
18 ax12o 1934 . . . . . . . . 9 z z = x → (¬ z z = y → (x = yz x = y)))
1918imp 418 . . . . . . . 8 ((¬ z z = x ¬ z z = y) → (x = yz x = y))
2015, 17, 19syl2an 463 . . . . . . 7 ((¬ x x = z ¬ y y = z) → (x = yz x = y))
2120imp 418 . . . . . 6 (((¬ x x = z ¬ y y = z) x = y) → z x = y)
2221adantlr 695 . . . . 5 ((((¬ x x = z ¬ y y = z) ¬ x x = y) x = y) → z x = y)
23 hbnae-o 2179 . . . . . . 7 x x = yz ¬ x x = y)
24 hba1-o 2149 . . . . . . 7 (z x = yzz x = y)
2523, 24hban 1828 . . . . . 6 ((¬ x x = y z x = y) → zx x = y z x = y))
26 ax-4 2135 . . . . . . 7 (z x = yx = y)
27 ax11indalem.1 . . . . . . . 8 x x = y → (x = y → (φx(x = yφ))))
2827imp 418 . . . . . . 7 ((¬ x x = y x = y) → (φx(x = yφ)))
2926, 28sylan2 460 . . . . . 6 ((¬ x x = y z x = y) → (φx(x = yφ)))
3025, 29alimdh 1563 . . . . 5 ((¬ x x = y z x = y) → (zφzx(x = yφ)))
3113, 22, 30syl2anc 642 . . . 4 ((((¬ x x = z ¬ y y = z) ¬ x x = y) x = y) → (zφzx(x = yφ)))
32 ax-7 1734 . . . . . 6 (zx(x = yφ) → xz(x = yφ))
33 hbnae-o 2179 . . . . . . . 8 x x = zx ¬ x x = z)
34 hbnae-o 2179 . . . . . . . 8 y y = zx ¬ y y = z)
3533, 34hban 1828 . . . . . . 7 ((¬ x x = z ¬ y y = z) → xx x = z ¬ y y = z))
36 hbnae-o 2179 . . . . . . . . . 10 x x = zz ¬ x x = z)
37 hbnae-o 2179 . . . . . . . . . 10 y y = zz ¬ y y = z)
3836, 37hban 1828 . . . . . . . . 9 ((¬ x x = z ¬ y y = z) → zx x = z ¬ y y = z))
3938, 20nfdh 1767 . . . . . . . 8 ((¬ x x = z ¬ y y = z) → Ⅎz x = y)
40 19.21t 1795 . . . . . . . 8 (Ⅎz x = y → (z(x = yφ) ↔ (x = yzφ)))
4139, 40syl 15 . . . . . . 7 ((¬ x x = z ¬ y y = z) → (z(x = yφ) ↔ (x = yzφ)))
4235, 41albidh 1590 . . . . . 6 ((¬ x x = z ¬ y y = z) → (xz(x = yφ) ↔ x(x = yzφ)))
4332, 42syl5ib 210 . . . . 5 ((¬ x x = z ¬ y y = z) → (zx(x = yφ) → x(x = yzφ)))
4443ad2antrr 706 . . . 4 ((((¬ x x = z ¬ y y = z) ¬ x x = y) x = y) → (zx(x = yφ) → x(x = yzφ)))
4531, 44syld 40 . . 3 ((((¬ x x = z ¬ y y = z) ¬ x x = y) x = y) → (zφx(x = yzφ)))
4645exp31 587 . 2 ((¬ x x = z ¬ y y = z) → (¬ x x = y → (x = y → (zφx(x = yzφ)))))
4712, 46pm2.61ian 765 1 y y = z → (¬ x x = y → (x = y → (zφx(x = yzφ)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 176   wa 358  wal 1540  wnf 1544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-4 2135  ax-5o 2136  ax-6o 2137  ax-10o 2139  ax-12o 2142
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545
This theorem is referenced by:  ax11inda2  2199
  Copyright terms: Public domain W3C validator