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