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