Definition df-kard

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 for its value. The principal theorem relating this type of cardinality to equinumerosity is kardeng . Our notation is from Enderton and differentiates this function from the standard cardinal size function defined in df-card . (Contributed by BTernaryTau, 2-Jul-2026)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ckard	⊢ kard
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4	3	cv	⊢ 𝑦
5		cen	⊢ ≈
6	1	cv	⊢ 𝑥
7	4 6 5	wbr	⊢ 𝑦 ≈ 𝑥
8	7 3	cab	⊢ { 𝑦 ∣ 𝑦 ≈ 𝑥 }
9	8	cscott	⊢ Scott { 𝑦 ∣ 𝑦 ≈ 𝑥 }
10	1 2 9	cmpt	⊢ ( 𝑥 ∈ V ↦ Scott { 𝑦 ∣ 𝑦 ≈ 𝑥 } )
11	0 10	wceq	⊢ kard = ( 𝑥 ∈ V ↦ Scott { 𝑦 ∣ 𝑦 ≈ 𝑥 } )