Metamath Proof Explorer

Definition df-ome

Description: Define the class of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion df-ome 
|- OutMeas = { x | ( ( ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x = ~P U. dom x ) /\ ( x ` (/) ) = 0 ) /\ A. y e. ~P U. dom x A. z e. ~P y ( x ` z ) <_ ( x ` y ) ) /\ A. y e. ~P dom x ( y ~<_ _om -> ( x ` U. y ) <_ ( sum^ ` ( x |` y ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 come 
 |-  OutMeas
1 vx 
 |-  x
2 1 cv 
 |-  x
3 2 cdm 
 |-  dom x
4 cc0 
 |-  0
5 cicc 
 |-  [,]
6 cpnf 
 |-  +oo
7 4 6 5 co 
 |-  ( 0 [,] +oo )
8 3 7 2 wf 
 |-  x : dom x --> ( 0 [,] +oo )
9 3 cuni 
 |-  U. dom x
10 9 cpw 
 |-  ~P U. dom x
11 3 10 wceq 
 |-  dom x = ~P U. dom x
12 8 11 wa 
 |-  ( x : dom x --> ( 0 [,] +oo ) /\ dom x = ~P U. dom x )
13 c0 
 |-  (/)
14 13 2 cfv 
 |-  ( x ` (/) )
15 14 4 wceq 
 |-  ( x ` (/) ) = 0
16 12 15 wa 
 |-  ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x = ~P U. dom x ) /\ ( x ` (/) ) = 0 )
17 vy 
 |-  y
18 vz 
 |-  z
19 17 cv 
 |-  y
20 19 cpw 
 |-  ~P y
21 18 cv 
 |-  z
22 21 2 cfv 
 |-  ( x ` z )
23 cle 
 |-  <_
24 19 2 cfv 
 |-  ( x ` y )
25 22 24 23 wbr 
 |-  ( x ` z ) <_ ( x ` y )
26 25 18 20 wral 
 |-  A. z e. ~P y ( x ` z ) <_ ( x ` y )
27 26 17 10 wral 
 |-  A. y e. ~P U. dom x A. z e. ~P y ( x ` z ) <_ ( x ` y )
28 16 27 wa 
 |-  ( ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x = ~P U. dom x ) /\ ( x ` (/) ) = 0 ) /\ A. y e. ~P U. dom x A. z e. ~P y ( x ` z ) <_ ( x ` y ) )
29 3 cpw 
 |-  ~P dom x
30 cdom 
 |-  ~<_
31 com 
 |-  _om
32 19 31 30 wbr 
 |-  y ~<_ _om
33 19 cuni 
 |-  U. y
34 33 2 cfv 
 |-  ( x ` U. y )
35 csumge0 
 |-  sum^
36 2 19 cres 
 |-  ( x |` y )
37 36 35 cfv 
 |-  ( sum^ ` ( x |` y ) )
38 34 37 23 wbr 
 |-  ( x ` U. y ) <_ ( sum^ ` ( x |` y ) )
39 32 38 wi 
 |-  ( y ~<_ _om -> ( x ` U. y ) <_ ( sum^ ` ( x |` y ) ) )
40 39 17 29 wral 
 |-  A. y e. ~P dom x ( y ~<_ _om -> ( x ` U. y ) <_ ( sum^ ` ( x |` y ) ) )
41 28 40 wa 
 |-  ( ( ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x = ~P U. dom x ) /\ ( x ` (/) ) = 0 ) /\ A. y e. ~P U. dom x A. z e. ~P y ( x ` z ) <_ ( x ` y ) ) /\ A. y e. ~P dom x ( y ~<_ _om -> ( x ` U. y ) <_ ( sum^ ` ( x |` y ) ) ) )
42 41 1 cab 
 |-  { x | ( ( ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x = ~P U. dom x ) /\ ( x ` (/) ) = 0 ) /\ A. y e. ~P U. dom x A. z e. ~P y ( x ` z ) <_ ( x ` y ) ) /\ A. y e. ~P dom x ( y ~<_ _om -> ( x ` U. y ) <_ ( sum^ ` ( x |` y ) ) ) ) }
43 0 42 wceq 
 |-  OutMeas = { x | ( ( ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x = ~P U. dom x ) /\ ( x ` (/) ) = 0 ) /\ A. y e. ~P U. dom x A. z e. ~P y ( x ` z ) <_ ( x ` y ) ) /\ A. y e. ~P dom x ( y ~<_ _om -> ( x ` U. y ) <_ ( sum^ ` ( x |` y ) ) ) ) }