Metamath Proof Explorer

Theorem insiga

Description: The intersection of a collection of sigma-algebras of same base is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016)

Ref Expression
Assertion insiga ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ∩ 𝐴 ∈ ( sigAlgebra ‘ 𝑂 ) )

Proof

Step Hyp Ref Expression
1 intex ⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V )
2 1 birani ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ∩ 𝐴 ∈ V )
3 intssuni ⊢ ( 𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴 )
4 3 adantr ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ∩ 𝐴 ⊆ ∪ 𝐴 )
5 simpr ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) )
6 elpwi ⊢ ( 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) → 𝐴 ⊆ ( sigAlgebra ‘ 𝑂 ) )
7 sigasspw ⊢ ( 𝑠 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑠 ⊆ 𝒫 𝑂 )
8 velpw ⊢ ( 𝑠 ∈ 𝒫 𝒫 𝑂 ↔ 𝑠 ⊆ 𝒫 𝑂 )
9 7 8 sylibr ⊢ ( 𝑠 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑠 ∈ 𝒫 𝒫 𝑂 )
10 9 ssriv ⊢ ( sigAlgebra ‘ 𝑂 ) ⊆ 𝒫 𝒫 𝑂
11 6 10 sstrdi ⊢ ( 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) → 𝐴 ⊆ 𝒫 𝒫 𝑂 )
12 5 11 syl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → 𝐴 ⊆ 𝒫 𝒫 𝑂 )
13 sspwuni ⊢ ( 𝐴 ⊆ 𝒫 𝒫 𝑂 ↔ ∪ 𝐴 ⊆ 𝒫 𝑂 )
14 12 13 sylib ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ∪ 𝐴 ⊆ 𝒫 𝑂 )
15 4 14 sstrd ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ∩ 𝐴 ⊆ 𝒫 𝑂 )
16 simpr ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ 𝐴 )
17 simplr ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑠 ∈ 𝐴 ) → 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) )
18 elelpwi ⊢ ( ( 𝑠 ∈ 𝐴 ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → 𝑠 ∈ ( sigAlgebra ‘ 𝑂 ) )
19 16 17 18 syl2anc ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ( sigAlgebra ‘ 𝑂 ) )
20 vex ⊢ 𝑠 ∈ V
21 issiga ⊢ ( 𝑠 ∈ V → ( 𝑠 ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( 𝑠 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) ) )
22 20 21 ax-mp ⊢ ( 𝑠 ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( 𝑠 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) )
23 19 22 sylib ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑠 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) ) )
24 23 simprd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑂 ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) ) )
25 24 simp1d ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑠 ∈ 𝐴 ) → 𝑂 ∈ 𝑠 )
26 25 ralrimiva ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ∀ 𝑠 ∈ 𝐴 𝑂 ∈ 𝑠 )
27 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑠 𝑠 ∈ 𝐴 )
28 27 birani ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ∃ 𝑠 𝑠 ∈ 𝐴 )
29 19 ex ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ( 𝑠 ∈ 𝐴 → 𝑠 ∈ ( sigAlgebra ‘ 𝑂 ) ) )
30 29 eximdv ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ( ∃ 𝑠 𝑠 ∈ 𝐴 → ∃ 𝑠 𝑠 ∈ ( sigAlgebra ‘ 𝑂 ) ) )
31 28 30 mpd ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ∃ 𝑠 𝑠 ∈ ( sigAlgebra ‘ 𝑂 ) )
32 elfvex ⊢ ( 𝑠 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑂 ∈ V )
33 32 exlimiv ⊢ ( ∃ 𝑠 𝑠 ∈ ( sigAlgebra ‘ 𝑂 ) → 𝑂 ∈ V )
34 31 33 syl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → 𝑂 ∈ V )
35 elintg ⊢ ( 𝑂 ∈ V → ( 𝑂 ∈ ∩ 𝐴 ↔ ∀ 𝑠 ∈ 𝐴 𝑂 ∈ 𝑠 ) )
36 34 35 syl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ( 𝑂 ∈ ∩ 𝐴 ↔ ∀ 𝑠 ∈ 𝐴 𝑂 ∈ 𝑠 ) )
37 26 36 mpbird ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → 𝑂 ∈ ∩ 𝐴 )
38 simpll ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) )
39 simpr ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ 𝐴 )
40 38 39 jca ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑠 ∈ 𝐴 ) )
41 elinti ⊢ ( 𝑥 ∈ ∩ 𝐴 → ( 𝑠 ∈ 𝐴 → 𝑥 ∈ 𝑠 ) )
42 41 imp ⊢ ( ( 𝑥 ∈ ∩ 𝐴 ∧ 𝑠 ∈ 𝐴 ) → 𝑥 ∈ 𝑠 )
43 42 adantll ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → 𝑥 ∈ 𝑠 )
44 24 simp2d ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑠 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 )
45 44 r19.21bi ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝑠 ) → ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 )
46 40 43 45 syl2anc ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 )
47 46 ralrimiva ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ ∩ 𝐴 ) → ∀ 𝑠 ∈ 𝐴 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 )
48 34 difexd ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ( 𝑂 ∖ 𝑥 ) ∈ V )
49 48 adantr ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ ∩ 𝐴 ) → ( 𝑂 ∖ 𝑥 ) ∈ V )
50 elintg ⊢ ( ( 𝑂 ∖ 𝑥 ) ∈ V → ( ( 𝑂 ∖ 𝑥 ) ∈ ∩ 𝐴 ↔ ∀ 𝑠 ∈ 𝐴 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ) )
51 49 50 syl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ ∩ 𝐴 ) → ( ( 𝑂 ∖ 𝑥 ) ∈ ∩ 𝐴 ↔ ∀ 𝑠 ∈ 𝐴 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ) )
52 47 51 mpbird ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ ∩ 𝐴 ) → ( 𝑂 ∖ 𝑥 ) ∈ ∩ 𝐴 )
53 52 ralrimiva ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ∀ 𝑥 ∈ ∩ 𝐴 ( 𝑂 ∖ 𝑥 ) ∈ ∩ 𝐴 )
54 simplll ⊢ ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴 ) ∧ 𝑥 ≼ ω ) ∧ 𝑠 ∈ 𝐴 ) → ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) )
55 simpr ⊢ ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴 ) ∧ 𝑥 ≼ ω ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ 𝐴 )
56 54 55 jca ⊢ ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴 ) ∧ 𝑥 ≼ ω ) ∧ 𝑠 ∈ 𝐴 ) → ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑠 ∈ 𝐴 ) )
57 simpllr ⊢ ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴 ) ∧ 𝑥 ≼ ω ) ∧ 𝑠 ∈ 𝐴 ) → 𝑥 ∈ 𝒫 ∩ 𝐴 )
58 elpwi ⊢ ( 𝑥 ∈ 𝒫 ∩ 𝐴 → 𝑥 ⊆ ∩ 𝐴 )
59 intss1 ⊢ ( 𝑠 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑠 )
60 58 59 sylan9ss ⊢ ( ( 𝑥 ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴 ) → 𝑥 ⊆ 𝑠 )
61 velpw ⊢ ( 𝑥 ∈ 𝒫 𝑠 ↔ 𝑥 ⊆ 𝑠 )
62 60 61 sylibr ⊢ ( ( 𝑥 ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴 ) → 𝑥 ∈ 𝒫 𝑠 )
63 57 62 sylancom ⊢ ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴 ) ∧ 𝑥 ≼ ω ) ∧ 𝑠 ∈ 𝐴 ) → 𝑥 ∈ 𝒫 𝑠 )
64 56 63 jca ⊢ ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴 ) ∧ 𝑥 ≼ ω ) ∧ 𝑠 ∈ 𝐴 ) → ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝒫 𝑠 ) )
65 simplr ⊢ ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴 ) ∧ 𝑥 ≼ ω ) ∧ 𝑠 ∈ 𝐴 ) → 𝑥 ≼ ω )
66 24 simp3d ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑠 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝒫 𝑠 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) )
67 66 r19.21bi ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝒫 𝑠 ) → ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠 ) )
68 64 65 67 sylc ⊢ ( ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴 ) ∧ 𝑥 ≼ ω ) ∧ 𝑠 ∈ 𝐴 ) → ∪ 𝑥 ∈ 𝑠 )
69 68 ralrimiva ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴 ) ∧ 𝑥 ≼ ω ) → ∀ 𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠 )
70 uniexg ⊢ ( 𝑥 ∈ 𝒫 ∩ 𝐴 → ∪ 𝑥 ∈ V )
71 70 ad2antlr ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴 ) ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ V )
72 elintg ⊢ ( ∪ 𝑥 ∈ V → ( ∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀ 𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠 ) )
73 71 72 syl ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴 ) ∧ 𝑥 ≼ ω ) → ( ∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀ 𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠 ) )
74 69 73 mpbird ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴 ) ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ ∩ 𝐴 )
75 74 ex ⊢ ( ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴 ) → ( 𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴 ) )
76 75 ralrimiva ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ∀ 𝑥 ∈ 𝒫 ∩ 𝐴 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴 ) )
77 37 53 76 3jca ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ( 𝑂 ∈ ∩ 𝐴 ∧ ∀ 𝑥 ∈ ∩ 𝐴 ( 𝑂 ∖ 𝑥 ) ∈ ∩ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 ∩ 𝐴 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴 ) ) )
78 issiga ⊢ ( ∩ 𝐴 ∈ V → ( ∩ 𝐴 ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( ∩ 𝐴 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ ∩ 𝐴 ∧ ∀ 𝑥 ∈ ∩ 𝐴 ( 𝑂 ∖ 𝑥 ) ∈ ∩ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 ∩ 𝐴 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴 ) ) ) ) )
79 78 biimpar ⊢ ( ( ∩ 𝐴 ∈ V ∧ ( ∩ 𝐴 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ ∩ 𝐴 ∧ ∀ 𝑥 ∈ ∩ 𝐴 ( 𝑂 ∖ 𝑥 ) ∈ ∩ 𝐴 ∧ ∀ 𝑥 ∈ 𝒫 ∩ 𝐴 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴 ) ) ) ) → ∩ 𝐴 ∈ ( sigAlgebra ‘ 𝑂 ) )
80 2 15 77 79 syl12anc ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 ( sigAlgebra ‘ 𝑂 ) ) → ∩ 𝐴 ∈ ( sigAlgebra ‘ 𝑂 ) )