Metamath Proof Explorer

Theorem issiga

Description: An alternative definition of the sigma-algebra, for a given base set. (Contributed by Thierry Arnoux, 19-Sep-2016)

Ref Expression
Assertion issiga ( 𝑆 ∈ V → ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( 𝑆 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elfvex ⊢ ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑂 ∈ V )
2 elex ⊢ ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑆 ∈ V )
3 1 2 jca ⊢ ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) → ( 𝑂 ∈ V ∧ 𝑆 ∈ V ) )
4 3 a1i ⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) → ( 𝑂 ∈ V ∧ 𝑆 ∈ V ) ) )
5 simpr1 ⊢ ( ( 𝑆 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) → 𝑂 ∈ 𝑆 )
6 elex ⊢ ( 𝑂 ∈ 𝑆 → 𝑂 ∈ V )
7 5 6 syl ⊢ ( ( 𝑆 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) → 𝑂 ∈ V )
8 7 a1i ⊢ ( 𝑆 ∈ V → ( ( 𝑆 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) → 𝑂 ∈ V ) )
9 8 anc2ri ⊢ ( 𝑆 ∈ V → ( ( 𝑆 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) → ( 𝑂 ∈ V ∧ 𝑆 ∈ V ) ) )
10 df-siga ⊢ sigAlgebra = ( 𝑜 ∈ V ↦ { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } )
11 sigaex ⊢ { 𝑠 ∣ ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) } ∈ V
12 pweq ⊢ ( 𝑜 = 𝑂 → 𝒫 𝑜 = 𝒫 𝑂 )
13 12 sseq2d ⊢ ( 𝑜 = 𝑂 → ( 𝑠 ⊆ 𝒫 𝑜 ↔ 𝑠 ⊆ 𝒫 𝑂 ) )
14 sseq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ⊆ 𝒫 𝑂 ↔ 𝑆 ⊆ 𝒫 𝑂 ) )
15 13 14 sylan9bb ⊢ ( ( 𝑜 = 𝑂 ∧ 𝑠 = 𝑆 ) → ( 𝑠 ⊆ 𝒫 𝑜 ↔ 𝑆 ⊆ 𝒫 𝑂 ) )
16 eleq12 ⊢ ( ( 𝑜 = 𝑂 ∧ 𝑠 = 𝑆 ) → ( 𝑜 ∈ 𝑠 ↔ 𝑂 ∈ 𝑆 ) )
17 simpr ⊢ ( ( 𝑜 = 𝑂 ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 )
18 difeq1 ⊢ ( 𝑜 = 𝑂 → ( 𝑜 ∖ 𝑥 ) = ( 𝑂 ∖ 𝑥 ) )
19 18 adantr ⊢ ( ( 𝑜 = 𝑂 ∧ 𝑠 = 𝑆 ) → ( 𝑜 ∖ 𝑥 ) = ( 𝑂 ∖ 𝑥 ) )
20 19 eleq1d ⊢ ( ( 𝑜 = 𝑂 ∧ 𝑠 = 𝑆 ) → ( ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ↔ ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ) )
21 eleq2 ⊢ ( 𝑠 = 𝑆 → ( ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ↔ ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ) )
22 21 adantl ⊢ ( ( 𝑜 = 𝑂 ∧ 𝑠 = 𝑆 ) → ( ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ↔ ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ) )
23 20 22 bitrd ⊢ ( ( 𝑜 = 𝑂 ∧ 𝑠 = 𝑆 ) → ( ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ↔ ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ) )
24 17 23 raleqbidv ⊢ ( ( 𝑜 = 𝑂 ∧ 𝑠 = 𝑆 ) → ( ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ↔ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ) )
25 pweq ⊢ ( 𝑠 = 𝑆 → 𝒫 𝑠 = 𝒫 𝑆 )
26 eleq2 ⊢ ( 𝑠 = 𝑆 → ( ∪ 𝑥 ∈ 𝑠 ↔ ∪ 𝑥 ∈ 𝑆 ) )
27 26 imbi2d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ↔ ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) )
28 25 27 raleqbidv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) )
29 28 adantl ⊢ ( ( 𝑜 = 𝑂 ∧ 𝑠 = 𝑆 ) → ( ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ↔ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) )
30 16 24 29 3anbi123d ⊢ ( ( 𝑜 = 𝑂 ∧ 𝑠 = 𝑆 ) → ( ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ↔ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
31 15 30 anbi12d ⊢ ( ( 𝑜 = 𝑂 ∧ 𝑠 = 𝑆 ) → ( ( 𝑠 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑜 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) ↔ ( 𝑆 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )
32 10 11 31 abfmpel ⊢ ( ( 𝑂 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( 𝑆 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )
33 32 a1i ⊢ ( 𝑆 ∈ V → ( ( 𝑂 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( 𝑆 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) ) )
34 4 9 33 pm5.21ndd ⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( 𝑆 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )