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

Theorem ax12indalem 34833
Description: Lemma for ax12inda2 34835 and ax12inda 34836. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
ax12indalem.1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))))
Assertion
Ref Expression
ax12indalem (¬ ∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))

Proof of Theorem ax12indalem
StepHypRef Expression
1 ax-1 6 . . . . . . . . 9 (∀𝑥𝜑 → (𝑥 = 𝑦 → ∀𝑥𝜑))
21axc4i-o 34786 . . . . . . . 8 (∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑))
32a1i 11 . . . . . . 7 (∀𝑧 𝑧 = 𝑥 → (∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑)))
4 biidd 253 . . . . . . . 8 (∀𝑧 𝑧 = 𝑥 → (𝜑𝜑))
54dral1-o 34792 . . . . . . 7 (∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 ↔ ∀𝑥𝜑))
65imbi2d 331 . . . . . . . 8 (∀𝑧 𝑧 = 𝑥 → ((𝑥 = 𝑦 → ∀𝑧𝜑) ↔ (𝑥 = 𝑦 → ∀𝑥𝜑)))
76dral2-o 34818 . . . . . . 7 (∀𝑧 𝑧 = 𝑥 → (∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑)))
83, 5, 73imtr4d 285 . . . . . 6 (∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
98aecoms-o 34790 . . . . 5 (∀𝑥 𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
109a1d 25 . . . 4 (∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))
1110a1d 25 . . 3 (∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
1211adantr 472 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
13 simplr 785 . . . . 5 ((((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ¬ ∀𝑥 𝑥 = 𝑦)
14 aecom-o 34789 . . . . . . . . 9 (∀𝑧 𝑧 = 𝑥 → ∀𝑥 𝑥 = 𝑧)
1514con3i 151 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑧 → ¬ ∀𝑧 𝑧 = 𝑥)
16 aecom-o 34789 . . . . . . . . 9 (∀𝑧 𝑧 = 𝑦 → ∀𝑦 𝑦 = 𝑧)
1716con3i 151 . . . . . . . 8 (¬ ∀𝑦 𝑦 = 𝑧 → ¬ ∀𝑧 𝑧 = 𝑦)
18 axc9 2402 . . . . . . . . 9 (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
1918imp 395 . . . . . . . 8 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
2015, 17, 19syl2an 589 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))
2120imp 395 . . . . . 6 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦)
2221adantlr 706 . . . . 5 ((((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦)
23 hbnae-o 34816 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
24 hba1-o 34785 . . . . . . 7 (∀𝑧 𝑥 = 𝑦 → ∀𝑧𝑧 𝑥 = 𝑦)
2523, 24hban 2305 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → ∀𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦))
26 ax-c5 34771 . . . . . . 7 (∀𝑧 𝑥 = 𝑦𝑥 = 𝑦)
27 ax12indalem.1 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑))))
2827imp 395 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
2926, 28sylan2 586 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦𝜑)))
3025, 29alimdh 1912 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧𝑥(𝑥 = 𝑦𝜑)))
3113, 22, 30syl2anc 579 . . . 4 ((((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧𝑥(𝑥 = 𝑦𝜑)))
32 ax-11 2198 . . . . . 6 (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥𝑧(𝑥 = 𝑦𝜑))
33 hbnae-o 34816 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑧 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑧)
34 hbnae-o 34816 . . . . . . . 8 (¬ ∀𝑦 𝑦 = 𝑧 → ∀𝑥 ¬ ∀𝑦 𝑦 = 𝑧)
3533, 34hban 2305 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∀𝑥(¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧))
36 hbnae-o 34816 . . . . . . . . . 10 (¬ ∀𝑥 𝑥 = 𝑧 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑧)
37 hbnae-o 34816 . . . . . . . . . 10 (¬ ∀𝑦 𝑦 = 𝑧 → ∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧)
3836, 37hban 2305 . . . . . . . . 9 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∀𝑧(¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧))
3938, 20nf5dh 2189 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑧 𝑥 = 𝑦)
40 19.21t 2238 . . . . . . . 8 (Ⅎ𝑧 𝑥 = 𝑦 → (∀𝑧(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑)))
4139, 40syl 17 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑧(𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑)))
4235, 41albidh 1963 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑥𝑧(𝑥 = 𝑦𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
4332, 42syl5ib 235 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
4443ad2antrr 717 . . . 4 ((((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝑥(𝑥 = 𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
4531, 44syld 47 . . 3 ((((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))
4645exp31 410 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))))
4712, 46pm2.61ian 846 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:  ax12inda2  34835
  Copyright terms: Public domain W3C validator