Metamath Proof Explorer


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 ( 𝜑 𝑋𝑆 )