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 ( 𝜑𝑆 ran sigAlgebra )
sigaclcu3.2 ( 𝜑 → ( 𝑁 = ℕ ∨ 𝑁 = ( 1 ..^ 𝑀 ) ) )
sigaclcu3.3 ( ( 𝜑𝑘𝑁 ) → 𝐴𝑆 )
Assertion sigaclcu3 ( 𝜑 𝑘𝑁 𝐴𝑆 )

Proof

Step Hyp Ref Expression
1 sigaclcu3.1 ( 𝜑𝑆 ran sigAlgebra )
2 sigaclcu3.2 ( 𝜑 → ( 𝑁 = ℕ ∨ 𝑁 = ( 1 ..^ 𝑀 ) ) )
3 sigaclcu3.3 ( ( 𝜑𝑘𝑁 ) → 𝐴𝑆 )
4 simpr ( ( 𝜑𝑁 = ℕ ) → 𝑁 = ℕ )
5 4 iuneq1d ( ( 𝜑𝑁 = ℕ ) → 𝑘𝑁 𝐴 = 𝑘 ∈ ℕ 𝐴 )
6 1 adantr ( ( 𝜑𝑁 = ℕ ) → 𝑆 ran sigAlgebra )
7 3 ralrimiva ( 𝜑 → ∀ 𝑘𝑁 𝐴𝑆 )
8 7 adantr ( ( 𝜑𝑁 = ℕ ) → ∀ 𝑘𝑁 𝐴𝑆 )
9 8 4 raleqtrdv ( ( 𝜑𝑁 = ℕ ) → ∀ 𝑘 ∈ ℕ 𝐴𝑆 )
10 sigaclcu2 ( ( 𝑆 ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ 𝐴𝑆 ) → 𝑘 ∈ ℕ 𝐴𝑆 )
11 6 9 10 syl2anc ( ( 𝜑𝑁 = ℕ ) → 𝑘 ∈ ℕ 𝐴𝑆 )
12 5 11 eqeltrd ( ( 𝜑𝑁 = ℕ ) → 𝑘𝑁 𝐴𝑆 )
13 simpr ( ( 𝜑𝑁 = ( 1 ..^ 𝑀 ) ) → 𝑁 = ( 1 ..^ 𝑀 ) )
14 13 iuneq1d ( ( 𝜑𝑁 = ( 1 ..^ 𝑀 ) ) → 𝑘𝑁 𝐴 = 𝑘 ∈ ( 1 ..^ 𝑀 ) 𝐴 )
15 1 adantr ( ( 𝜑𝑁 = ( 1 ..^ 𝑀 ) ) → 𝑆 ran sigAlgebra )
16 7 adantr ( ( 𝜑𝑁 = ( 1 ..^ 𝑀 ) ) → ∀ 𝑘𝑁 𝐴𝑆 )
17 16 13 raleqtrdv ( ( 𝜑𝑁 = ( 1 ..^ 𝑀 ) ) → ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) 𝐴𝑆 )
18 sigaclfu2 ( ( 𝑆 ran sigAlgebra ∧ ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) 𝐴𝑆 ) → 𝑘 ∈ ( 1 ..^ 𝑀 ) 𝐴𝑆 )
19 15 17 18 syl2anc ( ( 𝜑𝑁 = ( 1 ..^ 𝑀 ) ) → 𝑘 ∈ ( 1 ..^ 𝑀 ) 𝐴𝑆 )
20 14 19 eqeltrd ( ( 𝜑𝑁 = ( 1 ..^ 𝑀 ) ) → 𝑘𝑁 𝐴𝑆 )
21 12 20 2 mpjaodan ( 𝜑 𝑘𝑁 𝐴𝑆 )