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 4 raleqdv ⊢ φ ∧ N = ℕ → ∀ k ∈ N A ∈ S ↔ ∀ k ∈ ℕ A ∈ S
10 8 9 mpbid ⊢ φ ∧ N = ℕ → ∀ k ∈ ℕ A ∈ S
11 sigaclcu2 ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ ∀ k ∈ ℕ A ∈ S → ⋃ k ∈ ℕ A ∈ S
12 6 10 11 syl2anc ⊢ φ ∧ N = ℕ → ⋃ k ∈ ℕ A ∈ S
13 5 12 eqeltrd ⊢ φ ∧ N = ℕ → ⋃ k ∈ N A ∈ S
14 simpr ⊢ φ ∧ N = 1 ..^ M → N = 1 ..^ M
15 14 iuneq1d ⊢ φ ∧ N = 1 ..^ M → ⋃ k ∈ N A = ⋃ k ∈ 1 ..^ M A
16 1 adantr ⊢ φ ∧ N = 1 ..^ M → S ∈ ⋃ ran ⁡ sigAlgebra
17 7 adantr ⊢ φ ∧ N = 1 ..^ M → ∀ k ∈ N A ∈ S
18 14 raleqdv ⊢ φ ∧ N = 1 ..^ M → ∀ k ∈ N A ∈ S ↔ ∀ k ∈ 1 ..^ M A ∈ S
19 17 18 mpbid ⊢ φ ∧ N = 1 ..^ M → ∀ k ∈ 1 ..^ M A ∈ S
20 sigaclfu2 ⊢ S ∈ ⋃ ran ⁡ sigAlgebra ∧ ∀ k ∈ 1 ..^ M A ∈ S → ⋃ k ∈ 1 ..^ M A ∈ S
21 16 19 20 syl2anc ⊢ φ ∧ N = 1 ..^ M → ⋃ k ∈ 1 ..^ M A ∈ S
22 15 21 eqeltrd ⊢ φ ∧ N = 1 ..^ M → ⋃ k ∈ N A ∈ S
23 13 22 2 mpjaodan ⊢ φ → ⋃ k ∈ N A ∈ S