Metamath Proof Explorer

Theorem sigaclcu2

Description: A sigma-algebra is closed under countable union - indexing on NN (Contributed by Thierry Arnoux, 29-Dec-2016)

Ref Expression
Assertion sigaclcu2 ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ) → ∪ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 dfiun2g ⊢ ( ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 → ∪ 𝑘 ∈ ℕ 𝐴 = ∪ { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } )
2 1 adantl ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ) → ∪ 𝑘 ∈ ℕ 𝐴 = ∪ { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } )
3 simpl ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ) → 𝑆 ∈ ∪ ran sigAlgebra )
4 abid ⊢ ( 𝑥 ∈ { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ↔ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 )
5 eleq1a ⊢ ( 𝐴 ∈ 𝑆 → ( 𝑥 = 𝐴 → 𝑥 ∈ 𝑆 ) )
6 5 ralimi ⊢ ( ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 → ∀ 𝑘 ∈ ℕ ( 𝑥 = 𝐴 → 𝑥 ∈ 𝑆 ) )
7 r19.23v ⊢ ( ∀ 𝑘 ∈ ℕ ( 𝑥 = 𝐴 → 𝑥 ∈ 𝑆 ) ↔ ( ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 → 𝑥 ∈ 𝑆 ) )
8 6 7 sylib ⊢ ( ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 → ( ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 → 𝑥 ∈ 𝑆 ) )
9 8 imp ⊢ ( ( ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ∧ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 ) → 𝑥 ∈ 𝑆 )
10 9 adantll ⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ) ∧ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 ) → 𝑥 ∈ 𝑆 )
11 4 10 sylan2b ⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ) ∧ 𝑥 ∈ { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ) → 𝑥 ∈ 𝑆 )
12 11 ralrimiva ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ) → ∀ 𝑥 ∈ { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } 𝑥 ∈ 𝑆 )
13 nfab1 ⊢ Ⅎ 𝑥 { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 }
14 nfcv ⊢ Ⅎ 𝑥 𝑆
15 13 14 dfss3f ⊢ ( { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ⊆ 𝑆 ↔ ∀ 𝑥 ∈ { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } 𝑥 ∈ 𝑆 )
16 12 15 sylibr ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ) → { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ⊆ 𝑆 )
17 elpw2g ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ∈ 𝒫 𝑆 ↔ { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ⊆ 𝑆 ) )
18 17 adantr ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ) → ( { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ∈ 𝒫 𝑆 ↔ { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ⊆ 𝑆 ) )
19 16 18 mpbird ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ) → { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ∈ 𝒫 𝑆 )
20 nnct ⊢ ℕ ≼ ω
21 abrexct ⊢ ( ℕ ≼ ω → { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ≼ ω )
22 20 21 mp1i ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ) → { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ≼ ω )
23 sigaclcu ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ∈ 𝒫 𝑆 ∧ { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ≼ ω ) → ∪ { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ∈ 𝑆 )
24 3 19 22 23 syl3anc ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ) → ∪ { 𝑥 ∣ ∃ 𝑘 ∈ ℕ 𝑥 = 𝐴 } ∈ 𝑆 )
25 2 24 eqeltrd ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ) → ∪ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 )