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 fex 
 |-  ( ( R : Q --> ( 0 [,] +oo ) /\ Q e. V ) -> R e. _V )
4 1 2 3 syl2anc 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> R e. _V )
5 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 ) , < ) ) )
6 4 5 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 ) , < ) ) )
7 simpr 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) /\ a = A ) -> a = A )
8 7 sseq1d 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) /\ a = A ) -> ( a C_ U. z <-> A C_ U. z ) )
9 8 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 ) ) )
10 9 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 ) } )
11 10 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 ) ) )
12 11 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 ) ) )
13 12 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 ) , < ) )
14 simp3 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> A C_ U. Q )
15 fdm 
 |-  ( R : Q --> ( 0 [,] +oo ) -> dom R = Q )
16 15 3ad2ant2 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> dom R = Q )
17 16 unieqd 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> U. dom R = U. Q )
18 14 17 sseqtrrd 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> A C_ U. dom R )
19 2 uniexd 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> U. Q e. _V )
20 ssexg 
 |-  ( ( A C_ U. Q /\ U. Q e. _V ) -> A e. _V )
21 14 19 20 syl2anc 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> A e. _V )
22 elpwg 
 |-  ( A e. _V -> ( A e. ~P U. dom R <-> A C_ U. dom R ) )
23 21 22 syl 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> ( A e. ~P U. dom R <-> A C_ U. dom R ) )
24 18 23 mpbird 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> A e. ~P U. dom R )
25 xrltso 
 |-  < Or RR*
26 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
27 soss 
 |-  ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
28 26 27 ax-mp 
 |-  ( < Or RR* -> < Or ( 0 [,] +oo ) )
29 25 28 mp1i 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> < Or ( 0 [,] +oo ) )
30 29 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 )
31 6 13 24 30 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 ) , < ) )