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 39180
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 39179 . 2 class OutMeas
2 vx . . . . . . . . . 10 setvar 𝑥
32cv 1473 . . . . . . . . 9 class 𝑥
43cdm 5024 . . . . . . . 8 class dom 𝑥
5 cc0 9788 . . . . . . . . 9 class 0
6 cpnf 9923 . . . . . . . . 9 class +∞
7 cicc 12001 . . . . . . . . 9 class [,]
85, 6, 7co 6523 . . . . . . . 8 class (0[,]+∞)
94, 8, 3wf 5782 . . . . . . 7 wff 𝑥:dom 𝑥⟶(0[,]+∞)
104cuni 4362 . . . . . . . . 9 class dom 𝑥
1110cpw 4103 . . . . . . . 8 class 𝒫 dom 𝑥
124, 11wceq 1474 . . . . . . 7 wff dom 𝑥 = 𝒫 dom 𝑥
139, 12wa 382 . . . . . 6 wff (𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥)
14 c0 3869 . . . . . . . 8 class
1514, 3cfv 5786 . . . . . . 7 class (𝑥‘∅)
1615, 5wceq 1474 . . . . . 6 wff (𝑥‘∅) = 0
1713, 16wa 382 . . . . 5 wff ((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0)
18 vz . . . . . . . . . 10 setvar 𝑧
1918cv 1473 . . . . . . . . 9 class 𝑧
2019, 3cfv 5786 . . . . . . . 8 class (𝑥𝑧)
21 vy . . . . . . . . . 10 setvar 𝑦
2221cv 1473 . . . . . . . . 9 class 𝑦
2322, 3cfv 5786 . . . . . . . 8 class (𝑥𝑦)
24 cle 9927 . . . . . . . 8 class
2520, 23, 24wbr 4573 . . . . . . 7 wff (𝑥𝑧) ≤ (𝑥𝑦)
2622cpw 4103 . . . . . . 7 class 𝒫 𝑦
2725, 18, 26wral 2891 . . . . . 6 wff 𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)
2827, 21, 11wral 2891 . . . . 5 wff 𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)
2917, 28wa 382 . . . 4 wff (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦))
30 com 6930 . . . . . . 7 class ω
31 cdom 7812 . . . . . . 7 class
3222, 30, 31wbr 4573 . . . . . 6 wff 𝑦 ≼ ω
3322cuni 4362 . . . . . . . 8 class 𝑦
3433, 3cfv 5786 . . . . . . 7 class (𝑥 𝑦)
353, 22cres 5026 . . . . . . . 8 class (𝑥𝑦)
36 csumge0 39055 . . . . . . . 8 class Σ^
3735, 36cfv 5786 . . . . . . 7 class ^‘(𝑥𝑦))
3834, 37, 24wbr 4573 . . . . . 6 wff (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦))
3932, 38wi 4 . . . . 5 wff (𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦)))
404cpw 4103 . . . . 5 class 𝒫 dom 𝑥
4139, 21, 40wral 2891 . . . 4 wff 𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦)))
4229, 41wa 382 . . 3 wff ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦))))
4342, 2cab 2591 . 2 class {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦))))}
441, 43wceq 1474 1 wff OutMeas = {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥𝑧 ∈ 𝒫 𝑦(𝑥𝑧) ≤ (𝑥𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥 𝑦) ≤ (Σ^‘(𝑥𝑦))))}
Colors of variables: wff setvar class
This definition is referenced by:  isome  39184
  Copyright terms: Public domain W3C validator