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	4	raleqdv	⊢ ( ( 𝜑 ∧ 𝑁 = ℕ ) → ( ∀ 𝑘 ∈ 𝑁 𝐴 ∈ 𝑆 ↔ ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ) )
10	8 9	mpbid	⊢ ( ( 𝜑 ∧ 𝑁 = ℕ ) → ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 )
11		sigaclcu2	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 ) → ∪ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 )
12	6 10 11	syl2anc	⊢ ( ( 𝜑 ∧ 𝑁 = ℕ ) → ∪ 𝑘 ∈ ℕ 𝐴 ∈ 𝑆 )
13	5 12	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑁 = ℕ ) → ∪ 𝑘 ∈ 𝑁 𝐴 ∈ 𝑆 )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑁 = ( 1 ..^ 𝑀 ) ) → 𝑁 = ( 1 ..^ 𝑀 ) )
15	14	iuneq1d	⊢ ( ( 𝜑 ∧ 𝑁 = ( 1 ..^ 𝑀 ) ) → ∪ 𝑘 ∈ 𝑁 𝐴 = ∪ 𝑘 ∈ ( 1 ..^ 𝑀 ) 𝐴 )
16	1	adantr	⊢ ( ( 𝜑 ∧ 𝑁 = ( 1 ..^ 𝑀 ) ) → 𝑆 ∈ ∪ ran sigAlgebra )
17	7	adantr	⊢ ( ( 𝜑 ∧ 𝑁 = ( 1 ..^ 𝑀 ) ) → ∀ 𝑘 ∈ 𝑁 𝐴 ∈ 𝑆 )
18	14	raleqdv	⊢ ( ( 𝜑 ∧ 𝑁 = ( 1 ..^ 𝑀 ) ) → ( ∀ 𝑘 ∈ 𝑁 𝐴 ∈ 𝑆 ↔ ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) 𝐴 ∈ 𝑆 ) )
19	17 18	mpbid	⊢ ( ( 𝜑 ∧ 𝑁 = ( 1 ..^ 𝑀 ) ) → ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) 𝐴 ∈ 𝑆 )
20		sigaclfu2	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) 𝐴 ∈ 𝑆 ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑀 ) 𝐴 ∈ 𝑆 )
21	16 19 20	syl2anc	⊢ ( ( 𝜑 ∧ 𝑁 = ( 1 ..^ 𝑀 ) ) → ∪ 𝑘 ∈ ( 1 ..^ 𝑀 ) 𝐴 ∈ 𝑆 )
22	15 21	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑁 = ( 1 ..^ 𝑀 ) ) → ∪ 𝑘 ∈ 𝑁 𝐴 ∈ 𝑆 )
23	13 22 2	mpjaodan	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝑁 𝐴 ∈ 𝑆 )