Detailed syntax breakdown of Definition df-mvr
Step | Hyp | Ref
| Expression |
1 | | cmvr 20888 |
. 2
class
mVar |
2 | | vi |
. . 3
setvar 𝑖 |
3 | | vr |
. . 3
setvar 𝑟 |
4 | | cvv 3420 |
. . 3
class
V |
5 | | vx |
. . . 4
setvar 𝑥 |
6 | 2 | cv 1542 |
. . . 4
class 𝑖 |
7 | | vf |
. . . . 5
setvar 𝑓 |
8 | | vh |
. . . . . . . . . 10
setvar ℎ |
9 | 8 | cv 1542 |
. . . . . . . . 9
class ℎ |
10 | 9 | ccnv 5564 |
. . . . . . . 8
class ◡ℎ |
11 | | cn 11854 |
. . . . . . . 8
class
ℕ |
12 | 10, 11 | cima 5568 |
. . . . . . 7
class (◡ℎ “ ℕ) |
13 | | cfn 8646 |
. . . . . . 7
class
Fin |
14 | 12, 13 | wcel 2111 |
. . . . . 6
wff (◡ℎ “ ℕ) ∈ Fin |
15 | | cn0 12114 |
. . . . . . 7
class
ℕ0 |
16 | | cmap 8528 |
. . . . . . 7
class
↑m |
17 | 15, 6, 16 | co 7231 |
. . . . . 6
class
(ℕ0 ↑m 𝑖) |
18 | 14, 8, 17 | crab 3066 |
. . . . 5
class {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} |
19 | 7 | cv 1542 |
. . . . . . 7
class 𝑓 |
20 | | vy |
. . . . . . . 8
setvar 𝑦 |
21 | 20, 5 | weq 1971 |
. . . . . . . . 9
wff 𝑦 = 𝑥 |
22 | | c1 10754 |
. . . . . . . . 9
class
1 |
23 | | cc0 10753 |
. . . . . . . . 9
class
0 |
24 | 21, 22, 23 | cif 4453 |
. . . . . . . 8
class if(𝑦 = 𝑥, 1, 0) |
25 | 20, 6, 24 | cmpt 5149 |
. . . . . . 7
class (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)) |
26 | 19, 25 | wceq 1543 |
. . . . . 6
wff 𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)) |
27 | 3 | cv 1542 |
. . . . . . 7
class 𝑟 |
28 | | cur 19540 |
. . . . . . 7
class
1r |
29 | 27, 28 | cfv 6397 |
. . . . . 6
class
(1r‘𝑟) |
30 | | c0g 16968 |
. . . . . . 7
class
0g |
31 | 27, 30 | cfv 6397 |
. . . . . 6
class
(0g‘𝑟) |
32 | 26, 29, 31 | cif 4453 |
. . . . 5
class if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟)) |
33 | 7, 18, 32 | cmpt 5149 |
. . . 4
class (𝑓 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟))) |
34 | 5, 6, 33 | cmpt 5149 |
. . 3
class (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟)))) |
35 | 2, 3, 4, 4, 34 | cmpo 7233 |
. 2
class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟))))) |
36 | 1, 35 | wceq 1543 |
1
wff mVar =
(𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟))))) |