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	$$⊢Ⅎk\phi$$
	caragenfiiuncl.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
	caragenfiiuncl.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
	caragenfiiuncl.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	caragenfiiuncl.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in S$$
Assertion	caragenfiiuncl	$$⊢\phi \to \bigcup _{k\in A}B\in S$$

Proof

Step	Hyp	Ref	Expression
1		caragenfiiuncl.kph	$$⊢Ⅎk\phi$$
2		caragenfiiuncl.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
3		caragenfiiuncl.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
4		caragenfiiuncl.a	$$⊢\phi \to A\in \mathrm{Fin}$$
5		caragenfiiuncl.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in S$$
6		iuneq1	$$⊢A=\varnothing \to \bigcup _{k\in A}B=\bigcup _{k\in \varnothing }B$$
7		0iun	$$⊢\bigcup _{k\in \varnothing }B=\varnothing$$
8	7	a1i	$$⊢A=\varnothing \to \bigcup _{k\in \varnothing }B=\varnothing$$
9	6 8	eqtrd	$$⊢A=\varnothing \to \bigcup _{k\in A}B=\varnothing$$
10	9	adantl	$$⊢\left(\phi \wedge A=\varnothing \right)\to \bigcup _{k\in A}B=\varnothing$$
11	2 3	caragen0	$$⊢\phi \to \varnothing \in S$$
12	11	adantr	$$⊢\left(\phi \wedge A=\varnothing \right)\to \varnothing \in S$$
13	10 12	eqeltrd	$$⊢\left(\phi \wedge A=\varnothing \right)\to \bigcup _{k\in A}B\in S$$
14		simpl	$$⊢\left(\phi \wedge \neg A=\varnothing \right)\to \phi$$
15		neqne	$$⊢\neg A=\varnothing \to A\ne \varnothing$$
16	15	adantl	$$⊢\left(\phi \wedge \neg A=\varnothing \right)\to A\ne \varnothing$$
17		nfv	$$⊢ℲkA\ne \varnothing$$
18	1 17	nfan	$$⊢Ⅎk\left(\phi \wedge A\ne \varnothing \right)$$
19	5	adantlr	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge k\in A\right)\to B\in S$$
20	2	3ad2ant1	$$⊢\left(\phi \wedge x\in S\wedge y\in S\right)\to O\in \mathrm{OutMeas}$$
21		simp2	$$⊢\left(\phi \wedge x\in S\wedge y\in S\right)\to x\in S$$
22		simp3	$$⊢\left(\phi \wedge x\in S\wedge y\in S\right)\to y\in S$$
23	20 3 21 22	caragenuncl	$$⊢\left(\phi \wedge x\in S\wedge y\in S\right)\to x\cup y\in S$$
24	23	3adant1r	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge x\in S\wedge y\in S\right)\to x\cup y\in S$$
25	4	adantr	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to A\in \mathrm{Fin}$$
26		simpr	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to A\ne \varnothing$$
27	18 19 24 25 26	fiiuncl	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to \bigcup _{k\in A}B\in S$$
28	14 16 27	syl2anc	$$⊢\left(\phi \wedge \neg A=\varnothing \right)\to \bigcup _{k\in A}B\in S$$
29	13 28	pm2.61dan	$$⊢\phi \to \bigcup _{k\in A}B\in S$$