Metamath Proof Explorer

Theorem sigaclcuni

Description: A sigma-algebra is closed under countable union: indexed union version. (Contributed by Thierry Arnoux, 8-Jun-2017)

Ref Expression
Hypothesis sigaclcuni.1 ⊢ Ⅎ _ k A
Assertion sigaclcuni ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ ∀ k ∈ A B ∈ S ∧ A ≼ ω → ⋃ k ∈ A B ∈ S

Proof

Step Hyp Ref Expression
1 sigaclcuni.1 ⊢ Ⅎ _ k A
2 dfiun2g ⊢ ∀ k ∈ A B ∈ S → ⋃ k ∈ A B = ⋃ z | ∃ k ∈ A z = B
3 2 3ad2ant2 ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ ∀ k ∈ A B ∈ S ∧ A ≼ ω → ⋃ k ∈ A B = ⋃ z | ∃ k ∈ A z = B
4 simp1 ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ ∀ k ∈ A B ∈ S ∧ A ≼ ω → S ∈ ⋃ ran ⁡ sigAlgebra
5 r19.29 ⊢ ∀ k ∈ A B ∈ S ∧ ∃ k ∈ A z = B → ∃ k ∈ A B ∈ S ∧ z = B
6 simpr ⊢ B ∈ S ∧ z = B → z = B
7 simpl ⊢ B ∈ S ∧ z = B → B ∈ S
8 6 7 eqeltrd ⊢ B ∈ S ∧ z = B → z ∈ S
9 8 rexlimivw ⊢ ∃ k ∈ A B ∈ S ∧ z = B → z ∈ S
10 5 9 syl ⊢ ∀ k ∈ A B ∈ S ∧ ∃ k ∈ A z = B → z ∈ S
11 10 ex ⊢ ∀ k ∈ A B ∈ S → ∃ k ∈ A z = B → z ∈ S
12 11 abssdv ⊢ ∀ k ∈ A B ∈ S → z | ∃ k ∈ A z = B ⊆ S
13 12 3ad2ant2 ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ ∀ k ∈ A B ∈ S ∧ A ≼ ω → z | ∃ k ∈ A z = B ⊆ S
14 elpw2g ⊢ S ∈ ⋃ ran ⁡ sigAlgebra → z | ∃ k ∈ A z = B ∈ 𝒫 S ↔ z | ∃ k ∈ A z = B ⊆ S
15 4 14 syl ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ ∀ k ∈ A B ∈ S ∧ A ≼ ω → z | ∃ k ∈ A z = B ∈ 𝒫 S ↔ z | ∃ k ∈ A z = B ⊆ S
16 13 15 mpbird ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ ∀ k ∈ A B ∈ S ∧ A ≼ ω → z | ∃ k ∈ A z = B ∈ 𝒫 S
17 1 abrexctf ⊢ A ≼ ω → z | ∃ k ∈ A z = B ≼ ω
18 17 3ad2ant3 ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ ∀ k ∈ A B ∈ S ∧ A ≼ ω → z | ∃ k ∈ A z = B ≼ ω
19 sigaclcu ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ z | ∃ k ∈ A z = B ∈ 𝒫 S ∧ z | ∃ k ∈ A z = B ≼ ω → ⋃ z | ∃ k ∈ A z = B ∈ S
20 4 16 18 19 syl3anc ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ ∀ k ∈ A B ∈ S ∧ A ≼ ω → ⋃ z | ∃ k ∈ A z = B ∈ S
21 3 20 eqeltrd ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ ∀ k ∈ A B ∈ S ∧ A ≼ ω → ⋃ k ∈ A B ∈ S