Theorem sigaclcuni

Description: A sigma-algebra is closed under countable union: indexed union version. (Contributed by Thierry Arnoux, 8-Jun-2017)

	Ref	Expression
Hypothesis	sigaclcuni.1	⊢ Ⅎ 𝑘 𝐴
Assertion	sigaclcuni	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω ) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		sigaclcuni.1	⊢ Ⅎ 𝑘 𝐴
2		dfiun2g	⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 → ∪ 𝑘 ∈ 𝐴 𝐵 = ∪ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } )
3	2	3ad2ant2	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω ) → ∪ 𝑘 ∈ 𝐴 𝐵 = ∪ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } )
4		simp1	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω ) → 𝑆 ∈ ∪ ran sigAlgebra )
5		r19.29	⊢ ( ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 ) → ∃ 𝑘 ∈ 𝐴 ( 𝐵 ∈ 𝑆 ∧ 𝑧 = 𝐵 ) )
6		simpr	⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝑧 = 𝐵 ) → 𝑧 = 𝐵 )
7		simpl	⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝑧 = 𝐵 ) → 𝐵 ∈ 𝑆 )
8	6 7	eqeltrd	⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝑧 = 𝐵 ) → 𝑧 ∈ 𝑆 )
9	8	rexlimivw	⊢ ( ∃ 𝑘 ∈ 𝐴 ( 𝐵 ∈ 𝑆 ∧ 𝑧 = 𝐵 ) → 𝑧 ∈ 𝑆 )
10	5 9	syl	⊢ ( ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 ) → 𝑧 ∈ 𝑆 )
11	10	ex	⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 → ( ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ∈ 𝑆 ) )
12	11	abssdv	⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 → { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } ⊆ 𝑆 )
13	12	3ad2ant2	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω ) → { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } ⊆ 𝑆 )
14		elpw2g	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } ∈ 𝒫 𝑆 ↔ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } ⊆ 𝑆 ) )
15	4 14	syl	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω ) → ( { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } ∈ 𝒫 𝑆 ↔ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } ⊆ 𝑆 ) )
16	13 15	mpbird	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω ) → { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } ∈ 𝒫 𝑆 )
17	1	abrexctf	⊢ ( 𝐴 ≼ ω → { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } ≼ ω )
18	17	3ad2ant3	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω ) → { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } ≼ ω )
19		sigaclcu	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } ∈ 𝒫 𝑆 ∧ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } ≼ ω ) → ∪ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } ∈ 𝑆 )
20	4 16 18 19	syl3anc	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω ) → ∪ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐵 } ∈ 𝑆 )
21	3 20	eqeltrd	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 ∧ 𝐴 ≼ ω ) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 )