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 )