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 
|- ( ph -> O e. OutMeas )
caragenunicl.s 
|- S = ( CaraGen ` O )
caragenunicl.y 
|- ( ph -> X C_ S )
caragenunicl.ctb 
|- ( ph -> X ~<_ _om )
Assertion caragenunicl 
|- ( ph -> U. X e. S )

Proof

Step Hyp Ref Expression
1 caragenunicl.o 
 |-  ( ph -> O e. OutMeas )
2 caragenunicl.s 
 |-  S = ( CaraGen ` O )
3 caragenunicl.y 
 |-  ( ph -> X C_ S )
4 caragenunicl.ctb 
 |-  ( ph -> X ~<_ _om )
5 unieq 
 |-  ( X = (/) -> U. X = U. (/) )
6 uni0 
 |-  U. (/) = (/)
7 5 6 eqtrdi 
 |-  ( X = (/) -> U. X = (/) )
8 7 adantl 
 |-  ( ( ph /\ X = (/) ) -> U. X = (/) )
9 1 2 caragen0 
 |-  ( ph -> (/) e. S )
10 9 adantr 
 |-  ( ( ph /\ X = (/) ) -> (/) e. S )
11 8 10 eqeltrd 
 |-  ( ( ph /\ X = (/) ) -> U. X e. S )
12 simpl 
 |-  ( ( ph /\ -. X = (/) ) -> ph )
13 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
14 13 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> X =/= (/) )
15 simpr 
 |-  ( ( ph /\ X =/= (/) ) -> X =/= (/) )
16 reldom 
 |-  Rel ~<_
17 brrelex1 
 |-  ( ( Rel ~<_ /\ X ~<_ _om ) -> X e. _V )
18 16 17 mpan 
 |-  ( X ~<_ _om -> X e. _V )
19 4 18 syl 
 |-  ( ph -> X e. _V )
20 19 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> X e. _V )
21 0sdomg 
 |-  ( X e. _V -> ( (/) ~< X <-> X =/= (/) ) )
22 20 21 syl 
 |-  ( ( ph /\ X =/= (/) ) -> ( (/) ~< X <-> X =/= (/) ) )
23 15 22 mpbird 
 |-  ( ( ph /\ X =/= (/) ) -> (/) ~< X )
24 nnenom 
 |-  NN ~~ _om
25 24 ensymi 
 |-  _om ~~ NN
26 25 a1i 
 |-  ( ph -> _om ~~ NN )
27 domentr 
 |-  ( ( X ~<_ _om /\ _om ~~ NN ) -> X ~<_ NN )
28 4 26 27 syl2anc 
 |-  ( ph -> X ~<_ NN )
29 28 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> X ~<_ NN )
30 fodomr 
 |-  ( ( (/) ~< X /\ X ~<_ NN ) -> E. f f : NN -onto-> X )
31 23 29 30 syl2anc 
 |-  ( ( ph /\ X =/= (/) ) -> E. f f : NN -onto-> X )
32 founiiun 
 |-  ( f : NN -onto-> X -> U. X = U_ n e. NN ( f ` n ) )
33 32 adantl 
 |-  ( ( ph /\ f : NN -onto-> X ) -> U. X = U_ n e. NN ( f ` n ) )
34 1 adantr 
 |-  ( ( ph /\ f : NN -onto-> X ) -> O e. OutMeas )
35 1zzd 
 |-  ( ( ph /\ f : NN -onto-> X ) -> 1 e. ZZ )
36 nnuz 
 |-  NN = ( ZZ>= ` 1 )
37 fof 
 |-  ( f : NN -onto-> X -> f : NN --> X )
38 37 adantl 
 |-  ( ( ph /\ f : NN -onto-> X ) -> f : NN --> X )
39 3 adantr 
 |-  ( ( ph /\ f : NN -onto-> X ) -> X C_ S )
40 38 39 fssd 
 |-  ( ( ph /\ f : NN -onto-> X ) -> f : NN --> S )
41 34 2 35 36 40 carageniuncl 
 |-  ( ( ph /\ f : NN -onto-> X ) -> U_ n e. NN ( f ` n ) e. S )
42 33 41 eqeltrd 
 |-  ( ( ph /\ f : NN -onto-> X ) -> U. X e. S )
43 42 ex 
 |-  ( ph -> ( f : NN -onto-> X -> U. X e. S ) )
44 43 adantr 
 |-  ( ( ph /\ X =/= (/) ) -> ( f : NN -onto-> X -> U. X e. S ) )
45 44 exlimdv 
 |-  ( ( ph /\ X =/= (/) ) -> ( E. f f : NN -onto-> X -> U. X e. S ) )
46 31 45 mpd 
 |-  ( ( ph /\ X =/= (/) ) -> U. X e. S )
47 12 14 46 syl2anc 
 |-  ( ( ph /\ -. X = (/) ) -> U. X e. S )
48 11 47 pm2.61dan 
 |-  ( ph -> U. X e. S )