Definition df-kard 35496

Description: Define the alternative cardinal number function. Under this definition, the cardinal number of a set is the set of all sets equinumerous to it and having the least possible rank. Definition of [Enderton] p. 222. See kardval 35498 for its value. The principal theorem relating this type of cardinality to equinumerosity is kardeng 35503. Our notation is from Enderton and differentiates this function from the standard cardinal size function defined in df-card 9925. (Contributed by BTernaryTau, 2-Jul-2026.)

Assertion

Ref	Expression
df-kard	⊢ kard = (𝑥 ∈ V ↦ Scott {𝑦 ∣ 𝑦 ≈ 𝑥})

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-kard

Step	Hyp	Ref	Expression
1		ckard 35495	. 2 class kard
2		vx	. . 3 setvar 𝑥
3		cvv 3463	. . 3 class V
4		vy	. . . . . . 7 setvar 𝑦
5	4	cv 1566	. . . . . 6 class 𝑦
6	2	cv 1566	. . . . . 6 class 𝑥
7		cen 8940	. . . . . 6 class ≈
8	5, 6, 7	wbr 5113	. . . . 5 wff 𝑦 ≈ 𝑥
9	8, 4	cab 2747	. . . 4 class {𝑦 ∣ 𝑦 ≈ 𝑥}
10	9	cscott 9857	. . 3 class Scott {𝑦 ∣ 𝑦 ≈ 𝑥}
11	2, 3, 10	cmpt 5196	. 2 class (𝑥 ∈ V ↦ Scott {𝑦 ∣ 𝑦 ≈ 𝑥})
12	1, 11	wceq 1567	1 wff kard = (𝑥 ∈ V ↦ Scott {𝑦 ∣ 𝑦 ≈ 𝑥})

This definition is referenced by:  kardfn  35497  kardval  35498  kard0  35500