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∈𝒫yx⁡z≤x⁡y∧∀y∈𝒫dom⁡xy≼ω→x⁡⋃y≤sum^⁡x↾y

Detailed syntax breakdown

Step Hyp Ref Expression
0 come classOutMeas
1 vx setvarx
2 1 cv setvarx
3 2 cdm classdom⁡x
4 cc0 class0
5 cicc class.
6 cpnf class+∞
7 4 6 5 co class0+∞
8 3 7 2 wf wffx:dom⁡x⟶0+∞
9 3 cuni class⋃dom⁡x
10 9 cpw class𝒫⋃dom⁡x
11 3 10 wceq wffdom⁡x=𝒫⋃dom⁡x
12 8 11 wa wffx:dom⁡x⟶0+∞∧dom⁡x=𝒫⋃dom⁡x
13 c0 class∅
14 13 2 cfv classx⁡∅
15 14 4 wceq wffx⁡∅=0
16 12 15 wa wffx:dom⁡x⟶0+∞∧dom⁡x=𝒫⋃dom⁡x∧x⁡∅=0
17 vy setvary
18 vz setvarz
19 17 cv setvary
20 19 cpw class𝒫y
21 18 cv setvarz
22 21 2 cfv classx⁡z
23 cle class≤
24 19 2 cfv classx⁡y
25 22 24 23 wbr wffx⁡z≤x⁡y
26 25 18 20 wral wff∀z∈𝒫yx⁡z≤x⁡y
27 26 17 10 wral wff∀y∈𝒫⋃dom⁡x∀z∈𝒫yx⁡z≤x⁡y
28 16 27 wa wffx:dom⁡x⟶0+∞∧dom⁡x=𝒫⋃dom⁡x∧x⁡∅=0∧∀y∈𝒫⋃dom⁡x∀z∈𝒫yx⁡z≤x⁡y
29 3 cpw class𝒫dom⁡x
30 cdom class≼
31 com classω
32 19 31 30 wbr wffy≼ω
33 19 cuni class⋃y
34 33 2 cfv classx⁡⋃y
35 csumge0 classsum^
36 2 19 cres classx↾y
37 36 35 cfv classsum^⁡x↾y
38 34 37 23 wbr wffx⁡⋃y≤sum^⁡x↾y
39 32 38 wi wffy≼ω→x⁡⋃y≤sum^⁡x↾y
40 39 17 29 wral wff∀y∈𝒫dom⁡xy≼ω→x⁡⋃y≤sum^⁡x↾y
41 28 40 wa wffx:dom⁡x⟶0+∞∧dom⁡x=𝒫⋃dom⁡x∧x⁡∅=0∧∀y∈𝒫⋃dom⁡x∀z∈𝒫yx⁡z≤x⁡y∧∀y∈𝒫dom⁡xy≼ω→x⁡⋃y≤sum^⁡x↾y
42 41 1 cab classx|x:dom⁡x⟶0+∞∧dom⁡x=𝒫⋃dom⁡x∧x⁡∅=0∧∀y∈𝒫⋃dom⁡x∀z∈𝒫yx⁡z≤x⁡y∧∀y∈𝒫dom⁡xy≼ω→x⁡⋃y≤sum^⁡x↾y
43 0 42 wceq wffOutMeas=x|x:dom⁡x⟶0+∞∧dom⁡x=𝒫⋃dom⁡x∧x⁡∅=0∧∀y∈𝒫⋃dom⁡x∀z∈𝒫yx⁡z≤x⁡y∧∀y∈𝒫dom⁡xy≼ω→x⁡⋃y≤sum^⁡x↾y