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 34733
Description: Alternate proof of ax12inda2 34734, slightly more direct and not requiring ax-c16 34679. (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 34685 . . . . . . 7 (∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑))
32a1i 11 . . . . . 6 (∀𝑧 𝑧 = 𝑥 → (∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑)))
4 biidd 252 . . . . . . 7 (∀𝑧 𝑧 = 𝑥 → (𝜑𝜑))
54dral1-o 34691 . . . . . 6 (∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 ↔ ∀𝑥𝜑))
65imbi2d 329 . . . . . . 7 (∀𝑧 𝑧 = 𝑥 → ((𝑥 = 𝑦 → ∀𝑧𝜑) ↔ (𝑥 = 𝑦 → ∀𝑥𝜑)))
76dral2-o 34717 . . . . . 6 (∀𝑧 𝑧 = 𝑥 → (∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑)))
83, 5, 73imtr4d 283 . . . . 5 (∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
98aecoms-o 34689 . . . 4 (∀𝑥 𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
109a1d 25 . . 3 (∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
1110a1d 25 . 2 (∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
12 simplr 809 . . . . 5 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ¬ ∀𝑥 𝑥 = 𝑦)
13 dveeq1-o 34722 . . . . . . . 8 (¬ ∀𝑧 𝑧 = 𝑥 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
1413naecoms-o 34714 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
1514imp 444 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦)
1615adantlr 753 . . . . 5 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦)
17 hbnae-o 34715 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
18 hba1-o 34684 . . . . . . 7 (∀𝑧 𝑥 = 𝑦 → ∀𝑧𝑧 𝑥 = 𝑦)
1917, 18hban 2273 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → ∀𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦))
20 ax-c5 34670 . . . . . . 7 (∀𝑧 𝑥 = 𝑦𝑥 = 𝑦)
21 ax12inda2.1 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))))
2221imp 444 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2320, 22sylan2 492 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2419, 23alimdh 1892 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧𝑥(𝑥 = 𝑦𝜑)))
2512, 16, 24syl2anc 696 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧𝑥(𝑥 = 𝑦𝜑)))
26 ax-11 2181 . . . . . 6 (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥𝑧(𝑥 = 𝑦𝜑))
27 hbnae-o 34715 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑧 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑧)
28 hbnae-o 34715 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑧)
2928, 14nf5dh 2173 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑥 = 𝑦)
30 19.21t 2218 . . . . . . . 8 (Ⅎ𝑧 𝑥 = 𝑦 → (∀𝑧(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑)))
3129, 30syl 17 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑧(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑)))
3227, 31albidh 1940 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑥𝑧(𝑥 = 𝑦𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3326, 32syl5ib 234 . . . . 5 (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3433ad2antrr 764 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3525, 34syld 47 . . 3 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
3635exp31 631 . 2 (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
3711, 36pm2.61i 176 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  wal 1628  wnf 1855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-c5 34670  ax-c4 34671  ax-c7 34672  ax-c10 34673  ax-c11 34674  ax-c9 34677
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator