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