Theorem caragenfiiuncl

Description: The Caratheodory's construction is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	caragenfiiuncl.kph	⊢ Ⅎ 𝑘 𝜑
	caragenfiiuncl.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	caragenfiiuncl.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
	caragenfiiuncl.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	caragenfiiuncl.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑆 )
Assertion	caragenfiiuncl	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		caragenfiiuncl.kph	⊢ Ⅎ 𝑘 𝜑
2		caragenfiiuncl.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
3		caragenfiiuncl.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
4		caragenfiiuncl.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
5		caragenfiiuncl.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑆 )
6		iuneq1	⊢ ( 𝐴 = ∅ → ∪ 𝑘 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ ∅ 𝐵 )
7		0iun	⊢ ∪ 𝑘 ∈ ∅ 𝐵 = ∅
8	7	a1i	⊢ ( 𝐴 = ∅ → ∪ 𝑘 ∈ ∅ 𝐵 = ∅ )
9	6 8	eqtrd	⊢ ( 𝐴 = ∅ → ∪ 𝑘 ∈ 𝐴 𝐵 = ∅ )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ∪ 𝑘 ∈ 𝐴 𝐵 = ∅ )
11	2 3	caragen0	⊢ ( 𝜑 → ∅ ∈ 𝑆 )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ∅ ∈ 𝑆 )
13	10 12	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 )
14		simpl	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝜑 )
15		neqne	⊢ ( ¬ 𝐴 = ∅ → 𝐴 ≠ ∅ )
16	15	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ≠ ∅ )
17		nfv	⊢ Ⅎ 𝑘 𝐴 ≠ ∅
18	1 17	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝐴 ≠ ∅ )
19	5	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑆 )
20	2	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝑂 ∈ OutMeas )
21		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
22		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
23	20 3 21 22	caragenuncl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ∪ 𝑦 ) ∈ 𝑆 )
24	23	3adant1r	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ∪ 𝑦 ) ∈ 𝑆 )
25	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → 𝐴 ∈ Fin )
26		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
27	18 19 24 25 26	fiiuncl	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 )
28	14 16 27	syl2anc	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 )
29	13 28	pm2.61dan	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 )