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