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

Theorem ax12el 34046
 Description: Basis step for constructing a substitution instance of ax-c15 33993 without using ax-c15 33993. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ax12el (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))

Proof of Theorem ax12el
Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 19.26 1796 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2 elequ1 1995 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥𝑥𝑦𝑥))
3 elequ2 2002 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑦𝑥𝑦𝑦))
42, 3bitrd 268 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝑥𝑦𝑦))
54adantl 482 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝑥𝑥𝑦𝑦))
6 ax-5 1837 . . . . . . . . . 10 (𝑣𝑣 → ∀𝑥 𝑣𝑣)
7 ax-5 1837 . . . . . . . . . 10 (𝑦𝑦 → ∀𝑣 𝑦𝑦)
8 elequ1 1995 . . . . . . . . . . 11 (𝑣 = 𝑦 → (𝑣𝑣𝑦𝑣))
9 elequ2 2002 . . . . . . . . . . 11 (𝑣 = 𝑦 → (𝑦𝑣𝑦𝑦))
108, 9bitrd 268 . . . . . . . . . 10 (𝑣 = 𝑦 → (𝑣𝑣𝑦𝑦))
116, 7, 10dvelimf-o 34033 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦𝑦 → ∀𝑥 𝑦𝑦))
124biimprcd 240 . . . . . . . . . 10 (𝑦𝑦 → (𝑥 = 𝑦𝑥𝑥))
1312alimi 1737 . . . . . . . . 9 (∀𝑥 𝑦𝑦 → ∀𝑥(𝑥 = 𝑦𝑥𝑥))
1411, 13syl6 35 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦𝑦 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
1514adantr 481 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝑦𝑦 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
165, 15sylbid 230 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
1716adantl 482 . . . . 5 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
18 elequ1 1995 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥𝑥𝑧𝑥))
19 elequ2 2002 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
2018, 19sylan9bb 735 . . . . . . . 8 ((𝑥 = 𝑧𝑥 = 𝑤) → (𝑥𝑥𝑧𝑤))
2120sps-o 34012 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (𝑥𝑥𝑧𝑤))
22 nfa1-o 34019 . . . . . . . 8 𝑥𝑥(𝑥 = 𝑧𝑥 = 𝑤)
2321imbi2d 330 . . . . . . . 8 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥 = 𝑦𝑥𝑥) ↔ (𝑥 = 𝑦𝑧𝑤)))
2422, 23albid 2088 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑥𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
2521, 24imbi12d 334 . . . . . 6 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
2625adantr 481 . . . . 5 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
2717, 26mpbid 222 . . . 4 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
2827exp32 630 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
291, 28sylbir 225 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
30 elequ1 1995 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝑤𝑦𝑤))
3130ad2antll 764 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑤𝑦𝑤))
32 ax-c14 33995 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦𝑤 → ∀𝑥 𝑦𝑤)))
3332impcom 446 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦𝑤 → ∀𝑥 𝑦𝑤))
3433adantrr 752 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦𝑤 → ∀𝑥 𝑦𝑤))
3530biimprcd 240 . . . . . . . 8 (𝑦𝑤 → (𝑥 = 𝑦𝑥𝑤))
3635alimi 1737 . . . . . . 7 (∀𝑥 𝑦𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤))
3734, 36syl6 35 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)))
3831, 37sylbid 230 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)))
3938adantll 749 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)))
40 elequ1 1995 . . . . . . 7 (𝑥 = 𝑧 → (𝑥𝑤𝑧𝑤))
4140sps-o 34012 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (𝑥𝑤𝑧𝑤))
4241imbi2d 330 . . . . . . 7 (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦𝑥𝑤) ↔ (𝑥 = 𝑦𝑧𝑤)))
4342dral2-o 34034 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦𝑥𝑤) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
4441, 43imbi12d 334 . . . . 5 (∀𝑥 𝑥 = 𝑧 → ((𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
4544ad2antrr 761 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
4639, 45mpbid 222 . . 3 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
4746exp32 630 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
48 elequ2 2002 . . . . . . 7 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
4948ad2antll 764 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑥𝑧𝑦))
50 ax-c14 33995 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧𝑦 → ∀𝑥 𝑧𝑦)))
5150imp 445 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧𝑦 → ∀𝑥 𝑧𝑦))
5251adantrr 752 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑦 → ∀𝑥 𝑧𝑦))
5348biimprcd 240 . . . . . . . 8 (𝑧𝑦 → (𝑥 = 𝑦𝑧𝑥))
5453alimi 1737 . . . . . . 7 (∀𝑥 𝑧𝑦 → ∀𝑥(𝑥 = 𝑦𝑧𝑥))
5552, 54syl6 35 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑦 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)))
5649, 55sylbid 230 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)))
5756adantlr 750 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)))
5819sps-o 34012 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
5958imbi2d 330 . . . . . . 7 (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦𝑧𝑥) ↔ (𝑥 = 𝑦𝑧𝑤)))
6059dral2-o 34034 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦𝑧𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
6158, 60imbi12d 334 . . . . 5 (∀𝑥 𝑥 = 𝑤 → ((𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
6261ad2antlr 762 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
6357, 62mpbid 222 . . 3 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
6463exp32 630 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
65 ax6ev 1888 . . . . 5 𝑢 𝑢 = 𝑤
66 ax6ev 1888 . . . . . . 7 𝑣 𝑣 = 𝑧
67 ax-1 6 . . . . . . . . . . 11 (𝑣𝑢 → (𝑥 = 𝑦𝑣𝑢))
6867alrimiv 1853 . . . . . . . . . 10 (𝑣𝑢 → ∀𝑥(𝑥 = 𝑦𝑣𝑢))
69 elequ1 1995 . . . . . . . . . . . . 13 (𝑣 = 𝑧 → (𝑣𝑢𝑧𝑢))
70 elequ2 2002 . . . . . . . . . . . . 13 (𝑢 = 𝑤 → (𝑧𝑢𝑧𝑤))
7169, 70sylan9bb 735 . . . . . . . . . . . 12 ((𝑣 = 𝑧𝑢 = 𝑤) → (𝑣𝑢𝑧𝑤))
7271adantl 482 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑣𝑢𝑧𝑤))
73 dveeq2-o 34037 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
74 dveeq2-o 34037 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
7573, 74im2anan9 879 . . . . . . . . . . . . . 14 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
7675imp 445 . . . . . . . . . . . . 13 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
77 19.26 1796 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
7876, 77sylibr 224 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧𝑢 = 𝑤))
79 nfa1-o 34019 . . . . . . . . . . . . 13 𝑥𝑥(𝑣 = 𝑧𝑢 = 𝑤)
8071sps-o 34012 . . . . . . . . . . . . . 14 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (𝑣𝑢𝑧𝑤))
8180imbi2d 330 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → ((𝑥 = 𝑦𝑣𝑢) ↔ (𝑥 = 𝑦𝑧𝑤)))
8279, 81albid 2088 . . . . . . . . . . . 12 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑣𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
8378, 82syl 17 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦𝑣𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
8472, 83imbi12d 334 . . . . . . . . . 10 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ((𝑣𝑢 → ∀𝑥(𝑥 = 𝑦𝑣𝑢)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
8568, 84mpbii 223 . . . . . . . . 9 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
8685exp32 630 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
8786exlimdv 1859 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
8866, 87mpi 20 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
8988exlimdv 1859 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
9065, 89mpi 20 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
9190a1d 25 . . 3 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
9291a1d 25 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
9329, 47, 64, 924cases 989 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1479  ∃wex 1702 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-c5 33987  ax-c4 33988  ax-c7 33989  ax-c10 33990  ax-c11 33991  ax-c9 33994  ax-c14 33995 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator