Detailed syntax breakdown of Definition df-oms
Step | Hyp | Ref
| Expression |
1 | | coms 31820 |
. 2
class
toOMeas |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | cvv 3397 |
. . 3
class
V |
4 | | va |
. . . 4
setvar 𝑎 |
5 | 2 | cv 1541 |
. . . . . . 7
class 𝑟 |
6 | 5 | cdm 5519 |
. . . . . 6
class dom 𝑟 |
7 | 6 | cuni 4793 |
. . . . 5
class ∪ dom 𝑟 |
8 | 7 | cpw 4485 |
. . . 4
class 𝒫
∪ dom 𝑟 |
9 | | vx |
. . . . . . 7
setvar 𝑥 |
10 | 4 | cv 1541 |
. . . . . . . . . 10
class 𝑎 |
11 | | vz |
. . . . . . . . . . . 12
setvar 𝑧 |
12 | 11 | cv 1541 |
. . . . . . . . . . 11
class 𝑧 |
13 | 12 | cuni 4793 |
. . . . . . . . . 10
class ∪ 𝑧 |
14 | 10, 13 | wss 3841 |
. . . . . . . . 9
wff 𝑎 ⊆ ∪ 𝑧 |
15 | | com 7593 |
. . . . . . . . . 10
class
ω |
16 | | cdom 8546 |
. . . . . . . . . 10
class
≼ |
17 | 12, 15, 16 | wbr 5027 |
. . . . . . . . 9
wff 𝑧 ≼
ω |
18 | 14, 17 | wa 399 |
. . . . . . . 8
wff (𝑎 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω) |
19 | 6 | cpw 4485 |
. . . . . . . 8
class 𝒫
dom 𝑟 |
20 | 18, 11, 19 | crab 3057 |
. . . . . . 7
class {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} |
21 | 9 | cv 1541 |
. . . . . . . 8
class 𝑥 |
22 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
23 | 22 | cv 1541 |
. . . . . . . . 9
class 𝑦 |
24 | 23, 5 | cfv 6333 |
. . . . . . . 8
class (𝑟‘𝑦) |
25 | 21, 24, 22 | cesum 31557 |
. . . . . . 7
class
Σ*𝑦
∈ 𝑥(𝑟‘𝑦) |
26 | 9, 20, 25 | cmpt 5107 |
. . . . . 6
class (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑟‘𝑦)) |
27 | 26 | crn 5520 |
. . . . 5
class ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑟‘𝑦)) |
28 | | cc0 10608 |
. . . . . 6
class
0 |
29 | | cpnf 10743 |
. . . . . 6
class
+∞ |
30 | | cicc 12817 |
. . . . . 6
class
[,] |
31 | 28, 29, 30 | co 7164 |
. . . . 5
class
(0[,]+∞) |
32 | | clt 10746 |
. . . . 5
class
< |
33 | 27, 31, 32 | cinf 8971 |
. . . 4
class inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑟‘𝑦)), (0[,]+∞), < ) |
34 | 4, 8, 33 | cmpt 5107 |
. . 3
class (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑟‘𝑦)), (0[,]+∞), < )) |
35 | 2, 3, 34 | cmpt 5107 |
. 2
class (𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑟‘𝑦)), (0[,]+∞), < ))) |
36 | 1, 35 | wceq 1542 |
1
wff toOMeas =
(𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑦 ∈
𝑥(𝑟‘𝑦)), (0[,]+∞), < ))) |