Proof of Theorem ax12indalem
Step | Hyp | Ref
| Expression |
1 | | ax-1 6 |
. . . . . . . . 9
⊢
(∀𝑥𝜑 → (𝑥 = 𝑦 → ∀𝑥𝜑)) |
2 | 1 | axc4i-o 36921 |
. . . . . . . 8
⊢
(∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑)) |
3 | 2 | a1i 11 |
. . . . . . 7
⊢
(∀𝑧 𝑧 = 𝑥 → (∀𝑥𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑))) |
4 | | biidd 261 |
. . . . . . . 8
⊢
(∀𝑧 𝑧 = 𝑥 → (𝜑 ↔ 𝜑)) |
5 | 4 | dral1-o 36927 |
. . . . . . 7
⊢
(∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 ↔ ∀𝑥𝜑)) |
6 | 5 | imbi2d 341 |
. . . . . . . 8
⊢
(∀𝑧 𝑧 = 𝑥 → ((𝑥 = 𝑦 → ∀𝑧𝜑) ↔ (𝑥 = 𝑦 → ∀𝑥𝜑))) |
7 | 6 | dral2-o 36953 |
. . . . . . 7
⊢
(∀𝑧 𝑧 = 𝑥 → (∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑))) |
8 | 3, 5, 7 | 3imtr4d 294 |
. . . . . 6
⊢
(∀𝑧 𝑧 = 𝑥 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))) |
9 | 8 | aecoms-o 36925 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))) |
10 | 9 | a1d 25 |
. . . 4
⊢
(∀𝑥 𝑥 = 𝑧 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑)))) |
11 | 10 | a1d 25 |
. . 3
⊢
(∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))) |
12 | 11 | adantr 481 |
. 2
⊢
((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))) |
13 | | simplr 766 |
. . . . 5
⊢ ((((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ¬ ∀𝑥 𝑥 = 𝑦) |
14 | | aecom-o 36924 |
. . . . . . . . 9
⊢
(∀𝑧 𝑧 = 𝑥 → ∀𝑥 𝑥 = 𝑧) |
15 | 14 | con3i 154 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑧 → ¬ ∀𝑧 𝑧 = 𝑥) |
16 | | aecom-o 36924 |
. . . . . . . . 9
⊢
(∀𝑧 𝑧 = 𝑦 → ∀𝑦 𝑦 = 𝑧) |
17 | 16 | con3i 154 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ¬ ∀𝑧 𝑧 = 𝑦) |
18 | | axc9 2384 |
. . . . . . . . 9
⊢ (¬
∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦))) |
19 | 18 | imp 407 |
. . . . . . . 8
⊢ ((¬
∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
20 | 15, 17, 19 | syl2an 596 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)) |
21 | 20 | imp 407 |
. . . . . 6
⊢ (((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦) |
22 | 21 | adantlr 712 |
. . . . 5
⊢ ((((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → ∀𝑧 𝑥 = 𝑦) |
23 | | hbnae-o 36951 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) |
24 | | hba1-o 36920 |
. . . . . . 7
⊢
(∀𝑧 𝑥 = 𝑦 → ∀𝑧∀𝑧 𝑥 = 𝑦) |
25 | 23, 24 | hban 2301 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → ∀𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦)) |
26 | | ax-c5 36906 |
. . . . . . 7
⊢
(∀𝑧 𝑥 = 𝑦 → 𝑥 = 𝑦) |
27 | | ax12indalem.1 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))) |
28 | 27 | imp 407 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
29 | 26, 28 | sylan2 593 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
30 | 25, 29 | alimdh 1824 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑦 ∧ ∀𝑧 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑))) |
31 | 13, 22, 30 | syl2anc 584 |
. . . 4
⊢ ((((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑))) |
32 | | ax-11 2158 |
. . . . . 6
⊢
(∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥∀𝑧(𝑥 = 𝑦 → 𝜑)) |
33 | | hbnae-o 36951 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑧 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑧) |
34 | | hbnae-o 36951 |
. . . . . . . 8
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ∀𝑥 ¬ ∀𝑦 𝑦 = 𝑧) |
35 | 33, 34 | hban 2301 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∀𝑥(¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧)) |
36 | | hbnae-o 36951 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑧 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑧) |
37 | | hbnae-o 36951 |
. . . . . . . . . 10
⊢ (¬
∀𝑦 𝑦 = 𝑧 → ∀𝑧 ¬ ∀𝑦 𝑦 = 𝑧) |
38 | 36, 37 | hban 2301 |
. . . . . . . . 9
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∀𝑧(¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧)) |
39 | 38, 20 | nf5dh 2147 |
. . . . . . . 8
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑧 𝑥 = 𝑦) |
40 | | 19.21t 2203 |
. . . . . . . 8
⊢
(Ⅎ𝑧 𝑥 = 𝑦 → (∀𝑧(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑))) |
41 | 39, 40 | syl 17 |
. . . . . . 7
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑧(𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑦 → ∀𝑧𝜑))) |
42 | 35, 41 | albidh 1873 |
. . . . . 6
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑥∀𝑧(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))) |
43 | 32, 42 | syl5ib 243 |
. . . . 5
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))) |
44 | 43 | ad2antrr 723 |
. . . 4
⊢ ((((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧∀𝑥(𝑥 = 𝑦 → 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))) |
45 | 31, 44 | syld 47 |
. . 3
⊢ ((((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ ¬ ∀𝑥 𝑥 = 𝑦) ∧ 𝑥 = 𝑦) → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))) |
46 | 45 | exp31 420 |
. 2
⊢ ((¬
∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))) |
47 | 12, 46 | pm2.61ian 809 |
1
⊢ (¬
∀𝑦 𝑦 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑦 → ∀𝑧𝜑))))) |