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

Theorem ax12inda2ALT 34834
Description: Alternate proof of ax12inda2 34835, slightly more direct and not requiring ax-c16 34780. (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 34786 . . . . . . 7 (∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑))
32a1i 11 . . . . . 6 (∀𝑧 𝑧 = 𝑥 → (∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑)))
4 biidd 253 . . . . . . 7 (∀𝑧 𝑧 = 𝑥 → (𝜑𝜑))
54dral1-o 34792 . . . . . 6 (∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 ↔ ∀𝑥𝜑))
65imbi2d 331 . . . . . . 7 (∀𝑧 𝑧 = 𝑥 → ((𝑥 = 𝑦 → ∀𝑧𝜑) ↔ (𝑥 = 𝑦 → ∀𝑥𝜑)))
76dral2-o 34818 . . . . . 6 (∀𝑧 𝑧 = 𝑥 → (∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑)))
83, 5, 73imtr4d 285 . . . . 5 (∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
98aecoms-o 34790 . . . 4 (∀𝑥 𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
109a1d 25 . . 3 (∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
1110a1d 25 . 2 (∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
12 simplr 785 . . . . 5 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ¬ ∀𝑥 𝑥 = 𝑦)
13 dveeq1-o 34823 . . . . . . . 8 (¬ ∀𝑧 𝑧 = 𝑥 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
1413naecoms-o 34815 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
1514imp 395 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦)
1615adantlr 706 . . . . 5 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦)
17 hbnae-o 34816 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
18 hba1-o 34785 . . . . . . 7 (∀𝑧 𝑥 = 𝑦 → ∀𝑧𝑧 𝑥 = 𝑦)
1917, 18hban 2305 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → ∀𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦))
20 ax-c5 34771 . . . . . . 7 (∀𝑧 𝑥 = 𝑦𝑥 = 𝑦)
21 ax12inda2.1 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))))
2221imp 395 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2320, 22sylan2 586 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2419, 23alimdh 1912 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧𝑥(𝑥 = 𝑦𝜑)))
2512, 16, 24syl2anc 579 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧𝑥(𝑥 = 𝑦𝜑)))
26 ax-11 2198 . . . . . 6 (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥𝑧(𝑥 = 𝑦𝜑))
27 hbnae-o 34816 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑧 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑧)
28 hbnae-o 34816 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑧)
2928, 14nf5dh 2189 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑥 = 𝑦)
30 19.21t 2238 . . . . . . . 8 (Ⅎ𝑧 𝑥 = 𝑦 → (∀𝑧(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑)))
3129, 30syl 17 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑧(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑)))
3227, 31albidh 1963 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑥𝑧(𝑥 = 𝑦𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3326, 32syl5ib 235 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3433ad2antrr 717 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3525, 34syld 47 . . 3 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3635exp31 410 . 2 (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
3711, 36pm2.61i 176 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wal 1650  wnf 1878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-c5 34771  ax-c4 34772  ax-c7 34773  ax-c10 34774  ax-c11 34775  ax-c9 34778
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator