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	Could not format assertion : No typesetting found for |- kard = ( x e. _V |-> Scott { y | y ~~ x } ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ckard	Could not format kard : No typesetting found for class kard with typecode class
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vy	$$setvary$$
4	3	cv	$$setvary$$
5		cen	$$class\approx$$
6	1	cv	$$setvarx$$
7	4 6 5	wbr	$$wffy\approx x$$
8	7 3	cab	$$class\left\{y|y\approx x\right\}$$
9	8	cscott	$$classScott\left\{y|y\approx x\right\}$$
10	1 2 9	cmpt	$$class\left(x\in \mathrm{V}⟼Scott\left\{y|y\approx x\right\}\right)$$
11	0 10	wceq	Could not format kard = ( x e. _V |-> Scott { y | y ~~ x } ) : No typesetting found for wff kard = ( x e. _V |-> Scott { y | y ~~ x } ) with typecode wff