Metamath Proof Explorer

Theorem intsal

Description: The arbitrary intersection of sigma-algebra (on the same set X ) is a sigma-algebra ( on the same set X , see intsaluni ). (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses intsal.ga ⊢ ( 𝜑 → 𝐺 ⊆ SAlg )
intsal.gn0 ⊢ ( 𝜑 → 𝐺 ≠ ∅ )
intsal.x ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ∪ 𝑠 = 𝑋 )
Assertion intsal ( 𝜑 → ∩ 𝐺 ∈ SAlg )

Proof

Step Hyp Ref Expression
1 intsal.ga ⊢ ( 𝜑 → 𝐺 ⊆ SAlg )
2 intsal.gn0 ⊢ ( 𝜑 → 𝐺 ≠ ∅ )
3 intsal.x ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ∪ 𝑠 = 𝑋 )
4 simpl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → 𝜑 )
5 1 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → 𝑠 ∈ SAlg )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ SAlg ) → 𝑠 ∈ SAlg )
7 0sal ⊢ ( 𝑠 ∈ SAlg → ∅ ∈ 𝑠 )
8 6 7 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ SAlg ) → ∅ ∈ 𝑠 )
9 4 5 8 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ∅ ∈ 𝑠 )
10 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝐺 ∅ ∈ 𝑠 )
11 0ex ⊢ ∅ ∈ V
12 11 elint2 ⊢ ( ∅ ∈ ∩ 𝐺 ↔ ∀ 𝑠 ∈ 𝐺 ∅ ∈ 𝑠 )
13 10 12 sylibr ⊢ ( 𝜑 → ∅ ∈ ∩ 𝐺 )
14 1 2 3 intsaluni ⊢ ( 𝜑 → ∪ ∩ 𝐺 = 𝑋 )
15 14 eqcomd ⊢ ( 𝜑 → 𝑋 = ∪ ∩ 𝐺 )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → 𝑋 = ∪ ∩ 𝐺 )
17 3 16 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ∪ ∩ 𝐺 = ∪ 𝑠 )
18 17 difeq1d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ( ∪ ∩ 𝐺 ∖ 𝑦 ) = ( ∪ 𝑠 ∖ 𝑦 ) )
19 18 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝐺 ) ∧ 𝑠 ∈ 𝐺 ) → ( ∪ ∩ 𝐺 ∖ 𝑦 ) = ( ∪ 𝑠 ∖ 𝑦 ) )
20 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝐺 ) ∧ 𝑠 ∈ 𝐺 ) → 𝑠 ∈ SAlg )
21 elinti ⊢ ( 𝑦 ∈ ∩ 𝐺 → ( 𝑠 ∈ 𝐺 → 𝑦 ∈ 𝑠 ) )
22 21 imp ⊢ ( ( 𝑦 ∈ ∩ 𝐺 ∧ 𝑠 ∈ 𝐺 ) → 𝑦 ∈ 𝑠 )
23 22 adantll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝐺 ) ∧ 𝑠 ∈ 𝐺 ) → 𝑦 ∈ 𝑠 )
24 saldifcl ⊢ ( ( 𝑠 ∈ SAlg ∧ 𝑦 ∈ 𝑠 ) → ( ∪ 𝑠 ∖ 𝑦 ) ∈ 𝑠 )
25 20 23 24 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝐺 ) ∧ 𝑠 ∈ 𝐺 ) → ( ∪ 𝑠 ∖ 𝑦 ) ∈ 𝑠 )
26 19 25 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝐺 ) ∧ 𝑠 ∈ 𝐺 ) → ( ∪ ∩ 𝐺 ∖ 𝑦 ) ∈ 𝑠 )
27 26 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝐺 ) → ∀ 𝑠 ∈ 𝐺 ( ∪ ∩ 𝐺 ∖ 𝑦 ) ∈ 𝑠 )
28 intex ⊢ ( 𝐺 ≠ ∅ ↔ ∩ 𝐺 ∈ V )
29 28 biimpi ⊢ ( 𝐺 ≠ ∅ → ∩ 𝐺 ∈ V )
30 2 29 syl ⊢ ( 𝜑 → ∩ 𝐺 ∈ V )
31 30 uniexd ⊢ ( 𝜑 → ∪ ∩ 𝐺 ∈ V )
32 31 difexd ⊢ ( 𝜑 → ( ∪ ∩ 𝐺 ∖ 𝑦 ) ∈ V )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝐺 ) → ( ∪ ∩ 𝐺 ∖ 𝑦 ) ∈ V )
34 elintg ⊢ ( ( ∪ ∩ 𝐺 ∖ 𝑦 ) ∈ V → ( ( ∪ ∩ 𝐺 ∖ 𝑦 ) ∈ ∩ 𝐺 ↔ ∀ 𝑠 ∈ 𝐺 ( ∪ ∩ 𝐺 ∖ 𝑦 ) ∈ 𝑠 ) )
35 33 34 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝐺 ) → ( ( ∪ ∩ 𝐺 ∖ 𝑦 ) ∈ ∩ 𝐺 ↔ ∀ 𝑠 ∈ 𝐺 ( ∪ ∩ 𝐺 ∖ 𝑦 ) ∈ 𝑠 ) )
36 27 35 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∩ 𝐺 ) → ( ∪ ∩ 𝐺 ∖ 𝑦 ) ∈ ∩ 𝐺 )
37 36 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ ∩ 𝐺 ( ∪ ∩ 𝐺 ∖ 𝑦 ) ∈ ∩ 𝐺 )
38 5 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺 ) ∧ 𝑦 ≼ ω ) ∧ 𝑠 ∈ 𝐺 ) → 𝑠 ∈ SAlg )
39 elpwi ⊢ ( 𝑦 ∈ 𝒫 ∩ 𝐺 → 𝑦 ⊆ ∩ 𝐺 )
40 39 adantr ⊢ ( ( 𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺 ) → 𝑦 ⊆ ∩ 𝐺 )
41 intss1 ⊢ ( 𝑠 ∈ 𝐺 → ∩ 𝐺 ⊆ 𝑠 )
42 41 adantl ⊢ ( ( 𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺 ) → ∩ 𝐺 ⊆ 𝑠 )
43 40 42 sstrd ⊢ ( ( 𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺 ) → 𝑦 ⊆ 𝑠 )
44 vex ⊢ 𝑦 ∈ V
45 44 elpw ⊢ ( 𝑦 ∈ 𝒫 𝑠 ↔ 𝑦 ⊆ 𝑠 )
46 43 45 sylibr ⊢ ( ( 𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺 ) → 𝑦 ∈ 𝒫 𝑠 )
47 46 adantll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺 ) ∧ 𝑠 ∈ 𝐺 ) → 𝑦 ∈ 𝒫 𝑠 )
48 47 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺 ) ∧ 𝑦 ≼ ω ) ∧ 𝑠 ∈ 𝐺 ) → 𝑦 ∈ 𝒫 𝑠 )
49 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺 ) ∧ 𝑦 ≼ ω ) ∧ 𝑠 ∈ 𝐺 ) → 𝑦 ≼ ω )
50 38 48 49 salunicl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺 ) ∧ 𝑦 ≼ ω ) ∧ 𝑠 ∈ 𝐺 ) → ∪ 𝑦 ∈ 𝑠 )
51 50 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺 ) ∧ 𝑦 ≼ ω ) → ∀ 𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠 )
52 vuniex ⊢ ∪ 𝑦 ∈ V
53 52 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺 ) ∧ 𝑦 ≼ ω ) → ∪ 𝑦 ∈ V )
54 elintg ⊢ ( ∪ 𝑦 ∈ V → ( ∪ 𝑦 ∈ ∩ 𝐺 ↔ ∀ 𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠 ) )
55 53 54 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺 ) ∧ 𝑦 ≼ ω ) → ( ∪ 𝑦 ∈ ∩ 𝐺 ↔ ∀ 𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠 ) )
56 51 55 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺 ) ∧ 𝑦 ≼ ω ) → ∪ 𝑦 ∈ ∩ 𝐺 )
57 56 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺 ) → ( 𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺 ) )
58 57 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 ∩ 𝐺 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺 ) )
59 13 37 58 3jca ⊢ ( 𝜑 → ( ∅ ∈ ∩ 𝐺 ∧ ∀ 𝑦 ∈ ∩ 𝐺 ( ∪ ∩ 𝐺 ∖ 𝑦 ) ∈ ∩ 𝐺 ∧ ∀ 𝑦 ∈ 𝒫 ∩ 𝐺 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺 ) ) )
60 issal ⊢ ( ∩ 𝐺 ∈ V → ( ∩ 𝐺 ∈ SAlg ↔ ( ∅ ∈ ∩ 𝐺 ∧ ∀ 𝑦 ∈ ∩ 𝐺 ( ∪ ∩ 𝐺 ∖ 𝑦 ) ∈ ∩ 𝐺 ∧ ∀ 𝑦 ∈ 𝒫 ∩ 𝐺 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺 ) ) ) )
61 30 60 syl ⊢ ( 𝜑 → ( ∩ 𝐺 ∈ SAlg ↔ ( ∅ ∈ ∩ 𝐺 ∧ ∀ 𝑦 ∈ ∩ 𝐺 ( ∪ ∩ 𝐺 ∖ 𝑦 ) ∈ ∩ 𝐺 ∧ ∀ 𝑦 ∈ 𝒫 ∩ 𝐺 ( 𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺 ) ) ) )
62 59 61 mpbird ⊢ ( 𝜑 → ∩ 𝐺 ∈ SAlg )