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

Theorem ax12eq 36064
 Description: Basis step for constructing a substitution instance of ax-c15 36012 without using ax-c15 36012. 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 1864 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2 equid 2012 . . . . . . . 8 𝑥 = 𝑥
32a1i 11 . . . . . . 7 (𝑥 = 𝑦𝑥 = 𝑥)
43ax-gen 1789 . . . . . 6 𝑥(𝑥 = 𝑦𝑥 = 𝑥)
54a1i 11 . . . . 5 (𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥))
6 equequ1 2025 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥 = 𝑥𝑧 = 𝑥))
7 equequ2 2026 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
86, 7sylan9bb 512 . . . . . . . 8 ((𝑥 = 𝑧𝑥 = 𝑤) → (𝑥 = 𝑥𝑧 = 𝑤))
98sps-o 36031 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (𝑥 = 𝑥𝑧 = 𝑤))
10 nfa1-o 36038 . . . . . . . 8 𝑥𝑥(𝑥 = 𝑧𝑥 = 𝑤)
119imbi2d 343 . . . . . . . 8 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥 = 𝑦𝑥 = 𝑥) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
1210, 11albid 2216 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑥 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
139, 12imbi12d 347 . . . . . 6 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
1413adantr 483 . . . . 5 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
155, 14mpbii 235 . . . 4 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
1615exp32 423 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
171, 16sylbir 237 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
18 equequ1 2025 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 = 𝑤𝑦 = 𝑤))
1918ad2antll 727 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤𝑦 = 𝑤))
20 axc9 2393 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤)))
2120impcom 410 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
2221adantrr 715 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
23 equtrr 2022 . . . . . . . 8 (𝑦 = 𝑤 → (𝑥 = 𝑦𝑥 = 𝑤))
2423alimi 1805 . . . . . . 7 (∀𝑥 𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤))
2522, 24syl6 35 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
2619, 25sylbid 242 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
2726adantll 712 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
28 equequ1 2025 . . . . . . 7 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
2928sps-o 36031 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
3029imbi2d 343 . . . . . . 7 (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦𝑥 = 𝑤) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
3130dral2-o 36053 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦𝑥 = 𝑤) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
3229, 31imbi12d 347 . . . . 5 (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
3332ad2antrr 724 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
3427, 33mpbid 234 . . 3 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
3534exp32 423 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
36 equequ2 2026 . . . . . . 7 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
3736ad2antll 727 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥𝑧 = 𝑦))
38 axc9 2393 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)))
3938imp 409 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
4039adantrr 715 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
4136biimprcd 252 . . . . . . . 8 (𝑧 = 𝑦 → (𝑥 = 𝑦𝑧 = 𝑥))
4241alimi 1805 . . . . . . 7 (∀𝑥 𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥))
4340, 42syl6 35 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
4437, 43sylbid 242 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
4544adantlr 713 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
467sps-o 36031 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
4746imbi2d 343 . . . . . . 7 (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦𝑧 = 𝑥) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
4847dral2-o 36053 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦𝑧 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
4946, 48imbi12d 347 . . . . 5 (∀𝑥 𝑥 = 𝑤 → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
5049ad2antlr 725 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
5145, 50mpbid 234 . . 3 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
5251exp32 423 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
53 ax6ev 1965 . . . . 5 𝑢 𝑢 = 𝑤
54 ax6ev 1965 . . . . . . 7 𝑣 𝑣 = 𝑧
55 ax-1 6 . . . . . . . . . . 11 (𝑣 = 𝑢 → (𝑥 = 𝑦𝑣 = 𝑢))
5655alrimiv 1921 . . . . . . . . . 10 (𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦𝑣 = 𝑢))
57 equequ1 2025 . . . . . . . . . . . . 13 (𝑣 = 𝑧 → (𝑣 = 𝑢𝑧 = 𝑢))
58 equequ2 2026 . . . . . . . . . . . . 13 (𝑢 = 𝑤 → (𝑧 = 𝑢𝑧 = 𝑤))
5957, 58sylan9bb 512 . . . . . . . . . . . 12 ((𝑣 = 𝑧𝑢 = 𝑤) → (𝑣 = 𝑢𝑧 = 𝑤))
6059adantl 484 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑣 = 𝑢𝑧 = 𝑤))
61 dveeq2-o 36056 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
62 dveeq2-o 36056 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
6361, 62im2anan9 621 . . . . . . . . . . . . . 14 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
6463imp 409 . . . . . . . . . . . . 13 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
65 19.26 1864 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
6664, 65sylibr 236 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧𝑢 = 𝑤))
67 nfa1-o 36038 . . . . . . . . . . . . 13 𝑥𝑥(𝑣 = 𝑧𝑢 = 𝑤)
6859sps-o 36031 . . . . . . . . . . . . . 14 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (𝑣 = 𝑢𝑧 = 𝑤))
6968imbi2d 343 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → ((𝑥 = 𝑦𝑣 = 𝑢) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
7067, 69albid 2216 . . . . . . . . . . . 12 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7166, 70syl 17 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7260, 71imbi12d 347 . . . . . . . . . 10 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ((𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦𝑣 = 𝑢)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7356, 72mpbii 235 . . . . . . . . 9 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7473exp32 423 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
7574exlimdv 1927 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
7654, 75mpi 20 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7776exlimdv 1927 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7853, 77mpi 20 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7978a1d 25 . . 3 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
8079a1d 25 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
8117, 35, 52, 804cases 1034 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1528  ∃wex 1773 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2383  ax-c5 36006  ax-c4 36007  ax-c7 36008  ax-c10 36009  ax-c11 36010  ax-c9 36013 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator