Definition df-card 4803

Description: Define the cardinal number function. The cardinal number of a set is the least ordinal number equinumerous to it. In other words, it is the "size" of the set. Definition of [Enderton] p. 197. See cardval 4813 for its value, cardval2 4842 for a simpler version of its value. The principle theorem relating cardinality to equinumerosity is carden 4818. Our notation is from Enderton. Other textbooks often use a double bar over the set to express this function.

Assertion

Ref	Expression
df-card	|- card = {<.x, y>. | y = |^|{z e. On | z ~~ x}}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-card

Step	Hyp	Ref	Expression
1		ccrd 4800	. 2 class card
2		vy	. . . . 5 set y
3	2	cv 954	. . . 4 class y
4		vz	. . . . . . . 8 set z
5	4	cv 954	. . . . . . 7 class z
6		vx	. . . . . . . 8 set x
7	6	cv 954	. . . . . . 7 class x
8		cen 4361	. . . . . . 7 class ~~
9	5, 7, 8	wbr 2616	. . . . . 6 wff z ~~ x
10		con0 2945	. . . . . 6 class On
11	9, 4, 10	crab 1647	. . . . 5 class {z e. On | z ~~ x}
12	11	cint 2530	. . . 4 class |^|{z e. On | z ~~ x}
13	3, 12	wceq 955	. . 3 wff y = |^|{z e. On | z ~~ x}
14	13, 6, 2	copab 2663	. 2 class {<.x, y>. | y = |^|{z e. On | z ~~ x}}
15	1, 14	wceq 955	1 wff card = {<.x, y>. | y = |^|{z e. On | z ~~ x}}

This definition is referenced by:  oncardval 4806  cardval 4813

Copyright terms: Public domain