Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax12inda2ALT Structured version   Visualization version   GIF version

Theorem ax12inda2ALT 36074
 Description: Alternate proof of ax12inda2 36075, slightly more direct and not requiring ax-c16 36020. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
ax12inda2.1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))))
Assertion
Ref Expression
ax12inda2ALT (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
Distinct variable group:   𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem ax12inda2ALT
StepHypRef Expression
1 ax-1 6 . . . . . . . 8 (∀𝑥𝜑 → (𝑥 = 𝑦 → ∀𝑥𝜑))
21axc4i-o 36026 . . . . . . 7 (∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑))
32a1i 11 . . . . . 6 (∀𝑧 𝑧 = 𝑥 → (∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑)))
4 biidd 264 . . . . . . 7 (∀𝑧 𝑧 = 𝑥 → (𝜑𝜑))
54dral1-o 36032 . . . . . 6 (∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 ↔ ∀𝑥𝜑))
65imbi2d 343 . . . . . . 7 (∀𝑧 𝑧 = 𝑥 → ((𝑥 = 𝑦 → ∀𝑧𝜑) ↔ (𝑥 = 𝑦 → ∀𝑥𝜑)))
76dral2-o 36058 . . . . . 6 (∀𝑧 𝑧 = 𝑥 → (∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑)))
83, 5, 73imtr4d 296 . . . . 5 (∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
98aecoms-o 36030 . . . 4 (∀𝑥 𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
109a1d 25 . . 3 (∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
1110a1d 25 . 2 (∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
12 simplr 767 . . . . 5 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ¬ ∀𝑥 𝑥 = 𝑦)
13 dveeq1-o 36063 . . . . . . . 8 (¬ ∀𝑧 𝑧 = 𝑥 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
1413naecoms-o 36055 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
1514imp 409 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦)
1615adantlr 713 . . . . 5 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦)
17 hbnae-o 36056 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
18 hba1-o 36025 . . . . . . 7 (∀𝑧 𝑥 = 𝑦 → ∀𝑧𝑧 𝑥 = 𝑦)
1917, 18hban 2302 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → ∀𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦))
20 ax-c5 36011 . . . . . . 7 (∀𝑧 𝑥 = 𝑦𝑥 = 𝑦)
21 ax12inda2.1 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))))
2221imp 409 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2320, 22sylan2 594 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2419, 23alimdh 1812 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧𝑥(𝑥 = 𝑦𝜑)))
2512, 16, 24syl2anc 586 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧𝑥(𝑥 = 𝑦𝜑)))
26 ax-11 2154 . . . . . 6 (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥𝑧(𝑥 = 𝑦𝜑))
27 hbnae-o 36056 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑧 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑧)
28 hbnae-o 36056 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑧)
2928, 14nf5dh 2145 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑥 = 𝑦)
30 19.21t 2199 . . . . . . . 8 (Ⅎ𝑧 𝑥 = 𝑦 → (∀𝑧(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑)))
3129, 30syl 17 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑧(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑)))
3227, 31albidh 1861 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑥𝑧(𝑥 = 𝑦𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3326, 32syl5ib 246 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3433ad2antrr 724 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3525, 34syld 47 . . 3 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3635exp31 422 . 2 (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
3711, 36pm2.61i 184 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1529  Ⅎwnf 1778 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-10 2139  ax-11 2154  ax-12 2170  ax-13 2384  ax-c5 36011  ax-c4 36012  ax-c7 36013  ax-c10 36014  ax-c11 36015  ax-c9 36018 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator