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