Detailed syntax breakdown of Definition df-ome
Step | Hyp | Ref
| Expression |
1 | | come 43998 |
. 2
class
OutMeas |
2 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
3 | 2 | cv 1541 |
. . . . . . . . 9
class 𝑥 |
4 | 3 | cdm 5590 |
. . . . . . . 8
class dom 𝑥 |
5 | | cc0 10872 |
. . . . . . . . 9
class
0 |
6 | | cpnf 11007 |
. . . . . . . . 9
class
+∞ |
7 | | cicc 13081 |
. . . . . . . . 9
class
[,] |
8 | 5, 6, 7 | co 7271 |
. . . . . . . 8
class
(0[,]+∞) |
9 | 4, 8, 3 | wf 6428 |
. . . . . . 7
wff 𝑥:dom 𝑥⟶(0[,]+∞) |
10 | 4 | cuni 4845 |
. . . . . . . . 9
class ∪ dom 𝑥 |
11 | 10 | cpw 4539 |
. . . . . . . 8
class 𝒫
∪ dom 𝑥 |
12 | 4, 11 | wceq 1542 |
. . . . . . 7
wff dom 𝑥 = 𝒫 ∪ dom 𝑥 |
13 | 9, 12 | wa 396 |
. . . . . 6
wff (𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) |
14 | | c0 4262 |
. . . . . . . 8
class
∅ |
15 | 14, 3 | cfv 6432 |
. . . . . . 7
class (𝑥‘∅) |
16 | 15, 5 | wceq 1542 |
. . . . . 6
wff (𝑥‘∅) =
0 |
17 | 13, 16 | wa 396 |
. . . . 5
wff ((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) |
18 | | vz |
. . . . . . . . . 10
setvar 𝑧 |
19 | 18 | cv 1541 |
. . . . . . . . 9
class 𝑧 |
20 | 19, 3 | cfv 6432 |
. . . . . . . 8
class (𝑥‘𝑧) |
21 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
22 | 21 | cv 1541 |
. . . . . . . . 9
class 𝑦 |
23 | 22, 3 | cfv 6432 |
. . . . . . . 8
class (𝑥‘𝑦) |
24 | | cle 11011 |
. . . . . . . 8
class
≤ |
25 | 20, 23, 24 | wbr 5079 |
. . . . . . 7
wff (𝑥‘𝑧) ≤ (𝑥‘𝑦) |
26 | 22 | cpw 4539 |
. . . . . . 7
class 𝒫
𝑦 |
27 | 25, 18, 26 | wral 3066 |
. . . . . 6
wff
∀𝑧 ∈
𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦) |
28 | 27, 21, 11 | wral 3066 |
. . . . 5
wff
∀𝑦 ∈
𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦) |
29 | 17, 28 | wa 396 |
. . . 4
wff (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) |
30 | | com 7706 |
. . . . . . 7
class
ω |
31 | | cdom 8714 |
. . . . . . 7
class
≼ |
32 | 22, 30, 31 | wbr 5079 |
. . . . . 6
wff 𝑦 ≼
ω |
33 | 22 | cuni 4845 |
. . . . . . . 8
class ∪ 𝑦 |
34 | 33, 3 | cfv 6432 |
. . . . . . 7
class (𝑥‘∪ 𝑦) |
35 | 3, 22 | cres 5592 |
. . . . . . . 8
class (𝑥 ↾ 𝑦) |
36 | | csumge0 43871 |
. . . . . . . 8
class
Σ^ |
37 | 35, 36 | cfv 6432 |
. . . . . . 7
class
(Σ^‘(𝑥 ↾ 𝑦)) |
38 | 34, 37, 24 | wbr 5079 |
. . . . . 6
wff (𝑥‘∪ 𝑦)
≤ (Σ^‘(𝑥 ↾ 𝑦)) |
39 | 32, 38 | wi 4 |
. . . . 5
wff (𝑦 ≼ ω → (𝑥‘∪ 𝑦)
≤ (Σ^‘(𝑥 ↾ 𝑦))) |
40 | 4 | cpw 4539 |
. . . . 5
class 𝒫
dom 𝑥 |
41 | 39, 21, 40 | wral 3066 |
. . . 4
wff
∀𝑦 ∈
𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦)
≤ (Σ^‘(𝑥 ↾ 𝑦))) |
42 | 29, 41 | wa 396 |
. . 3
wff ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦)))) |
43 | 42, 2 | cab 2717 |
. 2
class {𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))))} |
44 | 1, 43 | wceq 1542 |
1
wff OutMeas =
{𝑥 ∣ ((((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 = 𝒫 ∪ dom 𝑥) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 ∪ dom 𝑥∀𝑧 ∈ 𝒫 𝑦(𝑥‘𝑧) ≤ (𝑥‘𝑦)) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥(𝑦 ≼ ω → (𝑥‘∪ 𝑦) ≤
(Σ^‘(𝑥 ↾ 𝑦))))} |