Detailed syntax breakdown of Definition df-evl1
Step | Hyp | Ref
| Expression |
1 | | ce1 19679 |
. 2
class
eval1 |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | cvv 3200 |
. . 3
class
V |
4 | | vb |
. . . 4
setvar 𝑏 |
5 | 2 | cv 1482 |
. . . . 5
class 𝑟 |
6 | | cbs 15857 |
. . . . 5
class
Base |
7 | 5, 6 | cfv 5888 |
. . . 4
class
(Base‘𝑟) |
8 | | vx |
. . . . . 6
setvar 𝑥 |
9 | 4 | cv 1482 |
. . . . . . 7
class 𝑏 |
10 | | c1o 7553 |
. . . . . . . 8
class
1𝑜 |
11 | | cmap 7857 |
. . . . . . . 8
class
↑𝑚 |
12 | 9, 10, 11 | co 6650 |
. . . . . . 7
class (𝑏 ↑𝑚
1𝑜) |
13 | 9, 12, 11 | co 6650 |
. . . . . 6
class (𝑏 ↑𝑚
(𝑏
↑𝑚 1𝑜)) |
14 | 8 | cv 1482 |
. . . . . . 7
class 𝑥 |
15 | | vy |
. . . . . . . 8
setvar 𝑦 |
16 | 15 | cv 1482 |
. . . . . . . . . 10
class 𝑦 |
17 | 16 | csn 4177 |
. . . . . . . . 9
class {𝑦} |
18 | 10, 17 | cxp 5112 |
. . . . . . . 8
class
(1𝑜 × {𝑦}) |
19 | 15, 9, 18 | cmpt 4729 |
. . . . . . 7
class (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})) |
20 | 14, 19 | ccom 5118 |
. . . . . 6
class (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦}))) |
21 | 8, 13, 20 | cmpt 4729 |
. . . . 5
class (𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) |
22 | | cevl 19505 |
. . . . . 6
class
eval |
23 | 10, 5, 22 | co 6650 |
. . . . 5
class
(1𝑜 eval 𝑟) |
24 | 21, 23 | ccom 5118 |
. . . 4
class ((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) ∘
(1𝑜 eval 𝑟)) |
25 | 4, 7, 24 | csb 3533 |
. . 3
class
⦋(Base‘𝑟) / 𝑏⦌((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) ∘
(1𝑜 eval 𝑟)) |
26 | 2, 3, 25 | cmpt 4729 |
. 2
class (𝑟 ∈ V ↦
⦋(Base‘𝑟) / 𝑏⦌((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) ∘
(1𝑜 eval 𝑟))) |
27 | 1, 26 | wceq 1483 |
1
wff
eval1 = (𝑟 ∈ V ↦
⦋(Base‘𝑟) / 𝑏⦌((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) ∘
(1𝑜 eval 𝑟))) |