Theorem caragenunicl

Description: The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of Fremlin1 p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	caragenunicl.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
	caragenunicl.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
	caragenunicl.y	$$⊢\phi \to X\subseteq S$$
	caragenunicl.ctb	$$⊢\phi \to X\preccurlyeq \mathrm{\omega }$$
Assertion	caragenunicl	$$⊢\phi \to \bigcup X\in S$$

Proof

Step	Hyp	Ref	Expression
1		caragenunicl.o	$$⊢\phi \to O\in \mathrm{OutMeas}$$
2		caragenunicl.s	$$⊢S=\mathrm{CaraGen}\left(O\right)$$
3		caragenunicl.y	$$⊢\phi \to X\subseteq S$$
4		caragenunicl.ctb	$$⊢\phi \to X\preccurlyeq \mathrm{\omega }$$
5		unieq	$$⊢X=\varnothing \to \bigcup X=\bigcup \varnothing$$
6		uni0	$$⊢\bigcup \varnothing =\varnothing$$
7	5 6	eqtrdi	$$⊢X=\varnothing \to \bigcup X=\varnothing$$
8	7	adantl	$$⊢\left(\phi \wedge X=\varnothing \right)\to \bigcup X=\varnothing$$
9	1 2	caragen0	$$⊢\phi \to \varnothing \in S$$
10	9	adantr	$$⊢\left(\phi \wedge X=\varnothing \right)\to \varnothing \in S$$
11	8 10	eqeltrd	$$⊢\left(\phi \wedge X=\varnothing \right)\to \bigcup X\in S$$
12		simpl	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to \phi$$
13		neqne	$$⊢\neg X=\varnothing \to X\ne \varnothing$$
14	13	adantl	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to X\ne \varnothing$$
15		simpr	$$⊢\left(\phi \wedge X\ne \varnothing \right)\to X\ne \varnothing$$
16		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
17		brrelex1	$$⊢\left(\mathrm{Rel}\preccurlyeq \wedge X\preccurlyeq \mathrm{\omega }\right)\to X\in \mathrm{V}$$
18	16 17	mpan	$$⊢X\preccurlyeq \mathrm{\omega }\to X\in \mathrm{V}$$
19	4 18	syl	$$⊢\phi \to X\in \mathrm{V}$$
20	19	adantr	$$⊢\left(\phi \wedge X\ne \varnothing \right)\to X\in \mathrm{V}$$
21		0sdomg	$$⊢X\in \mathrm{V}\to \left(\varnothing \prec X\leftrightarrow X\ne \varnothing \right)$$
22	20 21	syl	$$⊢\left(\phi \wedge X\ne \varnothing \right)\to \left(\varnothing \prec X\leftrightarrow X\ne \varnothing \right)$$
23	15 22	mpbird	$$⊢\left(\phi \wedge X\ne \varnothing \right)\to \varnothing \prec X$$
24		nnenom	$$⊢\mathbb{N}\approx \mathrm{\omega }$$
25	24	ensymi	$$⊢\mathrm{\omega }\approx \mathbb{N}$$
26	25	a1i	$$⊢\phi \to \mathrm{\omega }\approx \mathbb{N}$$
27		domentr	$$⊢\left(X\preccurlyeq \mathrm{\omega }\wedge \mathrm{\omega }\approx \mathbb{N}\right)\to X\preccurlyeq \mathbb{N}$$
28	4 26 27	syl2anc	$$⊢\phi \to X\preccurlyeq \mathbb{N}$$
29	28	adantr	$$⊢\left(\phi \wedge X\ne \varnothing \right)\to X\preccurlyeq \mathbb{N}$$
30		fodomr	$$⊢\left(\varnothing \prec X\wedge X\preccurlyeq \mathbb{N}\right)\to \exists ff:\mathbb{N}\underset{onto}{⟶}X$$
31	23 29 30	syl2anc	$$⊢\left(\phi \wedge X\ne \varnothing \right)\to \exists ff:\mathbb{N}\underset{onto}{⟶}X$$
32		founiiun	$$⊢f:\mathbb{N}\underset{onto}{⟶}X\to \bigcup X=\bigcup _{n\in \mathbb{N}}f\left(n\right)$$
33	32	adantl	$$⊢\left(\phi \wedge f:\mathbb{N}\underset{onto}{⟶}X\right)\to \bigcup X=\bigcup _{n\in \mathbb{N}}f\left(n\right)$$
34	1	adantr	$$⊢\left(\phi \wedge f:\mathbb{N}\underset{onto}{⟶}X\right)\to O\in \mathrm{OutMeas}$$
35		1zzd	$$⊢\left(\phi \wedge f:\mathbb{N}\underset{onto}{⟶}X\right)\to 1\in \mathbb{Z}$$
36		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
37		fof	$$⊢f:\mathbb{N}\underset{onto}{⟶}X\to f:\mathbb{N}⟶X$$
38	37	adantl	$$⊢\left(\phi \wedge f:\mathbb{N}\underset{onto}{⟶}X\right)\to f:\mathbb{N}⟶X$$
39	3	adantr	$$⊢\left(\phi \wedge f:\mathbb{N}\underset{onto}{⟶}X\right)\to X\subseteq S$$
40	38 39	fssd	$$⊢\left(\phi \wedge f:\mathbb{N}\underset{onto}{⟶}X\right)\to f:\mathbb{N}⟶S$$
41	34 2 35 36 40	carageniuncl	$$⊢\left(\phi \wedge f:\mathbb{N}\underset{onto}{⟶}X\right)\to \bigcup _{n\in \mathbb{N}}f\left(n\right)\in S$$
42	33 41	eqeltrd	$$⊢\left(\phi \wedge f:\mathbb{N}\underset{onto}{⟶}X\right)\to \bigcup X\in S$$
43	42	ex	$$⊢\phi \to \left(f:\mathbb{N}\underset{onto}{⟶}X\to \bigcup X\in S\right)$$
44	43	adantr	$$⊢\left(\phi \wedge X\ne \varnothing \right)\to \left(f:\mathbb{N}\underset{onto}{⟶}X\to \bigcup X\in S\right)$$
45	44	exlimdv	$$⊢\left(\phi \wedge X\ne \varnothing \right)\to \left(\exists ff:\mathbb{N}\underset{onto}{⟶}X\to \bigcup X\in S\right)$$
46	31 45	mpd	$$⊢\left(\phi \wedge X\ne \varnothing \right)\to \bigcup X\in S$$
47	12 14 46	syl2anc	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to \bigcup X\in S$$
48	11 47	pm2.61dan	$$⊢\phi \to \bigcup X\in S$$