Definition df-kard 35622

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 35624 for its value. The principal theorem relating this type of cardinality to equinumerosity is kardeng 35629. Our notation is from Enderton and differentiates this function from the standard cardinal size function defined in df-card 9941. (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 35621	. 2 class kard
2		vx	. . 3 setvar 𝑥
3		cvv 3457	. . 3 class V
4		vy	. . . . . . 7 setvar 𝑦
5	4	cv 1569	. . . . . 6 class 𝑦
6	2	cv 1569	. . . . . 6 class 𝑥
7		cen 8946	. . . . . 6 class ≈
8	5, 6, 7	wbr 5111	. . . . 5 wff 𝑦 ≈ 𝑥
9	8, 4	cab 2743	. . . 4 class {𝑦 ∣ 𝑦 ≈ 𝑥}
10	9	cscott 9864	. . 3 class Scott {𝑦 ∣ 𝑦 ≈ 𝑥}
11	2, 3, 10	cmpt 5194	. 2 class (𝑥 ∈ V ↦ Scott {𝑦 ∣ 𝑦 ≈ 𝑥})
12	1, 11	wceq 1570	1 wff kard = (𝑥 ∈ V ↦ Scott {𝑦 ∣ 𝑦 ≈ 𝑥})

This definition is used by:  kardfn  35623  kardval  35624  kard0  35626