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 36968
Description: Alternate proof of ax12inda2 36969, slightly more direct and not requiring ax-c16 36914. (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 36920 . . . . . . 7 (∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑))
32a1i 11 . . . . . 6 (∀𝑧 𝑧 = 𝑥 → (∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑)))
4 biidd 261 . . . . . . 7 (∀𝑧 𝑧 = 𝑥 → (𝜑𝜑))
54dral1-o 36926 . . . . . 6 (∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 ↔ ∀𝑥𝜑))
65imbi2d 341 . . . . . . 7 (∀𝑧 𝑧 = 𝑥 → ((𝑥 = 𝑦 → ∀𝑧𝜑) ↔ (𝑥 = 𝑦 → ∀𝑥𝜑)))
76dral2-o 36952 . . . . . 6 (∀𝑧 𝑧 = 𝑥 → (∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑)))
83, 5, 73imtr4d 294 . . . . 5 (∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
98aecoms-o 36924 . . . 4 (∀𝑥 𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
109a1d 25 . . 3 (∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
1110a1d 25 . 2 (∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
12 simplr 766 . . . . 5 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ¬ ∀𝑥 𝑥 = 𝑦)
13 dveeq1-o 36957 . . . . . . . 8 (¬ ∀𝑧 𝑧 = 𝑥 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
1413naecoms-o 36949 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
1514imp 407 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦)
1615adantlr 712 . . . . 5 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦)
17 hbnae-o 36950 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
18 hba1-o 36919 . . . . . . 7 (∀𝑧 𝑥 = 𝑦 → ∀𝑧𝑧 𝑥 = 𝑦)
1917, 18hban 2297 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → ∀𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦))
20 ax-c5 36905 . . . . . . 7 (∀𝑧 𝑥 = 𝑦𝑥 = 𝑦)
21 ax12inda2.1 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))))
2221imp 407 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2320, 22sylan2 593 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2419, 23alimdh 1820 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧𝑥(𝑥 = 𝑦𝜑)))
2512, 16, 24syl2anc 584 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧𝑥(𝑥 = 𝑦𝜑)))
26 ax-11 2154 . . . . . 6 (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥𝑧(𝑥 = 𝑦𝜑))
27 hbnae-o 36950 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑧 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑧)
28 hbnae-o 36950 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑧)
2928, 14nf5dh 2143 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑥 = 𝑦)
30 19.21t 2199 . . . . . . . 8 (Ⅎ𝑧 𝑥 = 𝑦 → (∀𝑧(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑)))
3129, 30syl 17 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑧(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑)))
3227, 31albidh 1869 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑥𝑧(𝑥 = 𝑦𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3326, 32syl5ib 243 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3433ad2antrr 723 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3525, 34syld 47 . . 3 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3635exp31 420 . 2 (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
3711, 36pm2.61i 182 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wal 1537  wnf 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2372  ax-c5 36905  ax-c4 36906  ax-c7 36907  ax-c10 36908  ax-c11 36909  ax-c9 36912
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator