Metamath Proof Explorer

Theorem sigaclci

Description: A sigma-algebra is closed under countable intersections. Deduction version. The proof uses abrexct rather than abrexdom2jm , and so does not require ax-ac . (Contributed by Thierry Arnoux, 19-Sep-2016) (Revised by Vincent Gonzalez, 19-Aug-2026)

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 abrexct ⊢ ( 𝐴 ≼ ω → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ ω )
25 24 adantl ⊢ ( ( 𝐴 ∈ 𝒫 𝑆 ∧ 𝐴 ≼ ω ) → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ ω )
26 25 ex ⊢ ( 𝐴 ∈ 𝒫 𝑆 → ( 𝐴 ≼ ω → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ ω ) )
27 26 adantl ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( 𝐴 ≼ ω → { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ ω ) )
28 breq1 ⊢ ( 𝑥 = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } → ( 𝑥 ≼ ω ↔ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ ω ) )
29 unieq ⊢ ( 𝑥 = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } → ∪ 𝑥 = ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } )
30 29 eleq1d ⊢ ( 𝑥 = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } → ( ∪ 𝑥 ∈ 𝑆 ↔ ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝑆 ) )
31 28 30 imbi12d ⊢ ( 𝑥 = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } → ( ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ↔ ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ ω → ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝑆 ) ) )
32 31 rspcva ⊢ ( ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝒫 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) → ( { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ≼ ω → ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝑆 ) )
33 23 27 32 sylsyld ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( 𝐴 ≼ ω → ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝑆 ) )
34 5 adantl ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → 𝐴 ⊆ 𝑆 )
35 11 adantr ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ∀ 𝑧 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 )
36 ssralv ⊢ ( 𝐴 ⊆ 𝑆 → ( ∀ 𝑧 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 → ∀ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 ) )
37 34 35 36 sylc ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ∀ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 )
38 dfiun2g ⊢ ( ∀ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 → ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) = ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } )
39 eleq1 ⊢ ( ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) = ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } → ( ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 ↔ ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝑆 ) )
40 37 38 39 3syl ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 ↔ ∪ { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 = ( ∪ 𝑆 ∖ 𝑧 ) } ∈ 𝑆 ) )
41 33 40 sylibrd ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( 𝐴 ≼ ω → ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 ) )
42 difeq2 ⊢ ( 𝑥 = ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) → ( ∪ 𝑆 ∖ 𝑥 ) = ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) )
43 42 eleq1d ⊢ ( 𝑥 = ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) → ( ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ↔ ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 ) )
44 43 rspccv ⊢ ( ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 → ( ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ∈ 𝑆 → ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 ) )
45 4 41 44 sylsyld ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( 𝐴 ≼ ω → ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 ) )
46 45 adantrd ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 ) )
47 46 imp ⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) ∧ ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) ) → ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 )
48 simpr ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → 𝐴 ∈ 𝒫 𝑆 )
49 pwuni ⊢ 𝑆 ⊆ 𝒫 ∪ 𝑆
50 5 49 sstrdi ⊢ ( 𝐴 ∈ 𝒫 𝑆 → 𝐴 ⊆ 𝒫 ∪ 𝑆 )
51 iundifdifd ⊢ ( 𝐴 ⊆ 𝒫 ∪ 𝑆 → ( 𝐴 ≠ ∅ → ∩ 𝐴 = ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ) )
52 48 50 51 3syl ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( 𝐴 ≠ ∅ → ∩ 𝐴 = ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ) )
53 52 adantld ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 = ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ) )
54 eleq1 ⊢ ( ∩ 𝐴 = ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) → ( ∩ 𝐴 ∈ 𝑆 ↔ ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 ) )
55 53 54 syl6 ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) → ( ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) → ( ∩ 𝐴 ∈ 𝑆 ↔ ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 ) ) )
56 55 imp ⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) ∧ ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) ) → ( ∩ 𝐴 ∈ 𝑆 ↔ ( ∪ 𝑆 ∖ ∪ 𝑧 ∈ 𝐴 ( ∪ 𝑆 ∖ 𝑧 ) ) ∈ 𝑆 ) )
57 47 56 mpbird ⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ 𝒫 𝑆 ) ∧ ( 𝐴 ≼ ω ∧ 𝐴 ≠ ∅ ) ) → ∩ 𝐴 ∈ 𝑆 )