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

Theorem ax12el 34750
 Description: Basis step for constructing a substitution instance of ax-c15 34697 without using ax-c15 34697. 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 1949 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2 elequ1 2152 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥𝑥𝑦𝑥))
3 elequ2 2159 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑦𝑥𝑦𝑦))
42, 3bitrd 268 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝑥𝑦𝑦))
54adantl 467 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝑥𝑥𝑦𝑦))
6 ax-5 1991 . . . . . . . . . 10 (𝑣𝑣 → ∀𝑥 𝑣𝑣)
7 ax-5 1991 . . . . . . . . . 10 (𝑦𝑦 → ∀𝑣 𝑦𝑦)
8 elequ1 2152 . . . . . . . . . . 11 (𝑣 = 𝑦 → (𝑣𝑣𝑦𝑣))
9 elequ2 2159 . . . . . . . . . . 11 (𝑣 = 𝑦 → (𝑦𝑣𝑦𝑦))
108, 9bitrd 268 . . . . . . . . . 10 (𝑣 = 𝑦 → (𝑣𝑣𝑦𝑦))
116, 7, 10dvelimf-o 34737 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦𝑦 → ∀𝑥 𝑦𝑦))
124biimprcd 240 . . . . . . . . . 10 (𝑦𝑦 → (𝑥 = 𝑦𝑥𝑥))
1312alimi 1887 . . . . . . . . 9 (∀𝑥 𝑦𝑦 → ∀𝑥(𝑥 = 𝑦𝑥𝑥))
1411, 13syl6 35 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦𝑦 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
1514adantr 466 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝑦𝑦 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
165, 15sylbid 230 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦) → (𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
1716adantl 467 . . . . 5 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)))
18 elequ1 2152 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥𝑥𝑧𝑥))
19 elequ2 2159 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
2018, 19sylan9bb 499 . . . . . . . 8 ((𝑥 = 𝑧𝑥 = 𝑤) → (𝑥𝑥𝑧𝑤))
2120sps-o 34716 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (𝑥𝑥𝑧𝑤))
22 nfa1-o 34723 . . . . . . . 8 𝑥𝑥(𝑥 = 𝑧𝑥 = 𝑤)
2321imbi2d 329 . . . . . . . 8 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥 = 𝑦𝑥𝑥) ↔ (𝑥 = 𝑦𝑧𝑤)))
2422, 23albid 2246 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑥𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
2521, 24imbi12d 333 . . . . . 6 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
2625adantr 466 . . . . 5 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥𝑥 → ∀𝑥(𝑥 = 𝑦𝑥𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
2717, 26mpbid 222 . . . 4 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
2827exp32 407 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
291, 28sylbir 225 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
30 elequ1 2152 . . . . . . 7 (𝑥 = 𝑦 → (𝑥𝑤𝑦𝑤))
3130ad2antll 708 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑤𝑦𝑤))
32 ax-c14 34699 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦𝑤 → ∀𝑥 𝑦𝑤)))
3332impcom 394 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦𝑤 → ∀𝑥 𝑦𝑤))
3433adantrr 696 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦𝑤 → ∀𝑥 𝑦𝑤))
3530biimprcd 240 . . . . . . . 8 (𝑦𝑤 → (𝑥 = 𝑦𝑥𝑤))
3635alimi 1887 . . . . . . 7 (∀𝑥 𝑦𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤))
3734, 36syl6 35 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)))
3831, 37sylbid 230 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)))
3938adantll 693 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)))
40 elequ1 2152 . . . . . . 7 (𝑥 = 𝑧 → (𝑥𝑤𝑧𝑤))
4140sps-o 34716 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (𝑥𝑤𝑧𝑤))
4241imbi2d 329 . . . . . . 7 (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦𝑥𝑤) ↔ (𝑥 = 𝑦𝑧𝑤)))
4342dral2-o 34738 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦𝑥𝑤) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
4441, 43imbi12d 333 . . . . 5 (∀𝑥 𝑥 = 𝑧 → ((𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
4544ad2antrr 705 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥𝑤 → ∀𝑥(𝑥 = 𝑦𝑥𝑤)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
4639, 45mpbid 222 . . 3 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
4746exp32 407 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
48 elequ2 2159 . . . . . . 7 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
4948ad2antll 708 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑥𝑧𝑦))
50 ax-c14 34699 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧𝑦 → ∀𝑥 𝑧𝑦)))
5150imp 393 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧𝑦 → ∀𝑥 𝑧𝑦))
5251adantrr 696 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑦 → ∀𝑥 𝑧𝑦))
5348biimprcd 240 . . . . . . . 8 (𝑧𝑦 → (𝑥 = 𝑦𝑧𝑥))
5453alimi 1887 . . . . . . 7 (∀𝑥 𝑧𝑦 → ∀𝑥(𝑥 = 𝑦𝑧𝑥))
5552, 54syl6 35 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑦 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)))
5649, 55sylbid 230 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)))
5756adantlr 694 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)))
5819sps-o 34716 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (𝑧𝑥𝑧𝑤))
5958imbi2d 329 . . . . . . 7 (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦𝑧𝑥) ↔ (𝑥 = 𝑦𝑧𝑤)))
6059dral2-o 34738 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦𝑧𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
6158, 60imbi12d 333 . . . . 5 (∀𝑥 𝑥 = 𝑤 → ((𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
6261ad2antlr 706 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑧𝑥 → ∀𝑥(𝑥 = 𝑦𝑧𝑥)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
6357, 62mpbid 222 . . 3 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
6463exp32 407 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
65 ax6ev 2059 . . . . 5 𝑢 𝑢 = 𝑤
66 ax6ev 2059 . . . . . . 7 𝑣 𝑣 = 𝑧
67 ax-1 6 . . . . . . . . . . 11 (𝑣𝑢 → (𝑥 = 𝑦𝑣𝑢))
6867alrimiv 2007 . . . . . . . . . 10 (𝑣𝑢 → ∀𝑥(𝑥 = 𝑦𝑣𝑢))
69 elequ1 2152 . . . . . . . . . . . . 13 (𝑣 = 𝑧 → (𝑣𝑢𝑧𝑢))
70 elequ2 2159 . . . . . . . . . . . . 13 (𝑢 = 𝑤 → (𝑧𝑢𝑧𝑤))
7169, 70sylan9bb 499 . . . . . . . . . . . 12 ((𝑣 = 𝑧𝑢 = 𝑤) → (𝑣𝑢𝑧𝑤))
7271adantl 467 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑣𝑢𝑧𝑤))
73 dveeq2-o 34741 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
74 dveeq2-o 34741 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
7573, 74im2anan9 606 . . . . . . . . . . . . . 14 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
7675imp 393 . . . . . . . . . . . . 13 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
77 19.26 1949 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
7876, 77sylibr 224 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧𝑢 = 𝑤))
79 nfa1-o 34723 . . . . . . . . . . . . 13 𝑥𝑥(𝑣 = 𝑧𝑢 = 𝑤)
8071sps-o 34716 . . . . . . . . . . . . . 14 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (𝑣𝑢𝑧𝑤))
8180imbi2d 329 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → ((𝑥 = 𝑦𝑣𝑢) ↔ (𝑥 = 𝑦𝑧𝑤)))
8279, 81albid 2246 . . . . . . . . . . . 12 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑣𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
8378, 82syl 17 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦𝑣𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
8472, 83imbi12d 333 . . . . . . . . . 10 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ((𝑣𝑢 → ∀𝑥(𝑥 = 𝑦𝑣𝑢)) ↔ (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
8568, 84mpbii 223 . . . . . . . . 9 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
8685exp32 407 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
8786exlimdv 2013 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
8866, 87mpi 20 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
8988exlimdv 2013 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
9065, 89mpi 20 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))
9190a1d 25 . . 3 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
9291a1d 25 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤)))))
9329, 47, 64, 924cases 1025 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧𝑤 → ∀𝑥(𝑥 = 𝑦𝑧𝑤))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382  ∀wal 1629  ∃wex 1852 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-c5 34691  ax-c4 34692  ax-c7 34693  ax-c10 34694  ax-c11 34695  ax-c9 34698  ax-c14 34699 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator