Detailed syntax breakdown of Definition df-evls1
Step | Hyp | Ref
| Expression |
1 | | ces1 21477 |
. 2
class
evalSub1 |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | vr |
. . 3
setvar 𝑟 |
4 | | cvv 3431 |
. . 3
class
V |
5 | 2 | cv 1541 |
. . . . 5
class 𝑠 |
6 | | cbs 16910 |
. . . . 5
class
Base |
7 | 5, 6 | cfv 6432 |
. . . 4
class
(Base‘𝑠) |
8 | 7 | cpw 4539 |
. . 3
class 𝒫
(Base‘𝑠) |
9 | | vb |
. . . 4
setvar 𝑏 |
10 | | vx |
. . . . . 6
setvar 𝑥 |
11 | 9 | cv 1541 |
. . . . . . 7
class 𝑏 |
12 | | c1o 8281 |
. . . . . . . 8
class
1o |
13 | | cmap 8598 |
. . . . . . . 8
class
↑m |
14 | 11, 12, 13 | co 7271 |
. . . . . . 7
class (𝑏 ↑m
1o) |
15 | 11, 14, 13 | co 7271 |
. . . . . 6
class (𝑏 ↑m (𝑏 ↑m
1o)) |
16 | 10 | cv 1541 |
. . . . . . 7
class 𝑥 |
17 | | vy |
. . . . . . . 8
setvar 𝑦 |
18 | 17 | cv 1541 |
. . . . . . . . . 10
class 𝑦 |
19 | 18 | csn 4567 |
. . . . . . . . 9
class {𝑦} |
20 | 12, 19 | cxp 5588 |
. . . . . . . 8
class
(1o × {𝑦}) |
21 | 17, 11, 20 | cmpt 5162 |
. . . . . . 7
class (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})) |
22 | 16, 21 | ccom 5594 |
. . . . . 6
class (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦}))) |
23 | 10, 15, 22 | cmpt 5162 |
. . . . 5
class (𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) |
24 | 3 | cv 1541 |
. . . . . 6
class 𝑟 |
25 | | ces 21278 |
. . . . . . 7
class
evalSub |
26 | 12, 5, 25 | co 7271 |
. . . . . 6
class
(1o evalSub 𝑠) |
27 | 24, 26 | cfv 6432 |
. . . . 5
class
((1o evalSub 𝑠)‘𝑟) |
28 | 23, 27 | ccom 5594 |
. . . 4
class ((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟)) |
29 | 9, 7, 28 | csb 3837 |
. . 3
class
⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟)) |
30 | 2, 3, 4, 8, 29 | cmpo 7273 |
. 2
class (𝑠 ∈ V, 𝑟 ∈ 𝒫 (Base‘𝑠) ↦
⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟))) |
31 | 1, 30 | wceq 1542 |
1
wff
evalSub1 = (𝑠
∈ V, 𝑟 ∈
𝒫 (Base‘𝑠)
↦ ⦋(Base‘𝑠) / 𝑏⦌((𝑥 ∈ (𝑏 ↑m (𝑏 ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1o × {𝑦})))) ∘ ((1o
evalSub 𝑠)‘𝑟))) |