Metamath Proof Explorer

Theorem isomennd

Description: Sufficient condition to prove that O is an outer measure. Definition 113A of Fremlin1 p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses isomennd.x 
|- ( ph -> X e. V )
isomennd.o 
|- ( ph -> O : ~P X --> ( 0 [,] +oo ) )
isomennd.o0 
|- ( ph -> ( O ` (/) ) = 0 )
isomennd.le 
|- ( ( ph /\ x C_ X /\ y C_ x ) -> ( O ` y ) <_ ( O ` x ) )
isomennd.sa 
|- ( ( ph /\ a : NN --> ~P X ) -> ( O ` U_ n e. NN ( a ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( O ` ( a ` n ) ) ) ) )
Assertion isomennd 
|- ( ph -> O e. OutMeas )

Proof

Step Hyp Ref Expression
1 isomennd.x 
 |-  ( ph -> X e. V )
2 isomennd.o 
 |-  ( ph -> O : ~P X --> ( 0 [,] +oo ) )
3 isomennd.o0 
 |-  ( ph -> ( O ` (/) ) = 0 )
4 isomennd.le 
 |-  ( ( ph /\ x C_ X /\ y C_ x ) -> ( O ` y ) <_ ( O ` x ) )
5 isomennd.sa 
 |-  ( ( ph /\ a : NN --> ~P X ) -> ( O ` U_ n e. NN ( a ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( O ` ( a ` n ) ) ) ) )
6 id 
 |-  ( O : ~P X --> ( 0 [,] +oo ) -> O : ~P X --> ( 0 [,] +oo ) )
7 fdm 
 |-  ( O : ~P X --> ( 0 [,] +oo ) -> dom O = ~P X )
8 7 feq2d 
 |-  ( O : ~P X --> ( 0 [,] +oo ) -> ( O : dom O --> ( 0 [,] +oo ) <-> O : ~P X --> ( 0 [,] +oo ) ) )
9 6 8 mpbird 
 |-  ( O : ~P X --> ( 0 [,] +oo ) -> O : dom O --> ( 0 [,] +oo ) )
10 2 9 syl 
 |-  ( ph -> O : dom O --> ( 0 [,] +oo ) )
11 unipw 
 |-  U. ~P X = X
12 11 pweqi 
 |-  ~P U. ~P X = ~P X
13 12 a1i 
 |-  ( ph -> ~P U. ~P X = ~P X )
14 2 7 syl 
 |-  ( ph -> dom O = ~P X )
15 14 unieqd 
 |-  ( ph -> U. dom O = U. ~P X )
16 15 pweqd 
 |-  ( ph -> ~P U. dom O = ~P U. ~P X )
17 13 16 14 3eqtr4rd 
 |-  ( ph -> dom O = ~P U. dom O )
18 10 17 3 jca31 
 |-  ( ph -> ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) )
19 simpl 
 |-  ( ( ph /\ ( x e. ~P U. dom O /\ y e. ~P x ) ) -> ph )
20 simpr 
 |-  ( ( ph /\ x e. ~P U. dom O ) -> x e. ~P U. dom O )
21 16 13 eqtrd 
 |-  ( ph -> ~P U. dom O = ~P X )
22 21 adantr 
 |-  ( ( ph /\ x e. ~P U. dom O ) -> ~P U. dom O = ~P X )
23 20 22 eleqtrd 
 |-  ( ( ph /\ x e. ~P U. dom O ) -> x e. ~P X )
24 elpwi 
 |-  ( x e. ~P X -> x C_ X )
25 23 24 syl 
 |-  ( ( ph /\ x e. ~P U. dom O ) -> x C_ X )
26 25 adantrr 
 |-  ( ( ph /\ ( x e. ~P U. dom O /\ y e. ~P x ) ) -> x C_ X )
27 elpwi 
 |-  ( y e. ~P x -> y C_ x )
28 27 adantl 
 |-  ( ( x e. ~P U. dom O /\ y e. ~P x ) -> y C_ x )
29 28 adantl 
 |-  ( ( ph /\ ( x e. ~P U. dom O /\ y e. ~P x ) ) -> y C_ x )
30 19 26 29 4 syl3anc 
 |-  ( ( ph /\ ( x e. ~P U. dom O /\ y e. ~P x ) ) -> ( O ` y ) <_ ( O ` x ) )
31 30 ralrimivva 
 |-  ( ph -> A. x e. ~P U. dom O A. y e. ~P x ( O ` y ) <_ ( O ` x ) )
32 0le0 
 |-  0 <_ 0
33 32 a1i 
 |-  ( ( ph /\ x = (/) ) -> 0 <_ 0 )
34 unieq 
 |-  ( x = (/) -> U. x = U. (/) )
35 uni0 
 |-  U. (/) = (/)
36 35 a1i 
 |-  ( x = (/) -> U. (/) = (/) )
37 34 36 eqtrd 
 |-  ( x = (/) -> U. x = (/) )
38 37 fveq2d 
 |-  ( x = (/) -> ( O ` U. x ) = ( O ` (/) ) )
39 38 adantl 
 |-  ( ( ph /\ x = (/) ) -> ( O ` U. x ) = ( O ` (/) ) )
40 3 adantr 
 |-  ( ( ph /\ x = (/) ) -> ( O ` (/) ) = 0 )
41 39 40 eqtrd 
 |-  ( ( ph /\ x = (/) ) -> ( O ` U. x ) = 0 )
42 reseq2 
 |-  ( x = (/) -> ( O |` x ) = ( O |` (/) ) )
43 res0 
 |-  ( O |` (/) ) = (/)
44 43 a1i 
 |-  ( x = (/) -> ( O |` (/) ) = (/) )
45 42 44 eqtrd 
 |-  ( x = (/) -> ( O |` x ) = (/) )
46 45 fveq2d 
 |-  ( x = (/) -> ( sum^ ` ( O |` x ) ) = ( sum^ ` (/) ) )
47 sge00 
 |-  ( sum^ ` (/) ) = 0
48 47 a1i 
 |-  ( x = (/) -> ( sum^ ` (/) ) = 0 )
49 46 48 eqtrd 
 |-  ( x = (/) -> ( sum^ ` ( O |` x ) ) = 0 )
50 49 adantl 
 |-  ( ( ph /\ x = (/) ) -> ( sum^ ` ( O |` x ) ) = 0 )
51 41 50 breq12d 
 |-  ( ( ph /\ x = (/) ) -> ( ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) <-> 0 <_ 0 ) )
52 33 51 mpbird 
 |-  ( ( ph /\ x = (/) ) -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) )
53 52 ad4ant14 
 |-  ( ( ( ( ph /\ x e. ~P dom O ) /\ x ~<_ _om ) /\ x = (/) ) -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) )
54 simpl 
 |-  ( ( ( ( ph /\ x e. ~P dom O ) /\ x ~<_ _om ) /\ -. x = (/) ) -> ( ( ph /\ x e. ~P dom O ) /\ x ~<_ _om ) )
55 neqne 
 |-  ( -. x = (/) -> x =/= (/) )
56 55 adantl 
 |-  ( ( ( ( ph /\ x e. ~P dom O ) /\ x ~<_ _om ) /\ -. x = (/) ) -> x =/= (/) )
57 ssnnf1octb 
 |-  ( ( x ~<_ _om /\ x =/= (/) ) -> E. f ( dom f C_ NN /\ f : dom f -1-1-onto-> x ) )
58 57 adantll 
 |-  ( ( ( ( ph /\ x e. ~P dom O ) /\ x ~<_ _om ) /\ x =/= (/) ) -> E. f ( dom f C_ NN /\ f : dom f -1-1-onto-> x ) )
59 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ~P dom O ) /\ ( dom f C_ NN /\ f : dom f -1-1-onto-> x ) ) -> O : ~P X --> ( 0 [,] +oo ) )
60 3 ad2antrr 
 |-  ( ( ( ph /\ x e. ~P dom O ) /\ ( dom f C_ NN /\ f : dom f -1-1-onto-> x ) ) -> ( O ` (/) ) = 0 )
61 simpr 
 |-  ( ( ph /\ x e. ~P dom O ) -> x e. ~P dom O )
62 14 pweqd 
 |-  ( ph -> ~P dom O = ~P ~P X )
63 62 adantr 
 |-  ( ( ph /\ x e. ~P dom O ) -> ~P dom O = ~P ~P X )
64 61 63 eleqtrd 
 |-  ( ( ph /\ x e. ~P dom O ) -> x e. ~P ~P X )
65 elpwi 
 |-  ( x e. ~P ~P X -> x C_ ~P X )
66 64 65 syl 
 |-  ( ( ph /\ x e. ~P dom O ) -> x C_ ~P X )
67 66 adantr 
 |-  ( ( ( ph /\ x e. ~P dom O ) /\ ( dom f C_ NN /\ f : dom f -1-1-onto-> x ) ) -> x C_ ~P X )
68 simpl 
 |-  ( ( ph /\ x e. ~P dom O ) -> ph )
69 68 5 sylan 
 |-  ( ( ( ph /\ x e. ~P dom O ) /\ a : NN --> ~P X ) -> ( O ` U_ n e. NN ( a ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( O ` ( a ` n ) ) ) ) )
70 69 adantlr 
 |-  ( ( ( ( ph /\ x e. ~P dom O ) /\ ( dom f C_ NN /\ f : dom f -1-1-onto-> x ) ) /\ a : NN --> ~P X ) -> ( O ` U_ n e. NN ( a ` n ) ) <_ ( sum^ ` ( n e. NN |-> ( O ` ( a ` n ) ) ) ) )
71 simprl 
 |-  ( ( ( ph /\ x e. ~P dom O ) /\ ( dom f C_ NN /\ f : dom f -1-1-onto-> x ) ) -> dom f C_ NN )
72 simprr 
 |-  ( ( ( ph /\ x e. ~P dom O ) /\ ( dom f C_ NN /\ f : dom f -1-1-onto-> x ) ) -> f : dom f -1-1-onto-> x )
73 eleq1w 
 |-  ( m = n -> ( m e. dom f <-> n e. dom f ) )
74 fveq2 
 |-  ( m = n -> ( f ` m ) = ( f ` n ) )
75 73 74 ifbieq1d 
 |-  ( m = n -> if ( m e. dom f , ( f ` m ) , (/) ) = if ( n e. dom f , ( f ` n ) , (/) ) )
76 75 cbvmptv 
 |-  ( m e. NN |-> if ( m e. dom f , ( f ` m ) , (/) ) ) = ( n e. NN |-> if ( n e. dom f , ( f ` n ) , (/) ) )
77 59 60 67 70 71 72 76 isomenndlem 
 |-  ( ( ( ph /\ x e. ~P dom O ) /\ ( dom f C_ NN /\ f : dom f -1-1-onto-> x ) ) -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) )
78 77 ex 
 |-  ( ( ph /\ x e. ~P dom O ) -> ( ( dom f C_ NN /\ f : dom f -1-1-onto-> x ) -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) ) )
79 78 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ~P dom O ) /\ x ~<_ _om ) /\ x =/= (/) ) -> ( ( dom f C_ NN /\ f : dom f -1-1-onto-> x ) -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) ) )
80 79 exlimdv 
 |-  ( ( ( ( ph /\ x e. ~P dom O ) /\ x ~<_ _om ) /\ x =/= (/) ) -> ( E. f ( dom f C_ NN /\ f : dom f -1-1-onto-> x ) -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) ) )
81 58 80 mpd 
 |-  ( ( ( ( ph /\ x e. ~P dom O ) /\ x ~<_ _om ) /\ x =/= (/) ) -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) )
82 54 56 81 syl2anc 
 |-  ( ( ( ( ph /\ x e. ~P dom O ) /\ x ~<_ _om ) /\ -. x = (/) ) -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) )
83 53 82 pm2.61dan 
 |-  ( ( ( ph /\ x e. ~P dom O ) /\ x ~<_ _om ) -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) )
84 83 ex 
 |-  ( ( ph /\ x e. ~P dom O ) -> ( x ~<_ _om -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) ) )
85 84 ralrimiva 
 |-  ( ph -> A. x e. ~P dom O ( x ~<_ _om -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) ) )
86 18 31 85 jca31 
 |-  ( ph -> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. x e. ~P U. dom O A. y e. ~P x ( O ` y ) <_ ( O ` x ) ) /\ A. x e. ~P dom O ( x ~<_ _om -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) ) ) )
87 1 pwexd 
 |-  ( ph -> ~P X e. _V )
88 2 87 fexd 
 |-  ( ph -> O e. _V )
89 isome 
 |-  ( O e. _V -> ( O e. OutMeas <-> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. x e. ~P U. dom O A. y e. ~P x ( O ` y ) <_ ( O ` x ) ) /\ A. x e. ~P dom O ( x ~<_ _om -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) ) ) ) )
90 88 89 syl 
 |-  ( ph -> ( O e. OutMeas <-> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. x e. ~P U. dom O A. y e. ~P x ( O ` y ) <_ ( O ` x ) ) /\ A. x e. ~P dom O ( x ~<_ _om -> ( O ` U. x ) <_ ( sum^ ` ( O |` x ) ) ) ) ) )
91 86 90 mpbird 
 |-  ( ph -> O e. OutMeas )