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 = A x ∈ S
13 nfab1 ⊢ Ⅎ _ x x | ∃ k ∈ ℕ x = A
14 nfcv ⊢ Ⅎ _ x S
15 13 14 dfss3f ⊢ x | ∃ k ∈ ℕ x = A ⊆ S ↔ ∀ x ∈ x | ∃ k ∈ ℕ x = A x ∈ 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