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 33044
Description: Basis step for constructing a substitution instance of ax-c15 32991 without using ax-c15 32991. 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 1784 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2 elequ1 1982 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥𝑥𝑦𝑥))
3 elequ2 1989 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑦𝑥𝑦𝑦))
42, 3bitrd 266 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝑥𝑦𝑦))
54adantl 480 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝑥𝑥𝑦𝑦))
6 ax-5 1825 . . . . . . . . . 10 (𝑣𝑣 → ∀𝑥 𝑣𝑣)
7 ax-5 1825 . . . . . . . . . 10 (𝑦𝑦 → ∀𝑣 𝑦𝑦)
8 elequ1 1982 . . . . . . . . . . 11 (𝑣 = 𝑦 → (𝑣𝑣𝑦𝑣))
9 elequ2 1989 . . . . . . . . . . 11 (𝑣 = 𝑦 → (𝑦𝑣𝑦𝑦))
108, 9bitrd 266 . . . . . . . . . 10 (𝑣 = 𝑦 → (𝑣𝑣𝑦𝑦))
116, 7, 10dvelimf-o 33031 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦𝑦 → ∀𝑥 𝑦𝑦))
124biimprcd 238 . . . . . . . . . 10 (𝑦𝑦 → (𝑥 = 𝑦𝑥𝑥))
1312alimi 1728 . . . . . . . . 9 (∀𝑥 𝑦𝑦 → ∀𝑥(𝑥 = 𝑦𝑥𝑥))
1411, 13syl6 34 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦𝑦 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
1514adantr 479 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝑦𝑦 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
165, 15sylbid 228 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
1716adantl 480 . . . . 5 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
18 elequ1 1982 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥𝑥𝑧𝑥))
19 elequ2 1989 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
2018, 19sylan9bb 731 . . . . . . . 8 ((𝑥 = 𝑧𝑥 = 𝑤) → (𝑥𝑥𝑧𝑤))
2120sps-o 33010 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (𝑥𝑥𝑧𝑤))
22 nfa1-o 33017 . . . . . . . 8 𝑥𝑥(𝑥 = 𝑧𝑥 = 𝑤)
2321imbi2d 328 . . . . . . . 8 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥 = 𝑦𝑥𝑥) ↔ (𝑥 = 𝑦𝑧𝑤)))
2422, 23albid 2074 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑥𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
2521, 24imbi12d 332 . . . . . 6 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
2625adantr 479 . . . . 5 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
2717, 26mpbid 220 . . . 4 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
2827exp32 628 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
291, 28sylbir 223 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
30 elequ1 1982 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝑤𝑦𝑤))
3130ad2antll 760 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑤𝑦𝑤))
32 ax-c14 32993 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦𝑤 → ∀𝑥 𝑦𝑤)))
3332impcom 444 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦𝑤 → ∀𝑥 𝑦𝑤))
3433adantrr 748 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦𝑤 → ∀𝑥 𝑦𝑤))
3530biimprcd 238 . . . . . . . 8 (𝑦𝑤 → (𝑥 = 𝑦𝑥𝑤))
3635alimi 1728 . . . . . . 7 (∀𝑥 𝑦𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤))
3734, 36syl6 34 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)))
3831, 37sylbid 228 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)))
3938adantll 745 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)))
40 elequ1 1982 . . . . . . 7 (𝑥 = 𝑧 → (𝑥𝑤𝑧𝑤))
4140sps-o 33010 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (𝑥𝑤𝑧𝑤))
4241imbi2d 328 . . . . . . 7 (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦𝑥𝑤) ↔ (𝑥 = 𝑦𝑧𝑤)))
4342dral2-o 33032 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦𝑥𝑤) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
4441, 43imbi12d 332 . . . . 5 (∀𝑥 𝑥 = 𝑧 → ((𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
4544ad2antrr 757 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
4639, 45mpbid 220 . . 3 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
4746exp32 628 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
48 elequ2 1989 . . . . . . 7 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
4948ad2antll 760 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑥𝑧𝑦))
50 ax-c14 32993 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧𝑦 → ∀𝑥 𝑧𝑦)))
5150imp 443 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧𝑦 → ∀𝑥 𝑧𝑦))
5251adantrr 748 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑦 → ∀𝑥 𝑧𝑦))
5348biimprcd 238 . . . . . . . 8 (𝑧𝑦 → (𝑥 = 𝑦𝑧𝑥))
5453alimi 1728 . . . . . . 7 (∀𝑥 𝑧𝑦 → ∀𝑥(𝑥 = 𝑦𝑧𝑥))
5552, 54syl6 34 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑦 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)))
5649, 55sylbid 228 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)))
5756adantlr 746 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)))
5819sps-o 33010 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
5958imbi2d 328 . . . . . . 7 (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦𝑧𝑥) ↔ (𝑥 = 𝑦𝑧𝑤)))
6059dral2-o 33032 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦𝑧𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
6158, 60imbi12d 332 . . . . 5 (∀𝑥 𝑥 = 𝑤 → ((𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
6261ad2antlr 758 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
6357, 62mpbid 220 . . 3 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
6463exp32 628 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
65 ax6ev 1875 . . . . 5 𝑢 𝑢 = 𝑤
66 ax6ev 1875 . . . . . . 7 𝑣 𝑣 = 𝑧
67 ax-1 6 . . . . . . . . . . 11 (𝑣𝑢 → (𝑥 = 𝑦𝑣𝑢))
6867alrimiv 1840 . . . . . . . . . 10 (𝑣𝑢 → ∀𝑥(𝑥 = 𝑦𝑣𝑢))
69 elequ1 1982 . . . . . . . . . . . . 13 (𝑣 = 𝑧 → (𝑣𝑢𝑧𝑢))
70 elequ2 1989 . . . . . . . . . . . . 13 (𝑢 = 𝑤 → (𝑧𝑢𝑧𝑤))
7169, 70sylan9bb 731 . . . . . . . . . . . 12 ((𝑣 = 𝑧𝑢 = 𝑤) → (𝑣𝑢𝑧𝑤))
7271adantl 480 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑣𝑢𝑧𝑤))
73 dveeq2-o 33035 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
74 dveeq2-o 33035 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
7573, 74im2anan9 875 . . . . . . . . . . . . . 14 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
7675imp 443 . . . . . . . . . . . . 13 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
77 19.26 1784 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
7876, 77sylibr 222 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧𝑢 = 𝑤))
79 nfa1-o 33017 . . . . . . . . . . . . 13 𝑥𝑥(𝑣 = 𝑧𝑢 = 𝑤)
8071sps-o 33010 . . . . . . . . . . . . . 14 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (𝑣𝑢𝑧𝑤))
8180imbi2d 328 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → ((𝑥 = 𝑦𝑣𝑢) ↔ (𝑥 = 𝑦𝑧𝑤)))
8279, 81albid 2074 . . . . . . . . . . . 12 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑣𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
8378, 82syl 17 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦𝑣𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
8472, 83imbi12d 332 . . . . . . . . . 10 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ((𝑣𝑢 → ∀𝑥(𝑥 = 𝑦𝑣𝑢)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
8568, 84mpbii 221 . . . . . . . . 9 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
8685exp32 628 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
8786exlimdv 1846 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
8866, 87mpi 20 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
8988exlimdv 1846 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
9065, 89mpi 20 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
9190a1d 25 . . 3 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
9291a1d 25 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
9329, 47, 64, 924cases 986 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  wal 1472  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-c5 32985  ax-c4 32986  ax-c7 32987  ax-c10 32988  ax-c11 32989  ax-c9 32992  ax-c14 32993
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator