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 ⊢S∈⋃ran⁡sigAlgebra∧∀k∈ℕA∈S→⋃k∈ℕA∈S

Proof

Step Hyp Ref Expression
1 dfiun2g ⊢∀k∈ℕA∈S→⋃k∈ℕA=⋃x|∃k∈ℕx=A
2 1 adantl ⊢S∈⋃ran⁡sigAlgebra∧∀k∈ℕA∈S→⋃k∈ℕA=⋃x|∃k∈ℕx=A
3 simpl ⊢S∈⋃ran⁡sigAlgebra∧∀k∈ℕA∈S→S∈⋃ran⁡sigAlgebra
4 abid ⊢x∈x|∃k∈ℕx=A↔∃k∈ℕx=A
5 eleq1a ⊢A∈S→x=A→x∈S
6 5 ralimi ⊢∀k∈ℕA∈S→∀k∈ℕx=A→x∈S
7 r19.23v ⊢∀k∈ℕx=A→x∈S↔∃k∈ℕx=A→x∈S
8 6 7 sylib ⊢∀k∈ℕA∈S→∃k∈ℕx=A→x∈S
9 8 imp ⊢∀k∈ℕA∈S∧∃k∈ℕx=A→x∈S
10 9 adantll ⊢S∈⋃ran⁡sigAlgebra∧∀k∈ℕA∈S∧∃k∈ℕx=A→x∈S
11 4 10 sylan2b ⊢S∈⋃ran⁡sigAlgebra∧∀k∈ℕA∈S∧x∈x|∃k∈ℕx=A→x∈S
12 11 ralrimiva ⊢S∈⋃ran⁡sigAlgebra∧∀k∈ℕA∈S→∀x∈x|∃k∈ℕx=Ax∈S
13 nfab1 ⊢Ⅎ_xx|∃k∈ℕx=A
14 nfcv ⊢Ⅎ_xS
15 13 14 dfss3f ⊢x|∃k∈ℕx=A⊆S↔∀x∈x|∃k∈ℕx=Ax∈S
16 12 15 sylibr ⊢S∈⋃ran⁡sigAlgebra∧∀k∈ℕA∈S→x|∃k∈ℕx=A⊆S
17 elpw2g ⊢S∈⋃ran⁡sigAlgebra→x|∃k∈ℕx=A∈𝒫S↔x|∃k∈ℕx=A⊆S
18 17 adantr ⊢S∈⋃ran⁡sigAlgebra∧∀k∈ℕA∈S→x|∃k∈ℕx=A∈𝒫S↔x|∃k∈ℕx=A⊆S
19 16 18 mpbird ⊢S∈⋃ran⁡sigAlgebra∧∀k∈ℕA∈S→x|∃k∈ℕx=A∈𝒫S
20 nnct ⊢ℕ≼ω
21 abrexct ⊢ℕ≼ω→x|∃k∈ℕx=A≼ω
22 20 21 mp1i ⊢S∈⋃ran⁡sigAlgebra∧∀k∈ℕA∈S→x|∃k∈ℕx=A≼ω
23 sigaclcu ⊢S∈⋃ran⁡sigAlgebra∧x|∃k∈ℕx=A∈𝒫S∧x|∃k∈ℕx=A≼ω→⋃x|∃k∈ℕx=A∈S
24 3 19 22 23 syl3anc ⊢S∈⋃ran⁡sigAlgebra∧∀k∈ℕA∈S→⋃x|∃k∈ℕx=A∈S
25 2 24 eqeltrd ⊢S∈⋃ran⁡sigAlgebra∧∀k∈ℕA∈S→⋃k∈ℕA∈S