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

Theorem ax12el 35958
Description: Basis step for constructing a substitution instance of ax-c15 35905 without using ax-c15 35905. 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 1862 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2 elequ1 2112 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥𝑥𝑦𝑥))
3 elequ2 2120 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑦𝑥𝑦𝑦))
42, 3bitrd 280 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝑥𝑦𝑦))
54adantl 482 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝑥𝑥𝑦𝑦))
6 ax-5 1902 . . . . . . . . . 10 (𝑣𝑣 → ∀𝑥 𝑣𝑣)
7 ax-5 1902 . . . . . . . . . 10 (𝑦𝑦 → ∀𝑣 𝑦𝑦)
8 elequ1 2112 . . . . . . . . . . 11 (𝑣 = 𝑦 → (𝑣𝑣𝑦𝑣))
9 elequ2 2120 . . . . . . . . . . 11 (𝑣 = 𝑦 → (𝑦𝑣𝑦𝑦))
108, 9bitrd 280 . . . . . . . . . 10 (𝑣 = 𝑦 → (𝑣𝑣𝑦𝑦))
116, 7, 10dvelimf-o 35945 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦𝑦 → ∀𝑥 𝑦𝑦))
124biimprcd 251 . . . . . . . . . 10 (𝑦𝑦 → (𝑥 = 𝑦𝑥𝑥))
1312alimi 1803 . . . . . . . . 9 (∀𝑥 𝑦𝑦 → ∀𝑥(𝑥 = 𝑦𝑥𝑥))
1411, 13syl6 35 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦𝑦 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
1514adantr 481 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝑦𝑦 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
165, 15sylbid 241 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
1716adantl 482 . . . . 5 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
18 elequ1 2112 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥𝑥𝑧𝑥))
19 elequ2 2120 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
2018, 19sylan9bb 510 . . . . . . . 8 ((𝑥 = 𝑧𝑥 = 𝑤) → (𝑥𝑥𝑧𝑤))
2120sps-o 35924 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (𝑥𝑥𝑧𝑤))
22 nfa1-o 35931 . . . . . . . 8 𝑥𝑥(𝑥 = 𝑧𝑥 = 𝑤)
2321imbi2d 342 . . . . . . . 8 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥 = 𝑦𝑥𝑥) ↔ (𝑥 = 𝑦𝑧𝑤)))
2422, 23albid 2214 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑥𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
2521, 24imbi12d 346 . . . . . 6 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
2625adantr 481 . . . . 5 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
2717, 26mpbid 233 . . . 4 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
2827exp32 421 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
291, 28sylbir 236 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
30 elequ1 2112 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝑤𝑦𝑤))
3130ad2antll 725 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑤𝑦𝑤))
32 ax-c14 35907 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦𝑤 → ∀𝑥 𝑦𝑤)))
3332impcom 408 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦𝑤 → ∀𝑥 𝑦𝑤))
3433adantrr 713 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦𝑤 → ∀𝑥 𝑦𝑤))
3530biimprcd 251 . . . . . . . 8 (𝑦𝑤 → (𝑥 = 𝑦𝑥𝑤))
3635alimi 1803 . . . . . . 7 (∀𝑥 𝑦𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤))
3734, 36syl6 35 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)))
3831, 37sylbid 241 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)))
3938adantll 710 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)))
40 elequ1 2112 . . . . . . 7 (𝑥 = 𝑧 → (𝑥𝑤𝑧𝑤))
4140sps-o 35924 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (𝑥𝑤𝑧𝑤))
4241imbi2d 342 . . . . . . 7 (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦𝑥𝑤) ↔ (𝑥 = 𝑦𝑧𝑤)))
4342dral2-o 35946 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦𝑥𝑤) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
4441, 43imbi12d 346 . . . . 5 (∀𝑥 𝑥 = 𝑧 → ((𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
4544ad2antrr 722 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
4639, 45mpbid 233 . . 3 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
4746exp32 421 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
48 elequ2 2120 . . . . . . 7 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
4948ad2antll 725 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑥𝑧𝑦))
50 ax-c14 35907 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧𝑦 → ∀𝑥 𝑧𝑦)))
5150imp 407 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧𝑦 → ∀𝑥 𝑧𝑦))
5251adantrr 713 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑦 → ∀𝑥 𝑧𝑦))
5348biimprcd 251 . . . . . . . 8 (𝑧𝑦 → (𝑥 = 𝑦𝑧𝑥))
5453alimi 1803 . . . . . . 7 (∀𝑥 𝑧𝑦 → ∀𝑥(𝑥 = 𝑦𝑧𝑥))
5552, 54syl6 35 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑦 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)))
5649, 55sylbid 241 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)))
5756adantlr 711 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)))
5819sps-o 35924 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
5958imbi2d 342 . . . . . . 7 (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦𝑧𝑥) ↔ (𝑥 = 𝑦𝑧𝑤)))
6059dral2-o 35946 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦𝑧𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
6158, 60imbi12d 346 . . . . 5 (∀𝑥 𝑥 = 𝑤 → ((𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
6261ad2antlr 723 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
6357, 62mpbid 233 . . 3 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
6463exp32 421 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
65 ax6ev 1963 . . . . 5 𝑢 𝑢 = 𝑤
66 ax6ev 1963 . . . . . . 7 𝑣 𝑣 = 𝑧
67 ax-1 6 . . . . . . . . . . 11 (𝑣𝑢 → (𝑥 = 𝑦𝑣𝑢))
6867alrimiv 1919 . . . . . . . . . 10 (𝑣𝑢 → ∀𝑥(𝑥 = 𝑦𝑣𝑢))
69 elequ1 2112 . . . . . . . . . . . . 13 (𝑣 = 𝑧 → (𝑣𝑢𝑧𝑢))
70 elequ2 2120 . . . . . . . . . . . . 13 (𝑢 = 𝑤 → (𝑧𝑢𝑧𝑤))
7169, 70sylan9bb 510 . . . . . . . . . . . 12 ((𝑣 = 𝑧𝑢 = 𝑤) → (𝑣𝑢𝑧𝑤))
7271adantl 482 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑣𝑢𝑧𝑤))
73 dveeq2-o 35949 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
74 dveeq2-o 35949 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
7573, 74im2anan9 619 . . . . . . . . . . . . . 14 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
7675imp 407 . . . . . . . . . . . . 13 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
77 19.26 1862 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
7876, 77sylibr 235 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧𝑢 = 𝑤))
79 nfa1-o 35931 . . . . . . . . . . . . 13 𝑥𝑥(𝑣 = 𝑧𝑢 = 𝑤)
8071sps-o 35924 . . . . . . . . . . . . . 14 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (𝑣𝑢𝑧𝑤))
8180imbi2d 342 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → ((𝑥 = 𝑦𝑣𝑢) ↔ (𝑥 = 𝑦𝑧𝑤)))
8279, 81albid 2214 . . . . . . . . . . . 12 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑣𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
8378, 82syl 17 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦𝑣𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
8472, 83imbi12d 346 . . . . . . . . . 10 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ((𝑣𝑢 → ∀𝑥(𝑥 = 𝑦𝑣𝑢)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
8568, 84mpbii 234 . . . . . . . . 9 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
8685exp32 421 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
8786exlimdv 1925 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
8866, 87mpi 20 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
8988exlimdv 1925 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
9065, 89mpi 20 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
9190a1d 25 . . 3 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
9291a1d 25 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
9329, 47, 64, 924cases 1032 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wal 1526  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-13 2381  ax-c5 35899  ax-c4 35900  ax-c7 35901  ax-c10 35902  ax-c11 35903  ax-c9 35906  ax-c14 35907
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator