Proof of Theorem ssclaxsep
| Step | Hyp | Ref
| Expression |
| 1 | | ax-sep 5294 |
. . . 4
⊢
∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) |
| 2 | | biimp 215 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → (𝑥 ∈ 𝑦 → (𝑥 ∈ 𝑧 ∧ 𝜑))) |
| 3 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑧 ∧ 𝜑) → 𝑥 ∈ 𝑧) |
| 4 | 2, 3 | syl6 35 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → (𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧)) |
| 5 | 4 | alimi 1811 |
. . . . . . . 8
⊢
(∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → ∀𝑥(𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧)) |
| 6 | | velpw 4603 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 𝑧 ↔ 𝑦 ⊆ 𝑧) |
| 7 | | df-ss 3967 |
. . . . . . . . 9
⊢ (𝑦 ⊆ 𝑧 ↔ ∀𝑥(𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧)) |
| 8 | 6, 7 | bitr2i 276 |
. . . . . . . 8
⊢
(∀𝑥(𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) ↔ 𝑦 ∈ 𝒫 𝑧) |
| 9 | 5, 8 | sylib 218 |
. . . . . . 7
⊢
(∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → 𝑦 ∈ 𝒫 𝑧) |
| 10 | | ssel 3976 |
. . . . . . 7
⊢
(𝒫 𝑧 ⊆
𝑀 → (𝑦 ∈ 𝒫 𝑧 → 𝑦 ∈ 𝑀)) |
| 11 | 9, 10 | syl5 34 |
. . . . . 6
⊢
(𝒫 𝑧 ⊆
𝑀 → (∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → 𝑦 ∈ 𝑀)) |
| 12 | | alral 3074 |
. . . . . 6
⊢
(∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))) |
| 13 | 11, 12 | jca2 513 |
. . . . 5
⊢
(𝒫 𝑧 ⊆
𝑀 → (∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → (𝑦 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))) |
| 14 | 13 | eximdv 1917 |
. . . 4
⊢
(𝒫 𝑧 ⊆
𝑀 → (∃𝑦∀𝑥(𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) → ∃𝑦(𝑦 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))))) |
| 15 | 1, 14 | mpi 20 |
. . 3
⊢
(𝒫 𝑧 ⊆
𝑀 → ∃𝑦(𝑦 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))) |
| 16 | | df-rex 3070 |
. . 3
⊢
(∃𝑦 ∈
𝑀 ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)) ↔ ∃𝑦(𝑦 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))) |
| 17 | 15, 16 | sylibr 234 |
. 2
⊢
(𝒫 𝑧 ⊆
𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))) |
| 18 | 17 | ralimi 3082 |
1
⊢
(∀𝑧 ∈
𝑀 𝒫 𝑧 ⊆ 𝑀 → ∀𝑧 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))) |