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 34954
Description: Basis step for constructing a substitution instance of ax-c15 34902 without using ax-c15 34902. 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 1969 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2 equid 2111 . . . . . . . 8 𝑥 = 𝑥
32a1i 11 . . . . . . 7 (𝑥 = 𝑦𝑥 = 𝑥)
43ax-gen 1891 . . . . . 6 𝑥(𝑥 = 𝑦𝑥 = 𝑥)
54a1i 11 . . . . 5 (𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥))
6 equequ1 2124 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥 = 𝑥𝑧 = 𝑥))
7 equequ2 2125 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
86, 7sylan9bb 506 . . . . . . . 8 ((𝑥 = 𝑧𝑥 = 𝑤) → (𝑥 = 𝑥𝑧 = 𝑤))
98sps-o 34921 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (𝑥 = 𝑥𝑧 = 𝑤))
10 nfa1-o 34928 . . . . . . . 8 𝑥𝑥(𝑥 = 𝑧𝑥 = 𝑤)
119imbi2d 332 . . . . . . . 8 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥 = 𝑦𝑥 = 𝑥) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
1210, 11albid 2257 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑥 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
139, 12imbi12d 336 . . . . . 6 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
1413adantr 473 . . . . 5 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
155, 14mpbii 225 . . . 4 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
1615exp32 412 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
171, 16sylbir 227 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
18 equequ1 2124 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 = 𝑤𝑦 = 𝑤))
1918ad2antll 721 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤𝑦 = 𝑤))
20 axc9 2366 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤)))
2120impcom 397 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
2221adantrr 709 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
23 equtrr 2121 . . . . . . . 8 (𝑦 = 𝑤 → (𝑥 = 𝑦𝑥 = 𝑤))
2423alimi 1907 . . . . . . 7 (∀𝑥 𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤))
2522, 24syl6 35 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
2619, 25sylbid 232 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
2726adantll 706 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
28 equequ1 2124 . . . . . . 7 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
2928sps-o 34921 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
3029imbi2d 332 . . . . . . 7 (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦𝑥 = 𝑤) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
3130dral2-o 34943 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦𝑥 = 𝑤) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
3229, 31imbi12d 336 . . . . 5 (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
3332ad2antrr 718 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
3427, 33mpbid 224 . . 3 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
3534exp32 412 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
36 equequ2 2125 . . . . . . 7 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
3736ad2antll 721 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥𝑧 = 𝑦))
38 axc9 2366 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)))
3938imp 396 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
4039adantrr 709 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
4136biimprcd 242 . . . . . . . 8 (𝑧 = 𝑦 → (𝑥 = 𝑦𝑧 = 𝑥))
4241alimi 1907 . . . . . . 7 (∀𝑥 𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥))
4340, 42syl6 35 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
4437, 43sylbid 232 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
4544adantlr 707 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
467sps-o 34921 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
4746imbi2d 332 . . . . . . 7 (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦𝑧 = 𝑥) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
4847dral2-o 34943 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦𝑧 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
4946, 48imbi12d 336 . . . . 5 (∀𝑥 𝑥 = 𝑤 → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
5049ad2antlr 719 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
5145, 50mpbid 224 . . 3 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
5251exp32 412 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
53 ax6ev 2074 . . . . 5 𝑢 𝑢 = 𝑤
54 ax6ev 2074 . . . . . . 7 𝑣 𝑣 = 𝑧
55 ax-1 6 . . . . . . . . . . 11 (𝑣 = 𝑢 → (𝑥 = 𝑦𝑣 = 𝑢))
5655alrimiv 2023 . . . . . . . . . 10 (𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦𝑣 = 𝑢))
57 equequ1 2124 . . . . . . . . . . . . 13 (𝑣 = 𝑧 → (𝑣 = 𝑢𝑧 = 𝑢))
58 equequ2 2125 . . . . . . . . . . . . 13 (𝑢 = 𝑤 → (𝑧 = 𝑢𝑧 = 𝑤))
5957, 58sylan9bb 506 . . . . . . . . . . . 12 ((𝑣 = 𝑧𝑢 = 𝑤) → (𝑣 = 𝑢𝑧 = 𝑤))
6059adantl 474 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑣 = 𝑢𝑧 = 𝑤))
61 dveeq2-o 34946 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
62 dveeq2-o 34946 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
6361, 62im2anan9 614 . . . . . . . . . . . . . 14 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
6463imp 396 . . . . . . . . . . . . 13 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
65 19.26 1969 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
6664, 65sylibr 226 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧𝑢 = 𝑤))
67 nfa1-o 34928 . . . . . . . . . . . . 13 𝑥𝑥(𝑣 = 𝑧𝑢 = 𝑤)
6859sps-o 34921 . . . . . . . . . . . . . 14 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (𝑣 = 𝑢𝑧 = 𝑤))
6968imbi2d 332 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → ((𝑥 = 𝑦𝑣 = 𝑢) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
7067, 69albid 2257 . . . . . . . . . . . 12 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7166, 70syl 17 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7260, 71imbi12d 336 . . . . . . . . . 10 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ((𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦𝑣 = 𝑢)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7356, 72mpbii 225 . . . . . . . . 9 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7473exp32 412 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
7574exlimdv 2029 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
7654, 75mpi 20 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7776exlimdv 2029 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7853, 77mpi 20 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7978a1d 25 . . 3 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
8079a1d 25 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
8117, 35, 52, 804cases 1064 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 385  wal 1651  wex 1875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-c5 34896  ax-c4 34897  ax-c7 34898  ax-c10 34899  ax-c11 34900  ax-c9 34903
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator