Detailed syntax breakdown of Definition df-ptfin
Step | Hyp | Ref
| Expression |
1 | | cptfin 22039 |
. 2
class
PtFin |
2 | | vy |
. . . . . . 7
setvar 𝑦 |
3 | | vz |
. . . . . . 7
setvar 𝑧 |
4 | 2, 3 | wel 2106 |
. . . . . 6
wff 𝑦 ∈ 𝑧 |
5 | | vx |
. . . . . . 7
setvar 𝑥 |
6 | 5 | cv 1527 |
. . . . . 6
class 𝑥 |
7 | 4, 3, 6 | crab 3139 |
. . . . 5
class {𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} |
8 | | cfn 8497 |
. . . . 5
class
Fin |
9 | 7, 8 | wcel 2105 |
. . . 4
wff {𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin |
10 | 6 | cuni 4830 |
. . . 4
class ∪ 𝑥 |
11 | 9, 2, 10 | wral 3135 |
. . 3
wff
∀𝑦 ∈
∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin |
12 | 11, 5 | cab 2796 |
. 2
class {𝑥 ∣ ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin} |
13 | 1, 12 | wceq 1528 |
1
wff PtFin =
{𝑥 ∣ ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin} |