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	|- F/ k ph
	caragenfiiuncl.o	|- ( ph -> O e. OutMeas )
	caragenfiiuncl.s	|- S = ( CaraGen ` O )
	caragenfiiuncl.a	|- ( ph -> A e. Fin )
	caragenfiiuncl.b	|- ( ( ph /\ k e. A ) -> B e. S )
Assertion	caragenfiiuncl	|- ( ph -> U_ k e. A B e. S )

Proof

Step	Hyp	Ref	Expression
1		caragenfiiuncl.kph	|- F/ k ph
2		caragenfiiuncl.o	|- ( ph -> O e. OutMeas )
3		caragenfiiuncl.s	|- S = ( CaraGen ` O )
4		caragenfiiuncl.a	|- ( ph -> A e. Fin )
5		caragenfiiuncl.b	|- ( ( ph /\ k e. A ) -> B e. S )
6		iuneq1	|- ( A = (/) -> U_ k e. A B = U_ k e. (/) B )
7		0iun	|- U_ k e. (/) B = (/)
8	7	a1i	|- ( A = (/) -> U_ k e. (/) B = (/) )
9	6 8	eqtrd	|- ( A = (/) -> U_ k e. A B = (/) )
10	9	adantl	|- ( ( ph /\ A = (/) ) -> U_ k e. A B = (/) )
11	2 3	caragen0	|- ( ph -> (/) e. S )
12	11	adantr	|- ( ( ph /\ A = (/) ) -> (/) e. S )
13	10 12	eqeltrd	|- ( ( ph /\ A = (/) ) -> U_ k e. A B e. S )
14		simpl	|- ( ( ph /\ -. A = (/) ) -> ph )
15		neqne	|- ( -. A = (/) -> A =/= (/) )
16	15	adantl	|- ( ( ph /\ -. A = (/) ) -> A =/= (/) )
17		nfv	|- F/ k A =/= (/)
18	1 17	nfan	|- F/ k ( ph /\ A =/= (/) )
19	5	adantlr	|- ( ( ( ph /\ A =/= (/) ) /\ k e. A ) -> B e. S )
20	2	3ad2ant1	|- ( ( ph /\ x e. S /\ y e. S ) -> O e. OutMeas )
21		simp2	|- ( ( ph /\ x e. S /\ y e. S ) -> x e. S )
22		simp3	|- ( ( ph /\ x e. S /\ y e. S ) -> y e. S )
23	20 3 21 22	caragenuncl	|- ( ( ph /\ x e. S /\ y e. S ) -> ( x u. y ) e. S )
24	23	3adant1r	|- ( ( ( ph /\ A =/= (/) ) /\ x e. S /\ y e. S ) -> ( x u. y ) e. S )
25	4	adantr	|- ( ( ph /\ A =/= (/) ) -> A e. Fin )
26		simpr	|- ( ( ph /\ A =/= (/) ) -> A =/= (/) )
27	18 19 24 25 26	fiiuncl	|- ( ( ph /\ A =/= (/) ) -> U_ k e. A B e. S )
28	14 16 27	syl2anc	|- ( ( ph /\ -. A = (/) ) -> U_ k e. A B e. S )
29	13 28	pm2.61dan	|- ( ph -> U_ k e. A B e. S )