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	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	caragenunicl.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
	caragenunicl.y	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
	caragenunicl.ctb	⊢ ( 𝜑 → 𝑋 ≼ ω )
Assertion	caragenunicl	⊢ ( 𝜑 → ∪ 𝑋 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		caragenunicl.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		caragenunicl.s	⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3		caragenunicl.y	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
4		caragenunicl.ctb	⊢ ( 𝜑 → 𝑋 ≼ ω )
5		unieq	⊢ ( 𝑋 = ∅ → ∪ 𝑋 = ∪ ∅ )
6		uni0	⊢ ∪ ∅ = ∅
7	5 6	eqtrdi	⊢ ( 𝑋 = ∅ → ∪ 𝑋 = ∅ )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∪ 𝑋 = ∅ )
9	1 2	caragen0	⊢ ( 𝜑 → ∅ ∈ 𝑆 )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∅ ∈ 𝑆 )
11	8 10	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∪ 𝑋 ∈ 𝑆 )
12		simpl	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝜑 )
13		neqne	⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
14	13	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≠ ∅ )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝑋 ≠ ∅ )
16		reldom	⊢ Rel ≼
17		brrelex1	⊢ ( ( Rel ≼ ∧ 𝑋 ≼ ω ) → 𝑋 ∈ V )
18	16 17	mpan	⊢ ( 𝑋 ≼ ω → 𝑋 ∈ V )
19	4 18	syl	⊢ ( 𝜑 → 𝑋 ∈ V )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝑋 ∈ V )
21		0sdomg	⊢ ( 𝑋 ∈ V → ( ∅ ≺ 𝑋 ↔ 𝑋 ≠ ∅ ) )
22	20 21	syl	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ∅ ≺ 𝑋 ↔ 𝑋 ≠ ∅ ) )
23	15 22	mpbird	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∅ ≺ 𝑋 )
24		nnenom	⊢ ℕ ≈ ω
25	24	ensymi	⊢ ω ≈ ℕ
26	25	a1i	⊢ ( 𝜑 → ω ≈ ℕ )
27		domentr	⊢ ( ( 𝑋 ≼ ω ∧ ω ≈ ℕ ) → 𝑋 ≼ ℕ )
28	4 26 27	syl2anc	⊢ ( 𝜑 → 𝑋 ≼ ℕ )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → 𝑋 ≼ ℕ )
30		fodomr	⊢ ( ( ∅ ≺ 𝑋 ∧ 𝑋 ≼ ℕ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝑋 )
31	23 29 30	syl2anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝑋 )
32		founiiun	⊢ ( 𝑓 : ℕ –onto→ 𝑋 → ∪ 𝑋 = ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) )
33	32	adantl	⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –onto→ 𝑋 ) → ∪ 𝑋 = ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) )
34	1	adantr	⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –onto→ 𝑋 ) → 𝑂 ∈ OutMeas )
35		1zzd	⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –onto→ 𝑋 ) → 1 ∈ ℤ )
36		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
37		fof	⊢ ( 𝑓 : ℕ –onto→ 𝑋 → 𝑓 : ℕ ⟶ 𝑋 )
38	37	adantl	⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –onto→ 𝑋 ) → 𝑓 : ℕ ⟶ 𝑋 )
39	3	adantr	⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –onto→ 𝑋 ) → 𝑋 ⊆ 𝑆 )
40	38 39	fssd	⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –onto→ 𝑋 ) → 𝑓 : ℕ ⟶ 𝑆 )
41	34 2 35 36 40	carageniuncl	⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –onto→ 𝑋 ) → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ∈ 𝑆 )
42	33 41	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –onto→ 𝑋 ) → ∪ 𝑋 ∈ 𝑆 )
43	42	ex	⊢ ( 𝜑 → ( 𝑓 : ℕ –onto→ 𝑋 → ∪ 𝑋 ∈ 𝑆 ) )
44	43	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( 𝑓 : ℕ –onto→ 𝑋 → ∪ 𝑋 ∈ 𝑆 ) )
45	44	exlimdv	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑓 𝑓 : ℕ –onto→ 𝑋 → ∪ 𝑋 ∈ 𝑆 ) )
46	31 45	mpd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ∪ 𝑋 ∈ 𝑆 )
47	12 14 46	syl2anc	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∪ 𝑋 ∈ 𝑆 )
48	11 47	pm2.61dan	⊢ ( 𝜑 → ∪ 𝑋 ∈ 𝑆 )