Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ome Structured version   Visualization version   GIF version

Definition df-ome 39380
 Description: Define the class of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Assertion
Ref Expression
df-ome OutMeas = {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦))))}
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-ome
StepHypRef Expression
1 come 39379 . 2 class OutMeas
2 vx . . . . . . . . . 10 setvar 𝑥
32cv 1474 . . . . . . . . 9 class 𝑥
43cdm 5038 . . . . . . . 8 class dom 𝑥
5 cc0 9815 . . . . . . . . 9 class 0
6 cpnf 9950 . . . . . . . . 9 class +∞
7 cicc 12049 . . . . . . . . 9 class [,]
85, 6, 7co 6549 . . . . . . . 8 class (0[,]+∞)
94, 8, 3wf 5800 . . . . . . 7 wff 𝑥:dom 𝑥⟶(0[,]+∞)
104cuni 4372 . . . . . . . . 9 class dom 𝑥
1110cpw 4108 . . . . . . . 8 class 𝒫 dom 𝑥
124, 11wceq 1475 . . . . . . 7 wff dom 𝑥 = 𝒫 dom 𝑥
139, 12wa 383 . . . . . 6 wff (𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥)
14 c0 3874 . . . . . . . 8 class
1514, 3cfv 5804 . . . . . . 7 class (𝑥‘∅)
1615, 5wceq 1475 . . . . . 6 wff (𝑥‘∅) = 0
1713, 16wa 383 . . . . 5 wff ((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0)
18 vz . . . . . . . . . 10 setvar 𝑧
1918cv 1474 . . . . . . . . 9 class 𝑧
2019, 3cfv 5804 . . . . . . . 8 class (𝑥𝑧)
21 vy . . . . . . . . . 10 setvar 𝑦
2221cv 1474 . . . . . . . . 9 class 𝑦
2322, 3cfv 5804 . . . . . . . 8 class (𝑥𝑦)
24 cle 9954 . . . . . . . 8 class
2520, 23, 24wbr 4583 . . . . . . 7 wff (𝑥𝑧) ≤ (𝑥𝑦)
2622cpw 4108 . . . . . . 7 class 𝒫 𝑦
2725, 18, 26wral 2896 . . . . . 6 wff 𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)
2827, 21, 11wral 2896 . . . . 5 wff 𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)
2917, 28wa 383 . . . 4 wff (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦))
30 com 6957 . . . . . . 7 class ω
31 cdom 7839 . . . . . . 7 class
3222, 30, 31wbr 4583 . . . . . 6 wff 𝑦 ≼ ω
3322cuni 4372 . . . . . . . 8 class 𝑦
3433, 3cfv 5804 . . . . . . 7 class (𝑥 𝑦)
353, 22cres 5040 . . . . . . . 8 class (𝑥𝑦)
36 csumge0 39255 . . . . . . . 8 class Σ^
3735, 36cfv 5804 . . . . . . 7 class ^‘(𝑥𝑦))
3834, 37, 24wbr 4583 . . . . . 6 wff (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦))
3932, 38wi 4 . . . . 5 wff (𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦)))
404cpw 4108 . . . . 5 class 𝒫 dom 𝑥
4139, 21, 40wral 2896 . . . 4 wff 𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦)))
4229, 41wa 383 . . 3 wff ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦))))
4342, 2cab 2596 . 2 class {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦))))}
441, 43wceq 1475 1 wff OutMeas = {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦))))}
 Colors of variables: wff setvar class This definition is referenced by:  isome  39384
 Copyright terms: Public domain W3C validator