Metamath Proof Explorer

Theorem omscl

Description: A closure lemma for the constructed outer measure. (Contributed by Thierry Arnoux, 17-Sep-2019)

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

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 simp2 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) -> R : Q --> ( 0 [,] +oo ) )
3 2 ad2antrr 
 |-  ( ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) /\ y e. x ) -> R : Q --> ( 0 [,] +oo ) )
4 ssrab2 
 |-  { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } C_ ~P dom R
5 simpr 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) -> x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } )
6 4 5 sseldi 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) -> x e. ~P dom R )
7 fdm 
 |-  ( R : Q --> ( 0 [,] +oo ) -> dom R = Q )
8 7 pweqd 
 |-  ( R : Q --> ( 0 [,] +oo ) -> ~P dom R = ~P Q )
9 2 8 syl 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) -> ~P dom R = ~P Q )
10 9 adantr 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) -> ~P dom R = ~P Q )
11 6 10 eleqtrd 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) -> x e. ~P Q )
12 elpwi 
 |-  ( x e. ~P Q -> x C_ Q )
13 11 12 syl 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) -> x C_ Q )
14 13 sselda 
 |-  ( ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) /\ y e. x ) -> y e. Q )
15 3 14 ffvelrnd 
 |-  ( ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) /\ y e. x ) -> ( R ` y ) e. ( 0 [,] +oo ) )
16 15 ralrimiva 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) -> A. y e. x ( R ` y ) e. ( 0 [,] +oo ) )
17 nfcv 
 |-  F/_ y x
18 17 esumcl 
 |-  ( ( x e. _V /\ A. y e. x ( R ` y ) e. ( 0 [,] +oo ) ) -> sum* y e. x ( R ` y ) e. ( 0 [,] +oo ) )
19 1 16 18 sylancr 
 |-  ( ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) -> sum* y e. x ( R ` y ) e. ( 0 [,] +oo ) )
20 19 ralrimiva 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A e. ~P U. dom R ) -> A. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } sum* y e. x ( R ` y ) e. ( 0 [,] +oo ) )
21 eqid 
 |-  ( 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 ) )
22 21 rnmptss 
 |-  ( A. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } sum* y e. x ( R ` y ) e. ( 0 [,] +oo ) -> ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) C_ ( 0 [,] +oo ) )
23 20 22 syl 
 |-  ( ( 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 ) )