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

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

Proof of Theorem ax12eq
Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 19.26 1873 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2 equid 2015 . . . . . . . 8 𝑥 = 𝑥
32a1i 11 . . . . . . 7 (𝑥 = 𝑦𝑥 = 𝑥)
43ax-gen 1798 . . . . . 6 𝑥(𝑥 = 𝑦𝑥 = 𝑥)
54a1i 11 . . . . 5 (𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥))
6 equequ1 2028 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥 = 𝑥𝑧 = 𝑥))
7 equequ2 2029 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
86, 7sylan9bb 510 . . . . . . . 8 ((𝑥 = 𝑧𝑥 = 𝑤) → (𝑥 = 𝑥𝑧 = 𝑤))
98sps-o 36922 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (𝑥 = 𝑥𝑧 = 𝑤))
10 nfa1-o 36929 . . . . . . . 8 𝑥𝑥(𝑥 = 𝑧𝑥 = 𝑤)
119imbi2d 341 . . . . . . . 8 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥 = 𝑦𝑥 = 𝑥) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
1210, 11albid 2215 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑥 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
139, 12imbi12d 345 . . . . . 6 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
1413adantr 481 . . . . 5 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
155, 14mpbii 232 . . . 4 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
1615exp32 421 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
171, 16sylbir 234 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
18 equequ1 2028 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 = 𝑤𝑦 = 𝑤))
1918ad2antll 726 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤𝑦 = 𝑤))
20 axc9 2382 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤)))
2120impcom 408 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
2221adantrr 714 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
23 equtrr 2025 . . . . . . . 8 (𝑦 = 𝑤 → (𝑥 = 𝑦𝑥 = 𝑤))
2423alimi 1814 . . . . . . 7 (∀𝑥 𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤))
2522, 24syl6 35 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
2619, 25sylbid 239 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
2726adantll 711 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
28 equequ1 2028 . . . . . . 7 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
2928sps-o 36922 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
3029imbi2d 341 . . . . . . 7 (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦𝑥 = 𝑤) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
3130dral2-o 36944 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦𝑥 = 𝑤) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
3229, 31imbi12d 345 . . . . 5 (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
3332ad2antrr 723 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
3427, 33mpbid 231 . . 3 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
3534exp32 421 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
36 equequ2 2029 . . . . . . 7 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
3736ad2antll 726 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥𝑧 = 𝑦))
38 axc9 2382 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)))
3938imp 407 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
4039adantrr 714 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
4136biimprcd 249 . . . . . . . 8 (𝑧 = 𝑦 → (𝑥 = 𝑦𝑧 = 𝑥))
4241alimi 1814 . . . . . . 7 (∀𝑥 𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥))
4340, 42syl6 35 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
4437, 43sylbid 239 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
4544adantlr 712 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
467sps-o 36922 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
4746imbi2d 341 . . . . . . 7 (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦𝑧 = 𝑥) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
4847dral2-o 36944 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦𝑧 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
4946, 48imbi12d 345 . . . . 5 (∀𝑥 𝑥 = 𝑤 → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
5049ad2antlr 724 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
5145, 50mpbid 231 . . 3 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
5251exp32 421 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
53 ax6ev 1973 . . . . 5 𝑢 𝑢 = 𝑤
54 ax6ev 1973 . . . . . . 7 𝑣 𝑣 = 𝑧
55 ax-1 6 . . . . . . . . . . 11 (𝑣 = 𝑢 → (𝑥 = 𝑦𝑣 = 𝑢))
5655alrimiv 1930 . . . . . . . . . 10 (𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦𝑣 = 𝑢))
57 equequ1 2028 . . . . . . . . . . . . 13 (𝑣 = 𝑧 → (𝑣 = 𝑢𝑧 = 𝑢))
58 equequ2 2029 . . . . . . . . . . . . 13 (𝑢 = 𝑤 → (𝑧 = 𝑢𝑧 = 𝑤))
5957, 58sylan9bb 510 . . . . . . . . . . . 12 ((𝑣 = 𝑧𝑢 = 𝑤) → (𝑣 = 𝑢𝑧 = 𝑤))
6059adantl 482 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑣 = 𝑢𝑧 = 𝑤))
61 dveeq2-o 36947 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
62 dveeq2-o 36947 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
6361, 62im2anan9 620 . . . . . . . . . . . . . 14 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
6463imp 407 . . . . . . . . . . . . 13 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
65 19.26 1873 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
6664, 65sylibr 233 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧𝑢 = 𝑤))
67 nfa1-o 36929 . . . . . . . . . . . . 13 𝑥𝑥(𝑣 = 𝑧𝑢 = 𝑤)
6859sps-o 36922 . . . . . . . . . . . . . 14 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (𝑣 = 𝑢𝑧 = 𝑤))
6968imbi2d 341 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → ((𝑥 = 𝑦𝑣 = 𝑢) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
7067, 69albid 2215 . . . . . . . . . . . 12 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7166, 70syl 17 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7260, 71imbi12d 345 . . . . . . . . . 10 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ((𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦𝑣 = 𝑢)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7356, 72mpbii 232 . . . . . . . . 9 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7473exp32 421 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
7574exlimdv 1936 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
7654, 75mpi 20 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7776exlimdv 1936 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7853, 77mpi 20 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7978a1d 25 . . 3 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
8079a1d 25 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
8117, 35, 52, 804cases 1038 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wal 1537  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2372  ax-c5 36897  ax-c4 36898  ax-c7 36899  ax-c10 36900  ax-c11 36901  ax-c9 36904
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator