Metamath Proof Explorer

Theorem issgon

Description: Property of being a sigma-algebra with a given base set, noting that the base set of a sigma-algebra is actually its union set. (Contributed by Thierry Arnoux, 24-Sep-2016) (Revised by Thierry Arnoux, 23-Oct-2016)

Ref Expression
Assertion issgon ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑂 = ∪ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 fvssunirn ⊢ ( sigAlgebra ‘ 𝑂 ) ⊆ ∪ ran sigAlgebra
2 1 sseli ⊢ ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑆 ∈ ∪ ran sigAlgebra )
3 elex ⊢ ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑆 ∈ V )
4 issiga ⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( 𝑆 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )
5 elpwuni ⊢ ( 𝑂 ∈ 𝑆 → ( 𝑆 ⊆ 𝒫 𝑂 ↔ ∪ 𝑆 = 𝑂 ) )
6 5 biimpa ⊢ ( ( 𝑂 ∈ 𝑆 ∧ 𝑆 ⊆ 𝒫 𝑂 ) → ∪ 𝑆 = 𝑂 )
7 ancom ⊢ ( ( 𝑆 ⊆ 𝒫 𝑂 ∧ 𝑂 ∈ 𝑆 ) ↔ ( 𝑂 ∈ 𝑆 ∧ 𝑆 ⊆ 𝒫 𝑂 ) )
8 eqcom ⊢ ( 𝑂 = ∪ 𝑆 ↔ ∪ 𝑆 = 𝑂 )
9 6 7 8 3imtr4i ⊢ ( ( 𝑆 ⊆ 𝒫 𝑂 ∧ 𝑂 ∈ 𝑆 ) → 𝑂 = ∪ 𝑆 )
10 9 3ad2antr1 ⊢ ( ( 𝑆 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) → 𝑂 = ∪ 𝑆 )
11 4 10 biimtrdi ⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑂 = ∪ 𝑆 ) )
12 3 11 mpcom ⊢ ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑂 = ∪ 𝑆 )
13 2 12 jca ⊢ ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) → ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑂 = ∪ 𝑆 ) )
14 elex ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ V )
15 isrnsiga ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra ↔ ( 𝑆 ∈ V ∧ ∃ 𝑜 ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )
16 15 simprbi ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∃ 𝑜 ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
17 elpwuni ⊢ ( 𝑜 ∈ 𝑆 → ( 𝑆 ⊆ 𝒫 𝑜 ↔ ∪ 𝑆 = 𝑜 ) )
18 17 biimpa ⊢ ( ( 𝑜 ∈ 𝑆 ∧ 𝑆 ⊆ 𝒫 𝑜 ) → ∪ 𝑆 = 𝑜 )
19 ancom ⊢ ( ( 𝑆 ⊆ 𝒫 𝑜 ∧ 𝑜 ∈ 𝑆 ) ↔ ( 𝑜 ∈ 𝑆 ∧ 𝑆 ⊆ 𝒫 𝑜 ) )
20 eqcom ⊢ ( 𝑜 = ∪ 𝑆 ↔ ∪ 𝑆 = 𝑜 )
21 18 19 20 3imtr4i ⊢ ( ( 𝑆 ⊆ 𝒫 𝑜 ∧ 𝑜 ∈ 𝑆 ) → 𝑜 = ∪ 𝑆 )
22 21 3ad2antr1 ⊢ ( ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) → 𝑜 = ∪ 𝑆 )
23 pweq ⊢ ( 𝑜 = ∪ 𝑆 → 𝒫 𝑜 = 𝒫 ∪ 𝑆 )
24 23 sseq2d ⊢ ( 𝑜 = ∪ 𝑆 → ( 𝑆 ⊆ 𝒫 𝑜 ↔ 𝑆 ⊆ 𝒫 ∪ 𝑆 ) )
25 eleq1 ⊢ ( 𝑜 = ∪ 𝑆 → ( 𝑜 ∈ 𝑆 ↔ ∪ 𝑆 ∈ 𝑆 ) )
26 difeq1 ⊢ ( 𝑜 = ∪ 𝑆 → ( 𝑜 ∖ 𝑥 ) = ( ∪ 𝑆 ∖ 𝑥 ) )
27 26 eleq1d ⊢ ( 𝑜 = ∪ 𝑆 → ( ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ↔ ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ) )
28 27 ralbidv ⊢ ( 𝑜 = ∪ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ↔ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ) )
29 25 28 3anbi12d ⊢ ( 𝑜 = ∪ 𝑆 → ( ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ↔ ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
30 24 29 anbi12d ⊢ ( 𝑜 = ∪ 𝑆 → ( ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ↔ ( 𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )
31 22 30 syl ⊢ ( ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) → ( ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ↔ ( 𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )
32 31 ibi ⊢ ( ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) → ( 𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
33 32 exlimiv ⊢ ( ∃ 𝑜 ( 𝑆 ⊆ 𝒫 𝑜 ∧ ( 𝑜 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑜 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) → ( 𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
34 16 33 syl ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
35 34 simprd ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) )
36 14 35 jca ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑆 ∈ V ∧ ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
37 eleq1 ⊢ ( 𝑂 = ∪ 𝑆 → ( 𝑂 ∈ 𝑆 ↔ ∪ 𝑆 ∈ 𝑆 ) )
38 difeq1 ⊢ ( 𝑂 = ∪ 𝑆 → ( 𝑂 ∖ 𝑥 ) = ( ∪ 𝑆 ∖ 𝑥 ) )
39 38 eleq1d ⊢ ( 𝑂 = ∪ 𝑆 → ( ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ↔ ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ) )
40 39 ralbidv ⊢ ( 𝑂 = ∪ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ↔ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ) )
41 37 40 3anbi12d ⊢ ( 𝑂 = ∪ 𝑆 → ( ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ↔ ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
42 41 biimprd ⊢ ( 𝑂 = ∪ 𝑆 → ( ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) → ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
43 pwuni ⊢ 𝑆 ⊆ 𝒫 ∪ 𝑆
44 pweq ⊢ ( 𝑂 = ∪ 𝑆 → 𝒫 𝑂 = 𝒫 ∪ 𝑆 )
45 43 44 sseqtrrid ⊢ ( 𝑂 = ∪ 𝑆 → 𝑆 ⊆ 𝒫 𝑂 )
46 42 45 jctild ⊢ ( 𝑂 = ∪ 𝑆 → ( ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) → ( 𝑆 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) )
47 46 anim2d ⊢ ( 𝑂 = ∪ 𝑆 → ( ( 𝑆 ∈ V ∧ ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) → ( 𝑆 ∈ V ∧ ( 𝑆 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) ) )
48 4 biimpar ⊢ ( ( 𝑆 ∈ V ∧ ( 𝑆 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑂 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) ) → 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) )
49 36 47 48 syl56 ⊢ ( 𝑂 = ∪ 𝑆 → ( 𝑆 ∈ ∪ ran sigAlgebra → 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) ) )
50 49 impcom ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑂 = ∪ 𝑆 ) → 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) )
51 13 50 impbii ⊢ ( 𝑆 ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑂 = ∪ 𝑆 ) )