Metamath Proof Explorer


Theorem sigaex

Description: Lemma for issiga and isrnsiga . The class of sigma-algebras with base set o is a set. Note: a more generic version with ( O e. _V -> ... ) could be useful for sigaval . (Contributed by Thierry Arnoux, 24-Oct-2016)

Ref Expression
Assertion sigaex { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜𝑠 ∧ ∀ 𝑥𝑠 ( 𝑜𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → 𝑥𝑠 ) ) ) } ∈ V

Proof

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