Step | Hyp | Ref
| Expression |
1 | | axprlem3 5430 |
. . 3
⊢
∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) |
2 | | axprlem1 5428 |
. . . . . . . . 9
⊢
∃𝑠∀𝑛(∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑛 ∈ 𝑠) |
3 | 2 | sepexi 5306 |
. . . . . . . 8
⊢
∃𝑠∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) |
4 | | biimp 215 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → (𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛)) |
5 | | ax-nul 5311 |
. . . . . . . . . 10
⊢
∃𝑛∀𝑡 ¬ 𝑡 ∈ 𝑛 |
6 | | exbi 1843 |
. . . . . . . . . 10
⊢
(∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → (∃𝑛 𝑛 ∈ 𝑠 ↔ ∃𝑛∀𝑡 ¬ 𝑡 ∈ 𝑛)) |
7 | 5, 6 | mpbiri 258 |
. . . . . . . . 9
⊢
(∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → ∃𝑛 𝑛 ∈ 𝑠) |
8 | | ifptru 1074 |
. . . . . . . . 9
⊢
(∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥)) |
9 | 7, 8 | syl 17 |
. . . . . . . 8
⊢
(∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥)) |
10 | 3, 4, 9 | axprlem4 5431 |
. . . . . . 7
⊢
(∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (𝑤 = 𝑥 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))) |
11 | | ax-nul 5311 |
. . . . . . . 8
⊢
∃𝑠∀𝑛 ¬ 𝑛 ∈ 𝑠 |
12 | | pm2.21 123 |
. . . . . . . 8
⊢ (¬
𝑛 ∈ 𝑠 → (𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛)) |
13 | | alnex 1777 |
. . . . . . . . 9
⊢
(∀𝑛 ¬
𝑛 ∈ 𝑠 ↔ ¬ ∃𝑛 𝑛 ∈ 𝑠) |
14 | | ifpfal 1075 |
. . . . . . . . 9
⊢ (¬
∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦)) |
15 | 13, 14 | sylbi 217 |
. . . . . . . 8
⊢
(∀𝑛 ¬
𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦)) |
16 | 11, 12, 15 | axprlem4 5431 |
. . . . . . 7
⊢
(∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (𝑤 = 𝑦 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))) |
17 | 10, 16 | jaod 859 |
. . . . . 6
⊢
(∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))) |
18 | | imbi2 348 |
. . . . . 6
⊢ ((𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) ↔ ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))) |
19 | 17, 18 | syl5ibrcom 247 |
. . . . 5
⊢
(∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → ((𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧))) |
20 | 19 | alimdv 1913 |
. . . 4
⊢
(∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧))) |
21 | 20 | eximdv 1914 |
. . 3
⊢
(∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧))) |
22 | 1, 21 | mpi 20 |
. 2
⊢
(∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)) |
23 | | axprlem2 5429 |
. 2
⊢
∃𝑝∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) |
24 | 22, 23 | exlimiiv 1928 |
1
⊢
∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) |