Proof of Theorem wl-ax11-lem8
Step | Hyp | Ref
| Expression |
1 | | axc11n 2307 |
. . 3
⊢
(∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑥 = 𝑦) |
2 | 1 | con3i 150 |
. 2
⊢ (¬
∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑦 𝑦 = 𝑥) |
3 | | wl-ax11-lem1 33362 |
. . . . . . 7
⊢
(∀𝑢 𝑢 = 𝑦 → (∀𝑢 𝑢 = 𝑥 ↔ ∀𝑦 𝑦 = 𝑥)) |
4 | 3 | notbid 308 |
. . . . . 6
⊢
(∀𝑢 𝑢 = 𝑦 → (¬ ∀𝑢 𝑢 = 𝑥 ↔ ¬ ∀𝑦 𝑦 = 𝑥)) |
5 | 4 | anbi1d 741 |
. . . . 5
⊢
(∀𝑢 𝑢 = 𝑦 → ((¬ ∀𝑢 𝑢 = 𝑥 ∧ ∀𝑢∀𝑥[𝑢 / 𝑦]𝜑) ↔ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ∀𝑢∀𝑥[𝑢 / 𝑦]𝜑))) |
6 | 4 | anbi1d 741 |
. . . . . . . 8
⊢
(∀𝑢 𝑢 = 𝑦 → ((¬ ∀𝑢 𝑢 = 𝑥 ∧ ∀𝑥[𝑢 / 𝑦]𝜑) ↔ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ∀𝑥[𝑢 / 𝑦]𝜑))) |
7 | | axc11n 2307 |
. . . . . . . . . . 11
⊢
(∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥) |
8 | 7 | con3i 150 |
. . . . . . . . . 10
⊢ (¬
∀𝑦 𝑦 = 𝑥 → ¬ ∀𝑥 𝑥 = 𝑦) |
9 | | wl-ax11-lem4 33365 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) |
10 | | sbequ12 2111 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑢 → (𝜑 ↔ [𝑢 / 𝑦]𝜑)) |
11 | 10 | equcoms 1947 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑦 → (𝜑 ↔ [𝑢 / 𝑦]𝜑)) |
12 | 11 | sps 2055 |
. . . . . . . . . . . . 13
⊢
(∀𝑢 𝑢 = 𝑦 → (𝜑 ↔ [𝑢 / 𝑦]𝜑)) |
13 | 12 | adantr 481 |
. . . . . . . . . . . 12
⊢
((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝜑 ↔ [𝑢 / 𝑦]𝜑)) |
14 | 9, 13 | albid 2090 |
. . . . . . . . . . 11
⊢
((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑥𝜑 ↔ ∀𝑥[𝑢 / 𝑦]𝜑)) |
15 | 14 | ex 450 |
. . . . . . . . . 10
⊢
(∀𝑢 𝑢 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑥[𝑢 / 𝑦]𝜑))) |
16 | 8, 15 | syl5 34 |
. . . . . . . . 9
⊢
(∀𝑢 𝑢 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 ↔ ∀𝑥[𝑢 / 𝑦]𝜑))) |
17 | 16 | pm5.32d 671 |
. . . . . . . 8
⊢
(∀𝑢 𝑢 = 𝑦 → ((¬ ∀𝑦 𝑦 = 𝑥 ∧ ∀𝑥𝜑) ↔ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ∀𝑥[𝑢 / 𝑦]𝜑))) |
18 | 6, 17 | bitr4d 271 |
. . . . . . 7
⊢
(∀𝑢 𝑢 = 𝑦 → ((¬ ∀𝑢 𝑢 = 𝑥 ∧ ∀𝑥[𝑢 / 𝑦]𝜑) ↔ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ∀𝑥𝜑))) |
19 | 18 | dral1 2325 |
. . . . . 6
⊢
(∀𝑢 𝑢 = 𝑦 → (∀𝑢(¬ ∀𝑢 𝑢 = 𝑥 ∧ ∀𝑥[𝑢 / 𝑦]𝜑) ↔ ∀𝑦(¬ ∀𝑦 𝑦 = 𝑥 ∧ ∀𝑥𝜑))) |
20 | | wl-ax11-lem7 33368 |
. . . . . 6
⊢
(∀𝑢(¬
∀𝑢 𝑢 = 𝑥 ∧ ∀𝑥[𝑢 / 𝑦]𝜑) ↔ (¬ ∀𝑢 𝑢 = 𝑥 ∧ ∀𝑢∀𝑥[𝑢 / 𝑦]𝜑)) |
21 | | wl-ax11-lem7 33368 |
. . . . . 6
⊢
(∀𝑦(¬
∀𝑦 𝑦 = 𝑥 ∧ ∀𝑥𝜑) ↔ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ∀𝑦∀𝑥𝜑)) |
22 | 19, 20, 21 | 3bitr3g 302 |
. . . . 5
⊢
(∀𝑢 𝑢 = 𝑦 → ((¬ ∀𝑢 𝑢 = 𝑥 ∧ ∀𝑢∀𝑥[𝑢 / 𝑦]𝜑) ↔ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ∀𝑦∀𝑥𝜑))) |
23 | 5, 22 | bitr3d 270 |
. . . 4
⊢
(∀𝑢 𝑢 = 𝑦 → ((¬ ∀𝑦 𝑦 = 𝑥 ∧ ∀𝑢∀𝑥[𝑢 / 𝑦]𝜑) ↔ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ∀𝑦∀𝑥𝜑))) |
24 | | pm5.32 668 |
. . . 4
⊢ ((¬
∀𝑦 𝑦 = 𝑥 → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥𝜑)) ↔ ((¬ ∀𝑦 𝑦 = 𝑥 ∧ ∀𝑢∀𝑥[𝑢 / 𝑦]𝜑) ↔ (¬ ∀𝑦 𝑦 = 𝑥 ∧ ∀𝑦∀𝑥𝜑))) |
25 | 23, 24 | sylibr 224 |
. . 3
⊢
(∀𝑢 𝑢 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑥 → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥𝜑))) |
26 | 25 | imp 445 |
. 2
⊢
((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑦 𝑦 = 𝑥) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥𝜑)) |
27 | 2, 26 | sylan2 491 |
1
⊢
((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥𝜑)) |