Step |
Hyp |
Ref |
Expression |
1 |
|
df-rab |
⊢ { 𝑠 ∈ 𝒫 𝒫 𝑜 ∣ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) } = { 𝑠 ∣ ( 𝑠 ∈ 𝒫 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } |
2 |
|
velpw |
⊢ ( 𝑠 ∈ 𝒫 𝒫 𝑜 ↔ 𝑠 ⊆ 𝒫 𝑜 ) |
3 |
2
|
anbi1i |
⊢ ( ( 𝑠 ∈ 𝒫 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) ↔ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) ) |
4 |
3
|
abbii |
⊢ { 𝑠 ∣ ( 𝑠 ∈ 𝒫 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } = { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } |
5 |
1 4
|
eqtri |
⊢ { 𝑠 ∈ 𝒫 𝒫 𝑜 ∣ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) } = { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } |
6 |
|
vex |
⊢ 𝑜 ∈ V |
7 |
|
pwexg |
⊢ ( 𝑜 ∈ V → 𝒫 𝑜 ∈ V ) |
8 |
|
pwexg |
⊢ ( 𝒫 𝑜 ∈ V → 𝒫 𝒫 𝑜 ∈ V ) |
9 |
6 7 8
|
mp2b |
⊢ 𝒫 𝒫 𝑜 ∈ V |
10 |
9
|
rabex |
⊢ { 𝑠 ∈ 𝒫 𝒫 𝑜 ∣ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) } ∈ V |
11 |
5 10
|
eqeltrri |
⊢ { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } ∈ V |