Users' Mathboxes 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 43999
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 43998 . 2 class OutMeas
2 vx . . . . . . . . . 10 setvar 𝑥
32cv 1541 . . . . . . . . 9 class 𝑥
43cdm 5590 . . . . . . . 8 class dom 𝑥
5 cc0 10872 . . . . . . . . 9 class 0
6 cpnf 11007 . . . . . . . . 9 class +∞
7 cicc 13081 . . . . . . . . 9 class [,]
85, 6, 7co 7271 . . . . . . . 8 class (0[,]+∞)
94, 8, 3wf 6428 . . . . . . 7 wff 𝑥:dom 𝑥⟶(0[,]+∞)
104cuni 4845 . . . . . . . . 9 class dom 𝑥
1110cpw 4539 . . . . . . . 8 class 𝒫 dom 𝑥
124, 11wceq 1542 . . . . . . 7 wff dom 𝑥 = 𝒫 dom 𝑥
139, 12wa 396 . . . . . 6 wff (𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥)
14 c0 4262 . . . . . . . 8 class
1514, 3cfv 6432 . . . . . . 7 class (𝑥‘∅)
1615, 5wceq 1542 . . . . . 6 wff (𝑥‘∅) = 0
1713, 16wa 396 . . . . 5 wff ((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0)
18 vz . . . . . . . . . 10 setvar 𝑧
1918cv 1541 . . . . . . . . 9 class 𝑧
2019, 3cfv 6432 . . . . . . . 8 class (𝑥𝑧)
21 vy . . . . . . . . . 10 setvar 𝑦
2221cv 1541 . . . . . . . . 9 class 𝑦
2322, 3cfv 6432 . . . . . . . 8 class (𝑥𝑦)
24 cle 11011 . . . . . . . 8 class
2520, 23, 24wbr 5079 . . . . . . 7 wff (𝑥𝑧) ≤ (𝑥𝑦)
2622cpw 4539 . . . . . . 7 class 𝒫 𝑦
2725, 18, 26wral 3066 . . . . . 6 wff 𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)
2827, 21, 11wral 3066 . . . . 5 wff 𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)
2917, 28wa 396 . . . 4 wff (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦))
30 com 7706 . . . . . . 7 class ω
31 cdom 8714 . . . . . . 7 class
3222, 30, 31wbr 5079 . . . . . 6 wff 𝑦 ≼ ω
3322cuni 4845 . . . . . . . 8 class 𝑦
3433, 3cfv 6432 . . . . . . 7 class (𝑥 𝑦)
353, 22cres 5592 . . . . . . . 8 class (𝑥𝑦)
36 csumge0 43871 . . . . . . . 8 class Σ^
3735, 36cfv 6432 . . . . . . 7 class ^‘(𝑥𝑦))
3834, 37, 24wbr 5079 . . . . . 6 wff (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦))
3932, 38wi 4 . . . . 5 wff (𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦)))
404cpw 4539 . . . . 5 class 𝒫 dom 𝑥
4139, 21, 40wral 3066 . . . 4 wff 𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦)))
4229, 41wa 396 . . 3 wff ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦))))
4342, 2cab 2717 . 2 class {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦))))}
441, 43wceq 1542 1 wff OutMeas = {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦))))}
Colors of variables: wff setvar class
This definition is referenced by:  isome  44003
  Copyright terms: Public domain W3C validator