Proof of Theorem axprlem3
Step | Hyp | Ref
| Expression |
1 | | axrep4v 5290 |
. 2
⊢
(∀𝑠∃𝑧∀𝑤(if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧) → ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))) |
2 | | ifptru 1074 |
. . . . . . 7
⊢
(∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥)) |
3 | 2 | biimpd 229 |
. . . . . 6
⊢
(∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑥)) |
4 | | equeuclr 2020 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (𝑤 = 𝑥 → 𝑤 = 𝑧)) |
5 | 3, 4 | syl9r 78 |
. . . . 5
⊢ (𝑧 = 𝑥 → (∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧))) |
6 | 5 | alrimdv 1927 |
. . . 4
⊢ (𝑧 = 𝑥 → (∃𝑛 𝑛 ∈ 𝑠 → ∀𝑤(if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧))) |
7 | 6 | spimevw 1992 |
. . 3
⊢
(∃𝑛 𝑛 ∈ 𝑠 → ∃𝑧∀𝑤(if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧)) |
8 | | ifpfal 1075 |
. . . . . . 7
⊢ (¬
∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦)) |
9 | 8 | biimpd 229 |
. . . . . 6
⊢ (¬
∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑦)) |
10 | | equeuclr 2020 |
. . . . . 6
⊢ (𝑧 = 𝑦 → (𝑤 = 𝑦 → 𝑤 = 𝑧)) |
11 | 9, 10 | syl9r 78 |
. . . . 5
⊢ (𝑧 = 𝑦 → (¬ ∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧))) |
12 | 11 | alrimdv 1927 |
. . . 4
⊢ (𝑧 = 𝑦 → (¬ ∃𝑛 𝑛 ∈ 𝑠 → ∀𝑤(if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧))) |
13 | 12 | spimevw 1992 |
. . 3
⊢ (¬
∃𝑛 𝑛 ∈ 𝑠 → ∃𝑧∀𝑤(if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧)) |
14 | 7, 13 | pm2.61i 182 |
. 2
⊢
∃𝑧∀𝑤(if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧) |
15 | 1, 14 | mpg 1794 |
1
⊢
∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) |