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	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝑁 𝐴 ∈ 𝑆 )