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 36610
Description: Basis step for constructing a substitution instance of ax-c15 36558 without using ax-c15 36558. 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 1877 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2 equid 2024 . . . . . . . 8 𝑥 = 𝑥
32a1i 11 . . . . . . 7 (𝑥 = 𝑦𝑥 = 𝑥)
43ax-gen 1802 . . . . . 6 𝑥(𝑥 = 𝑦𝑥 = 𝑥)
54a1i 11 . . . . 5 (𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥))
6 equequ1 2037 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥 = 𝑥𝑧 = 𝑥))
7 equequ2 2038 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
86, 7sylan9bb 513 . . . . . . . 8 ((𝑥 = 𝑧𝑥 = 𝑤) → (𝑥 = 𝑥𝑧 = 𝑤))
98sps-o 36577 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (𝑥 = 𝑥𝑧 = 𝑤))
10 nfa1-o 36584 . . . . . . . 8 𝑥𝑥(𝑥 = 𝑧𝑥 = 𝑤)
119imbi2d 344 . . . . . . . 8 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥 = 𝑦𝑥 = 𝑥) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
1210, 11albid 2224 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑥 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
139, 12imbi12d 348 . . . . . 6 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
1413adantr 484 . . . . 5 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
155, 14mpbii 236 . . . 4 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
1615exp32 424 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
171, 16sylbir 238 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
18 equequ1 2037 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 = 𝑤𝑦 = 𝑤))
1918ad2antll 729 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤𝑦 = 𝑤))
20 axc9 2383 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤)))
2120impcom 411 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
2221adantrr 717 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
23 equtrr 2034 . . . . . . . 8 (𝑦 = 𝑤 → (𝑥 = 𝑦𝑥 = 𝑤))
2423alimi 1818 . . . . . . 7 (∀𝑥 𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤))
2522, 24syl6 35 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
2619, 25sylbid 243 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
2726adantll 714 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
28 equequ1 2037 . . . . . . 7 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
2928sps-o 36577 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
3029imbi2d 344 . . . . . . 7 (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦𝑥 = 𝑤) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
3130dral2-o 36599 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦𝑥 = 𝑤) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
3229, 31imbi12d 348 . . . . 5 (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
3332ad2antrr 726 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
3427, 33mpbid 235 . . 3 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
3534exp32 424 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
36 equequ2 2038 . . . . . . 7 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
3736ad2antll 729 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥𝑧 = 𝑦))
38 axc9 2383 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)))
3938imp 410 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
4039adantrr 717 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
4136biimprcd 253 . . . . . . . 8 (𝑧 = 𝑦 → (𝑥 = 𝑦𝑧 = 𝑥))
4241alimi 1818 . . . . . . 7 (∀𝑥 𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥))
4340, 42syl6 35 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
4437, 43sylbid 243 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
4544adantlr 715 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
467sps-o 36577 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
4746imbi2d 344 . . . . . . 7 (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦𝑧 = 𝑥) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
4847dral2-o 36599 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦𝑧 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
4946, 48imbi12d 348 . . . . 5 (∀𝑥 𝑥 = 𝑤 → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
5049ad2antlr 727 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
5145, 50mpbid 235 . . 3 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
5251exp32 424 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
53 ax6ev 1977 . . . . 5 𝑢 𝑢 = 𝑤
54 ax6ev 1977 . . . . . . 7 𝑣 𝑣 = 𝑧
55 ax-1 6 . . . . . . . . . . 11 (𝑣 = 𝑢 → (𝑥 = 𝑦𝑣 = 𝑢))
5655alrimiv 1934 . . . . . . . . . 10 (𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦𝑣 = 𝑢))
57 equequ1 2037 . . . . . . . . . . . . 13 (𝑣 = 𝑧 → (𝑣 = 𝑢𝑧 = 𝑢))
58 equequ2 2038 . . . . . . . . . . . . 13 (𝑢 = 𝑤 → (𝑧 = 𝑢𝑧 = 𝑤))
5957, 58sylan9bb 513 . . . . . . . . . . . 12 ((𝑣 = 𝑧𝑢 = 𝑤) → (𝑣 = 𝑢𝑧 = 𝑤))
6059adantl 485 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑣 = 𝑢𝑧 = 𝑤))
61 dveeq2-o 36602 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
62 dveeq2-o 36602 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
6361, 62im2anan9 623 . . . . . . . . . . . . . 14 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
6463imp 410 . . . . . . . . . . . . 13 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
65 19.26 1877 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
6664, 65sylibr 237 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧𝑢 = 𝑤))
67 nfa1-o 36584 . . . . . . . . . . . . 13 𝑥𝑥(𝑣 = 𝑧𝑢 = 𝑤)
6859sps-o 36577 . . . . . . . . . . . . . 14 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (𝑣 = 𝑢𝑧 = 𝑤))
6968imbi2d 344 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → ((𝑥 = 𝑦𝑣 = 𝑢) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
7067, 69albid 2224 . . . . . . . . . . . 12 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7166, 70syl 17 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7260, 71imbi12d 348 . . . . . . . . . 10 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ((𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦𝑣 = 𝑢)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7356, 72mpbii 236 . . . . . . . . 9 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7473exp32 424 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
7574exlimdv 1940 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
7654, 75mpi 20 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7776exlimdv 1940 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7853, 77mpi 20 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7978a1d 25 . . 3 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
8079a1d 25 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
8117, 35, 52, 804cases 1040 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wal 1540  wex 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-10 2145  ax-11 2162  ax-12 2179  ax-13 2373  ax-c5 36552  ax-c4 36553  ax-c7 36554  ax-c10 36555  ax-c11 36556  ax-c9 36559
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator