Metamath Proof Explorer

Theorem omsfval

Description: Value of the outer measure evaluated for a given set A . (Contributed by Thierry Arnoux, 15-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Assertion 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 ) , < ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> R : Q --> ( 0 [,] +oo ) )
2 simp1 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> Q e. V )
3 1 2 fexd 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> R e. _V )
4 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 ) , < ) ) )
5 3 4 syl 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> ( 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 ) , < ) ) )
6 simpr 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) /\ a = A ) -> a = A )
7 6 sseq1d 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) /\ a = A ) -> ( a C_ U. z <-> A C_ U. z ) )
8 7 anbi1d 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) /\ a = A ) -> ( ( a C_ U. z /\ z ~<_ _om ) <-> ( A C_ U. z /\ z ~<_ _om ) ) )
9 8 rabbidv 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) /\ a = A ) -> { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } = { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } )
10 9 mpteq1d 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) /\ a = A ) -> ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) = ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) )
11 10 rneqd 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) /\ a = A ) -> ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) = ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) )
12 11 infeq1d 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) /\ a = A ) -> inf ( ran ( x e. { z e. ~P dom R | ( a C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) = inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) )
13 simp3 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> A C_ U. Q )
14 fdm 
 |-  ( R : Q --> ( 0 [,] +oo ) -> dom R = Q )
15 14 3ad2ant2 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> dom R = Q )
16 15 unieqd 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> U. dom R = U. Q )
17 13 16 sseqtrrd 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> A C_ U. dom R )
18 2 uniexd 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> U. Q e. _V )
19 ssexg 
 |-  ( ( A C_ U. Q /\ U. Q e. _V ) -> A e. _V )
20 13 18 19 syl2anc 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> A e. _V )
21 elpwg 
 |-  ( A e. _V -> ( A e. ~P U. dom R <-> A C_ U. dom R ) )
22 20 21 syl 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> ( A e. ~P U. dom R <-> A C_ U. dom R ) )
23 17 22 mpbird 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> A e. ~P U. dom R )
24 xrltso 
 |-  < Or RR*
25 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
26 soss 
 |-  ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
27 25 26 ax-mp 
 |-  ( < Or RR* -> < Or ( 0 [,] +oo ) )
28 24 27 mp1i 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> < Or ( 0 [,] +oo ) )
29 28 infexd 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) e. _V )
30 5 12 23 29 fvmptd 
 |-  ( ( 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 ) , < ) )