Metamath Proof Explorer

Theorem sigaclci

Description: A sigma-algebra is closed under countable intersections. Deduction version. (Contributed by Thierry Arnoux, 19-Sep-2016)

Ref Expression
Assertion sigaclci ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) ∧ ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) ) → ∩ 𝐴 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 isrnsigau ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
2 1 simprd ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) )
3 2 simp2d ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 )
4 3 adantr ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 )
5 elpwi ⊢ ( 𝐴 ∈ 𝒫 𝑆 → 𝐴 ⊆ 𝑆 )
6 ssrexv ⊢ ( 𝐴 ⊆ 𝑆 → ( ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) → ∃ 𝑧 ∈ 𝑆 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) ) )
7 5 6 syl ⊢ ( 𝐴 ∈ 𝒫 𝑆 → ( ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) → ∃ 𝑧 ∈ 𝑆 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) ) )
8 7 ss2abdv ⊢ ( 𝐴 ∈ 𝒫 𝑆 → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ⊆ { 𝑦 ∣ ∃ 𝑧 ∈ 𝑆 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } )
9 isrnsigau ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ≼ ω → ∪ 𝑧 ∈ 𝑆 ) ) ) )
10 9 simprd ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ≼ ω → ∪ 𝑧 ∈ 𝑆 ) ) )
11 10 simp2d ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∀ 𝑧 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 )
12 uniiunlem ⊢ ( ∀ 𝑧 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 → ( ∀ 𝑧 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 ↔ { 𝑦 ∣ ∃ 𝑧 ∈ 𝑆 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ⊆ 𝑆 ) )
13 11 12 syl ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ∀ 𝑧 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 ↔ { 𝑦 ∣ ∃ 𝑧 ∈ 𝑆 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ⊆ 𝑆 ) )
14 11 13 mpbid ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → { 𝑦 ∣ ∃ 𝑧 ∈ 𝑆 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ⊆ 𝑆 )
15 8 14 sylan9ssr ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ⊆ 𝑆 )
16 abrexexg ⊢ ( 𝐴 ∈ 𝒫 𝑆 → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ V )
17 elpwg ⊢ ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ V → ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝒫 𝑆 ↔ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ⊆ 𝑆 ) )
18 16 17 syl ⊢ ( 𝐴 ∈ 𝒫 𝑆 → ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝒫 𝑆 ↔ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ⊆ 𝑆 ) )
19 18 adantl ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝒫 𝑆 ↔ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ⊆ 𝑆 ) )
20 15 19 mpbird ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝒫 𝑆 )
21 2 simp3d ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) )
22 21 adantr ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) )
23 20 22 jca ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝒫 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) )
24 abrexdom2jm ⊢ ( 𝐴 ∈ 𝒫 𝑆 → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ 𝐴 )
25 domtr ⊢ ( ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ 𝐴 ∧ 𝐴 ≼ ω ) → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ ω )
26 24 25 sylan ⊢ ( ( 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω ) → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ ω )
27 26 ex ⊢ ( 𝐴 ∈ 𝒫 𝑆 → ( 𝐴 ≼ ω → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ ω ) )
28 27 adantl ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( 𝐴 ≼ ω → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ ω ) )
29 breq1 ⊢ ( 𝑥 = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } → ( 𝑥 ≼ ω ↔ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ ω ) )
30 unieq ⊢ ( 𝑥 = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } → ∪ 𝑥 = ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } )
31 30 eleq1d ⊢ ( 𝑥 = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } → ( ∪ 𝑥 ∈ 𝑆 ↔ ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝑆 ) )
32 29 31 imbi12d ⊢ ( 𝑥 = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } → ( ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ↔ ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ ω → ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝑆 ) ) )
33 32 rspcva ⊢ ( ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝒫 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) → ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ ω → ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝑆 ) )
34 23 28 33 sylsyld ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( 𝐴 ≼ ω → ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝑆 ) )
35 5 adantl ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → 𝐴 ⊆ 𝑆 )
36 11 adantr ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ∀ 𝑧 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 )
37 ssralv ⊢ ( 𝐴 ⊆ 𝑆 → ( ∀ 𝑧 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 → ∀ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 ) )
38 35 36 37 sylc ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ∀ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 )
39 dfiun2g ⊢ ( ∀ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 → ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) = ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } )
40 eleq1 ⊢ ( ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) = ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } → ( ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 ↔ ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝑆 ) )
41 38 39 40 3syl ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 ↔ ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝑆 ) )
42 34 41 sylibrd ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( 𝐴 ≼ ω → ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 ) )
43 difeq2 ⊢ ( 𝑥 = ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) → ( ∪ 𝑆 ∖ 𝑥 ) = ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) )
44 43 eleq1d ⊢ ( 𝑥 = ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) → ( ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ↔ ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 ) )
45 44 rspccv ⊢ ( ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 → ( ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 → ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 ) )
46 4 42 45 sylsyld ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( 𝐴 ≼ ω → ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 ) )
47 46 adantrd ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 ) )
48 47 imp ⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) ∧ ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) ) → ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 )
49 simpr ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → 𝐴 ∈ 𝒫 𝑆 )
50 pwuni ⊢ 𝑆 ⊆ 𝒫 ∪ 𝑆
51 5 50 sstrdi ⊢ ( 𝐴 ∈ 𝒫 𝑆 → 𝐴 ⊆ 𝒫 ∪ 𝑆 )
52 iundifdifd ⊢ ( 𝐴 ⊆ 𝒫 ∪ 𝑆 → ( 𝐴 ≠ ∅ → ∩ 𝐴 = ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ) )
53 49 51 52 3syl ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( 𝐴 ≠ ∅ → ∩ 𝐴 = ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ) )
54 53 adantld ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 = ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ) )
55 eleq1 ⊢ ( ∩ 𝐴 = ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) → ( ∩ 𝐴 ∈ 𝑆 ↔ ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 ) )
56 54 55 syl6 ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ( ∩ 𝐴 ∈ 𝑆 ↔ ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 ) ) )
57 56 imp ⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) ∧ ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) ) → ( ∩ 𝐴 ∈ 𝑆 ↔ ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 ) )
58 48 57 mpbird ⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) ∧ ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) ) → ∩ 𝐴 ∈ 𝑆 )