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 +∞ dom x = 𝒫 dom x x = 0 y 𝒫 dom x z 𝒫 y x z x y y 𝒫 dom x y ω x y sum^ x y

Detailed syntax breakdown

Step Hyp Ref Expression
0 come class OutMeas
1 vx setvar x
2 1 cv setvar x
3 2 cdm class dom x
4 cc0 class 0
5 cicc class .
6 cpnf class +∞
7 4 6 5 co class 0 +∞
8 3 7 2 wf wff x : dom x 0 +∞
9 3 cuni class dom x
10 9 cpw class 𝒫 dom x
11 3 10 wceq wff dom x = 𝒫 dom x
12 8 11 wa wff x : dom x 0 +∞ dom x = 𝒫 dom x
13 c0 class
14 13 2 cfv class x
15 14 4 wceq wff x = 0
16 12 15 wa wff x : dom x 0 +∞ dom x = 𝒫 dom x x = 0
17 vy setvar y
18 vz setvar z
19 17 cv setvar y
20 19 cpw class 𝒫 y
21 18 cv setvar z
22 21 2 cfv class x z
23 cle class
24 19 2 cfv class x y
25 22 24 23 wbr wff x z x y
26 25 18 20 wral wff z 𝒫 y x z x y
27 26 17 10 wral wff y 𝒫 dom x z 𝒫 y x z x y
28 16 27 wa wff x : dom x 0 +∞ dom x = 𝒫 dom x x = 0 y 𝒫 dom x z 𝒫 y x z x y
29 3 cpw class 𝒫 dom x
30 cdom class
31 com class ω
32 19 31 30 wbr wff y ω
33 19 cuni class y
34 33 2 cfv class x y
35 csumge0 class sum^
36 2 19 cres class x y
37 36 35 cfv class sum^ x y
38 34 37 23 wbr wff x y sum^ x y
39 32 38 wi wff y ω x y sum^ x y
40 39 17 29 wral wff y 𝒫 dom x y ω x y sum^ x y
41 28 40 wa wff x : dom x 0 +∞ dom x = 𝒫 dom x x = 0 y 𝒫 dom x z 𝒫 y x z x y y 𝒫 dom x y ω x y sum^ x y
42 41 1 cab class x | x : dom x 0 +∞ dom x = 𝒫 dom x x = 0 y 𝒫 dom x z 𝒫 y x z x y y 𝒫 dom x y ω x y sum^ x y
43 0 42 wceq wff OutMeas = x | x : dom x 0 +∞ dom x = 𝒫 dom x x = 0 y 𝒫 dom x z 𝒫 y x z x y y 𝒫 dom x y ω x y sum^ x y