Metamath Proof Explorer

Theorem sigaclcu3

Description: A sigma-algebra is closed under countable or finite union. (Contributed by Thierry Arnoux, 6-Mar-2017)

Ref Expression
Hypotheses sigaclcu3.1 ⊢ φ → S ∈ ⋃ ran ⁡ sigAlgebra
sigaclcu3.2 ⊢ φ → N = ℕ ∨ N = 1 ..^ M
sigaclcu3.3 ⊢ φ ∧ k ∈ N → A ∈ S
Assertion sigaclcu3 ⊢ φ → ⋃ k ∈ N A ∈ S

Proof

Step Hyp Ref Expression
1 sigaclcu3.1 ⊢ φ → S ∈ ⋃ ran ⁡ sigAlgebra
2 sigaclcu3.2 ⊢ φ → N = ℕ ∨ N = 1 ..^ M
3 sigaclcu3.3 ⊢ φ ∧ k ∈ N → A ∈ S
4 simpr ⊢ φ ∧ N = ℕ → N = ℕ
5 4 iuneq1d ⊢ φ ∧ N = ℕ → ⋃ k ∈ N A = ⋃ k ∈ ℕ A
6 1 adantr ⊢ φ ∧ N = ℕ → S ∈ ⋃ ran ⁡ sigAlgebra
7 3 ralrimiva ⊢ φ → ∀ k ∈ N A ∈ S
8 7 adantr ⊢ φ ∧ N = ℕ → ∀ k ∈ N A ∈ S
9 8 4 raleqtrdv ⊢ φ ∧ N = ℕ → ∀ k ∈ ℕ A ∈ S
10 sigaclcu2 ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ ∀ k ∈ ℕ A ∈ S → ⋃ k ∈ ℕ A ∈ S
11 6 9 10 syl2anc ⊢ φ ∧ N = ℕ → ⋃ k ∈ ℕ A ∈ S
12 5 11 eqeltrd ⊢ φ ∧ N = ℕ → ⋃ k ∈ N A ∈ S
13 simpr ⊢ φ ∧ N = 1 ..^ M → N = 1 ..^ M
14 13 iuneq1d ⊢ φ ∧ N = 1 ..^ M → ⋃ k ∈ N A = ⋃ k ∈ 1 ..^ M A
15 1 adantr ⊢ φ ∧ N = 1 ..^ M → S ∈ ⋃ ran ⁡ sigAlgebra
16 7 adantr ⊢ φ ∧ N = 1 ..^ M → ∀ k ∈ N A ∈ S
17 16 13 raleqtrdv ⊢ φ ∧ N = 1 ..^ M → ∀ k ∈ 1 ..^ M A ∈ S
18 sigaclfu2 ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ ∀ k ∈ 1 ..^ M A ∈ S → ⋃ k ∈ 1 ..^ M A ∈ S
19 15 17 18 syl2anc ⊢ φ ∧ N = 1 ..^ M → ⋃ k ∈ 1 ..^ M A ∈ S
20 14 19 eqeltrd ⊢ φ ∧ N = 1 ..^ M → ⋃ k ∈ N A ∈ S
21 12 20 2 mpjaodan ⊢ φ → ⋃ k ∈ N A ∈ S