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

Theorem ax12eq 33244
 Description: Basis step for constructing a substitution instance of ax-c15 33192 without using ax-c15 33192. 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 1786 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2 equid 1926 . . . . . . . 8 𝑥 = 𝑥
32a1i 11 . . . . . . 7 (𝑥 = 𝑦𝑥 = 𝑥)
43ax-gen 1713 . . . . . 6 𝑥(𝑥 = 𝑦𝑥 = 𝑥)
54a1i 11 . . . . 5 (𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥))
6 equequ1 1939 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥 = 𝑥𝑧 = 𝑥))
7 equequ2 1940 . . . . . . . . 9 (𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
86, 7sylan9bb 732 . . . . . . . 8 ((𝑥 = 𝑧𝑥 = 𝑤) → (𝑥 = 𝑥𝑧 = 𝑤))
98sps-o 33211 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (𝑥 = 𝑥𝑧 = 𝑤))
10 nfa1-o 33218 . . . . . . . 8 𝑥𝑥(𝑥 = 𝑧𝑥 = 𝑤)
119imbi2d 329 . . . . . . . 8 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥 = 𝑦𝑥 = 𝑥) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
1210, 11albid 2077 . . . . . . 7 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑥 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
139, 12imbi12d 333 . . . . . 6 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
1413adantr 480 . . . . 5 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
155, 14mpbii 222 . . . 4 ((∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
1615exp32 629 . . 3 (∀𝑥(𝑥 = 𝑧𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
171, 16sylbir 224 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
18 equequ1 1939 . . . . . . 7 (𝑥 = 𝑦 → (𝑥 = 𝑤𝑦 = 𝑤))
1918ad2antll 761 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤𝑦 = 𝑤))
20 axc9 2290 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤)))
2120impcom 445 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
2221adantrr 749 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥 𝑦 = 𝑤))
23 equtrr 1936 . . . . . . . 8 (𝑦 = 𝑤 → (𝑥 = 𝑦𝑥 = 𝑤))
2423alimi 1730 . . . . . . 7 (∀𝑥 𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤))
2522, 24syl6 34 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑦 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
2619, 25sylbid 229 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
2726adantll 746 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)))
28 equequ1 1939 . . . . . . 7 (𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
2928sps-o 33211 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑤𝑧 = 𝑤))
3029imbi2d 329 . . . . . . 7 (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦𝑥 = 𝑤) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
3130dral2-o 33233 . . . . . 6 (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦𝑥 = 𝑤) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
3229, 31imbi12d 333 . . . . 5 (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
3332ad2antrr 758 . . . 4 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑥 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑥 = 𝑤)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
3427, 33mpbid 221 . . 3 (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
3534exp32 629 . 2 ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
36 equequ2 1940 . . . . . . 7 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
3736ad2antll 761 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥𝑧 = 𝑦))
38 axc9 2290 . . . . . . . . 9 (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)))
3938imp 444 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
4039adantrr 749 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
4136biimprcd 239 . . . . . . . 8 (𝑧 = 𝑦 → (𝑥 = 𝑦𝑧 = 𝑥))
4241alimi 1730 . . . . . . 7 (∀𝑥 𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥))
4340, 42syl6 34 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
4437, 43sylbid 229 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
4544adantlr 747 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)))
467sps-o 33211 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (𝑧 = 𝑥𝑧 = 𝑤))
4746imbi2d 329 . . . . . . 7 (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦𝑧 = 𝑥) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
4847dral2-o 33233 . . . . . 6 (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦𝑧 = 𝑥) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
4946, 48imbi12d 333 . . . . 5 (∀𝑥 𝑥 = 𝑤 → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
5049ad2antlr 759 . . . 4 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → ((𝑧 = 𝑥 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑥)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
5145, 50mpbid 221 . . 3 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦𝑥 = 𝑦)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
5251exp32 629 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
53 ax6ev 1877 . . . . 5 𝑢 𝑢 = 𝑤
54 ax6ev 1877 . . . . . . 7 𝑣 𝑣 = 𝑧
55 ax-1 6 . . . . . . . . . . 11 (𝑣 = 𝑢 → (𝑥 = 𝑦𝑣 = 𝑢))
5655alrimiv 1842 . . . . . . . . . 10 (𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦𝑣 = 𝑢))
57 equequ1 1939 . . . . . . . . . . . . 13 (𝑣 = 𝑧 → (𝑣 = 𝑢𝑧 = 𝑢))
58 equequ2 1940 . . . . . . . . . . . . 13 (𝑢 = 𝑤 → (𝑧 = 𝑢𝑧 = 𝑤))
5957, 58sylan9bb 732 . . . . . . . . . . . 12 ((𝑣 = 𝑧𝑢 = 𝑤) → (𝑣 = 𝑢𝑧 = 𝑤))
6059adantl 481 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑣 = 𝑢𝑧 = 𝑤))
61 dveeq2-o 33236 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
62 dveeq2-o 33236 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
6361, 62im2anan9 876 . . . . . . . . . . . . . 14 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
6463imp 444 . . . . . . . . . . . . 13 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
65 19.26 1786 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
6664, 65sylibr 223 . . . . . . . . . . . 12 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧𝑢 = 𝑤))
67 nfa1-o 33218 . . . . . . . . . . . . 13 𝑥𝑥(𝑣 = 𝑧𝑢 = 𝑤)
6859sps-o 33211 . . . . . . . . . . . . . 14 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (𝑣 = 𝑢𝑧 = 𝑤))
6968imbi2d 329 . . . . . . . . . . . . 13 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → ((𝑥 = 𝑦𝑣 = 𝑢) ↔ (𝑥 = 𝑦𝑧 = 𝑤)))
7067, 69albid 2077 . . . . . . . . . . . 12 (∀𝑥(𝑣 = 𝑧𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7166, 70syl 17 . . . . . . . . . . 11 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦𝑣 = 𝑢) ↔ ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7260, 71imbi12d 333 . . . . . . . . . 10 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → ((𝑣 = 𝑢 → ∀𝑥(𝑥 = 𝑦𝑣 = 𝑢)) ↔ (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7356, 72mpbii 222 . . . . . . . . 9 (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧𝑢 = 𝑤)) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7473exp32 629 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
7574exlimdv 1848 . . . . . . 7 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
7654, 75mpi 20 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7776exlimdv 1848 . . . . 5 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
7853, 77mpi 20 . . . 4 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))
7978a1d 25 . . 3 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
8079a1d 25 . 2 ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤)))))
8117, 35, 52, 804cases 987 1 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 = 𝑤 → ∀𝑥(𝑥 = 𝑦𝑧 = 𝑤))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-c5 33186  ax-c4 33187  ax-c7 33188  ax-c10 33189  ax-c11 33190  ax-c9 33193 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator