Detailed syntax breakdown of Definition df-fsupp
Step | Hyp | Ref
| Expression |
1 | | cfsupp 9098 |
. 2
class
finSupp |
2 | | vr |
. . . . . 6
setvar 𝑟 |
3 | 2 | cv 1541 |
. . . . 5
class 𝑟 |
4 | 3 | wfun 6425 |
. . . 4
wff Fun 𝑟 |
5 | | vz |
. . . . . . 7
setvar 𝑧 |
6 | 5 | cv 1541 |
. . . . . 6
class 𝑧 |
7 | | csupp 7962 |
. . . . . 6
class
supp |
8 | 3, 6, 7 | co 7269 |
. . . . 5
class (𝑟 supp 𝑧) |
9 | | cfn 8708 |
. . . . 5
class
Fin |
10 | 8, 9 | wcel 2110 |
. . . 4
wff (𝑟 supp 𝑧) ∈ Fin |
11 | 4, 10 | wa 396 |
. . 3
wff (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin) |
12 | 11, 2, 5 | copab 5141 |
. 2
class
{〈𝑟, 𝑧〉 ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)} |
13 | 1, 12 | wceq 1542 |
1
wff finSupp =
{〈𝑟, 𝑧〉 ∣ (Fun 𝑟 ∧ (𝑟 supp 𝑧) ∈ Fin)} |