Proof of Theorem ax12inda2ALT
Step | Hyp | Ref
| Expression |
1 | | ax-1 6 |
. . . . . . . 8
⊢
(∀𝑥𝜑 → (𝑥 = 𝑦 → ∀𝑥𝜑)) |
2 | 1 | axc4i-o 34183 |
. . . . . . 7
⊢
(∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑)) |
3 | 2 | a1i 11 |
. . . . . 6
⊢
(∀𝑧 𝑧 = 𝑥 → (∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑))) |
4 | | biidd 252 |
. . . . . . 7
⊢
(∀𝑧 𝑧 = 𝑥 → (𝜑 ↔ 𝜑)) |
5 | 4 | dral1-o 34189 |
. . . . . 6
⊢
(∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 ↔ ∀𝑥𝜑)) |
6 | 5 | imbi2d 330 |
. . . . . . 7
⊢
(∀𝑧 𝑧 = 𝑥 → ((𝑥 = 𝑦 → ∀𝑧𝜑) ↔ (𝑥 = 𝑦 → ∀𝑥𝜑))) |
7 | 6 | dral2-o 34215 |
. . . . . 6
⊢
(∀𝑧 𝑧 = 𝑥 → (∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑))) |
8 | 3, 5, 7 | 3imtr4d 283 |
. . . . 5
⊢
(∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))) |
9 | 8 | aecoms-o 34187 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))) |
10 | 9 | a1d 25 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) |
11 | 10 | a1d 25 |
. 2
⊢
(∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))) |
12 | | simplr 792 |
. . . . 5
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ¬ ∀𝑥 𝑥 = 𝑦) |
13 | | dveeq1-o 34220 |
. . . . . . . 8
⊢ (¬
∀𝑧 𝑧 = 𝑥 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
14 | 13 | naecoms-o 34212 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
15 | 14 | imp 445 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ 𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦) |
16 | 15 | adantlr 751 |
. . . . 5
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦) |
17 | | hbnae-o 34213 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) |
18 | | hba1-o 34182 |
. . . . . . 7
⊢
(∀𝑧 𝑥 = 𝑦 → ∀𝑧∀𝑧 𝑥 = 𝑦) |
19 | 17, 18 | hban 2128 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → ∀𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦)) |
20 | | ax-c5 34168 |
. . . . . . 7
⊢
(∀𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦) |
21 | | ax12inda2.1 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) |
22 | 21 | imp 445 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
23 | 20, 22 | sylan2 491 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
24 | 19, 23 | alimdh 1745 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑))) |
25 | 12, 16, 24 | syl2anc 693 |
. . . 4
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑))) |
26 | | ax-11 2034 |
. . . . . 6
⊢
(∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥∀𝑧(𝑥 = 𝑦 → 𝜑)) |
27 | | hbnae-o 34213 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑧 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑧) |
28 | | hbnae-o 34213 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑧 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑧) |
29 | 28, 14 | nf5dh 2026 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑥 = 𝑦) |
30 | | 19.21t 2073 |
. . . . . . . 8
⊢
(Ⅎ𝑧 𝑥 = 𝑦 → (∀𝑧(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑))) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑧 → (∀𝑧(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑))) |
32 | 27, 31 | albidh 1793 |
. . . . . 6
⊢ (¬
∀𝑥 𝑥 = 𝑧 → (∀𝑥∀𝑧(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))) |
33 | 26, 32 | syl5ib 234 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑧 → (∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))) |
34 | 33 | ad2antrr 762 |
. . . 4
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))) |
35 | 25, 34 | syld 47 |
. . 3
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))) |
36 | 35 | exp31 630 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))) |
37 | 11, 36 | pm2.61i 176 |
1
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) |