Detailed syntax breakdown of Definition df-fsupp
Step | Hyp | Ref
| Expression |
1 | | cfsupp 8275 |
. 2
class
finSupp |
2 | | vr |
. . . . . 6
setvar 𝑟 |
3 | 2 | cv 1482 |
. . . . 5
class 𝑟 |
4 | 3 | wfun 5882 |
. . . 4
wff Fun 𝑟 |
5 | | vz |
. . . . . . 7
setvar 𝑧 |
6 | 5 | cv 1482 |
. . . . . 6
class 𝑧 |
7 | | csupp 7295 |
. . . . . 6
class
supp |
8 | 3, 6, 7 | co 6650 |
. . . . 5
class (𝑟 supp 𝑧) |
9 | | cfn 7955 |
. . . . 5
class
Fin |
10 | 8, 9 | wcel 1990 |
. . . 4
wff (𝑟 supp 𝑧) ∈ Fin |
11 | 4, 10 | wa 384 |
. . 3
wff (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin) |
12 | 11, 2, 5 | copab 4712 |
. 2
class
{〈𝑟, 𝑧〉 ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)} |
13 | 1, 12 | wceq 1483 |
1
wff finSupp =
{〈𝑟, 𝑧〉 ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)} |