Definition df-ome 40704

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

Assertion

Ref	Expression
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 ) <_ (Σ^ ` ( x |` y ) ) ) ) }

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-ome

Step	Hyp	Ref	Expression
1		come 40703	. 2 class OutMeas
2		vx	. . . . . . . . . 10 setvar x
3	2	cv 1482	. . . . . . . . 9 class x
4	3	cdm 5114	. . . . . . . 8 class dom x
5		cc0 9936	. . . . . . . . 9 class 0
6		cpnf 10071	. . . . . . . . 9 class +oo
7		cicc 12178	. . . . . . . . 9 class [,]
8	5, 6, 7	co 6650	. . . . . . . 8 class ( 0 [,] +oo )
9	4, 8, 3	wf 5884	. . . . . . 7 wff x : dom x --> ( 0 [,] +oo )
10	4	cuni 4436	. . . . . . . . 9 class U. dom x
11	10	cpw 4158	. . . . . . . 8 class ~P U. dom x
12	4, 11	wceq 1483	. . . . . . 7 wff dom x = ~P U. dom x
13	9, 12	wa 384	. . . . . 6 wff ( x : dom x --> ( 0 [,] +oo ) /\ dom x = ~P U. dom x )
14		c0 3915	. . . . . . . 8 class (/)
15	14, 3	cfv 5888	. . . . . . 7 class ( x ` (/) )
16	15, 5	wceq 1483	. . . . . 6 wff ( x ` (/) ) = 0
17	13, 16	wa 384	. . . . 5 wff ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x = ~P U. dom x ) /\ ( x ` (/) ) = 0 )
18		vz	. . . . . . . . . 10 setvar z
19	18	cv 1482	. . . . . . . . 9 class z
20	19, 3	cfv 5888	. . . . . . . 8 class ( x ` z )
21		vy	. . . . . . . . . 10 setvar y
22	21	cv 1482	. . . . . . . . 9 class y
23	22, 3	cfv 5888	. . . . . . . 8 class ( x ` y )
24		cle 10075	. . . . . . . 8 class <_
25	20, 23, 24	wbr 4653	. . . . . . 7 wff ( x ` z ) <_ ( x ` y )
26	22	cpw 4158	. . . . . . 7 class ~P y
27	25, 18, 26	wral 2912	. . . . . 6 wff A. z e. ~P y ( x ` z ) <_ ( x ` y )
28	27, 21, 11	wral 2912	. . . . 5 wff A. y e. ~P U. dom x A. z e. ~P y ( x ` z ) <_ ( x ` y )
29	17, 28	wa 384	. . . 4 wff ( ( ( 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 ) )
30		com 7065	. . . . . . 7 class om
31		cdom 7953	. . . . . . 7 class ~<_
32	22, 30, 31	wbr 4653	. . . . . 6 wff y ~<_ om
33	22	cuni 4436	. . . . . . . 8 class U. y
34	33, 3	cfv 5888	. . . . . . 7 class ( x ` U. y )
35	3, 22	cres 5116	. . . . . . . 8 class ( x |` y )
36		csumge0 40579	. . . . . . . 8 class Σ^
37	35, 36	cfv 5888	. . . . . . 7 class (Σ^ ` ( x |` y ) )
38	34, 37, 24	wbr 4653	. . . . . 6 wff ( x ` U. y ) <_ (Σ^ ` ( x |` y ) )
39	32, 38	wi 4	. . . . 5 wff ( y ~<_ om -> ( x ` U. y ) <_ (Σ^ ` ( x |` y ) ) )
40	4	cpw 4158	. . . . 5 class ~P dom x
41	39, 21, 40	wral 2912	. . . 4 wff A. y e. ~P dom x ( y ~<_ om -> ( x ` U. y ) <_ (Σ^ ` ( x |` y ) ) )
42	29, 41	wa 384	. . 3 wff ( ( ( ( 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 ) <_ (Σ^ ` ( x |` y ) ) ) )
43	42, 2	cab 2608	. 2 class { 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 ) <_ (Σ^ ` ( x |` y ) ) ) ) }
44	1, 43	wceq 1483	1 wff 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 ) <_ (Σ^ ` ( x |` y ) ) ) ) }

This definition is referenced by:  isome  40708