Metamath Proof Explorer

Theorem omsf

Description: A constructed outer measure is a function. (Contributed by Thierry Arnoux, 17-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Assertion omsf 
|- ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> ( toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
2 xrltso 
 |-  < Or RR*
3 soss 
 |-  ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
4 1 2 3 mp2 
 |-  < Or ( 0 [,] +oo )
5 4 a1i 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) /\ a e. ~P U. dom R ) -> < Or ( 0 [,] +oo ) )
6 omscl 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ a e. ~P U. dom R ) -> ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) C_ ( 0 [,] +oo ) )
7 6 3expa 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) /\ a e. ~P U. dom R ) -> ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) C_ ( 0 [,] +oo ) )
8 xrge0infss 
 |-  ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) C_ ( 0 [,] +oo ) -> E. t e. ( 0 [,] +oo ) ( A. w e. ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) -. w < t /\ A. w e. ( 0 [,] +oo ) ( t < w -> E. s e. ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) s < w ) ) )
9 7 8 syl 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) /\ a e. ~P U. dom R ) -> E. t e. ( 0 [,] +oo ) ( A. w e. ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) -. w < t /\ A. w e. ( 0 [,] +oo ) ( t < w -> E. s e. ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) s < w ) ) )
10 5 9 infcl 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) /\ a e. ~P U. dom R ) -> inf ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) e. ( 0 [,] +oo ) )
11 fex 
 |-  ( ( R : Q --> ( 0 [,] +oo ) /\ Q e. V ) -> R e. _V )
12 11 ancoms 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> R e. _V )
13 omsval 
 |-  ( R e. _V -> ( toOMeas ` R ) = ( a e. ~P U. dom R |-> inf ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) ) )
14 12 13 syl 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> ( toOMeas ` R ) = ( a e. ~P U. dom R |-> inf ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) ) )
15 simpll 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) /\ a e. ~P U. dom R ) -> Q e. V )
16 simplr 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) /\ a e. ~P U. dom R ) -> R : Q --> ( 0 [,] +oo ) )
17 simpr 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) /\ a e. ~P U. dom R ) -> a e. ~P U. dom R )
18 fdm 
 |-  ( R : Q --> ( 0 [,] +oo ) -> dom R = Q )
19 18 unieqd 
 |-  ( R : Q --> ( 0 [,] +oo ) -> U. dom R = U. Q )
20 19 pweqd 
 |-  ( R : Q --> ( 0 [,] +oo ) -> ~P U. dom R = ~P U. Q )
21 20 ad2antlr 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) /\ a e. ~P U. dom R ) -> ~P U. dom R = ~P U. Q )
22 17 21 eleqtrd 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) /\ a e. ~P U. dom R ) -> a e. ~P U. Q )
23 elpwi 
 |-  ( a e. ~P U. Q -> a C_ U. Q )
24 22 23 syl 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) /\ a e. ~P U. dom R ) -> a C_ U. Q )
25 omsfval 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ a C_ U. Q ) -> ( ( toOMeas ` R ) ` a ) = inf ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) )
26 15 16 24 25 syl3anc 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) /\ a e. ~P U. dom R ) -> ( ( toOMeas ` R ) ` a ) = inf ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) )
27 26 10 eqeltrd 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) /\ a e. ~P U. dom R ) -> ( ( toOMeas ` R ) ` a ) e. ( 0 [,] +oo ) )
28 10 14 27 fmpt2d 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) ) -> ( toOMeas ` R ) : ~P U. dom R --> ( 0 [,] +oo ) )