Definition df-card 3623

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 3633 for its value, cardval2 3661 for a simpler version of its value. The principle theorem relating cardinality to equinumerosity is carden 3638. 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(s):   x,y,z

Detailed syntax breakdown of Definition df-card

Step	Hyp	Ref	Expression
1		ccrd 3620	. 2 class card
2		vy	. . . . 5 set y
3	2	cv 1089	. . . 4 class y
4		vz	. . . . . . . 8 set z
5	4	cv 1089	. . . . . . 7 class z
6		vx	. . . . . . . 8 set x
7	6	cv 1089	. . . . . . 7 class x
8		cen 3271	. . . . . . 7 class ~~
9	5, 7, 8	wbr 2054	. . . . . 6 wff z ~~ x
10		con0 2199	. . . . . 6 class On
11	9, 4, 10	crab 1204	. . . . 5 class {z e. On | z ~~ x}
12	11	cint 1965	. . . 4 class |^|{z e. On | z ~~ x}
13	3, 12	wceq 1091	. . 3 wff y = |^|{z e. On | z ~~ x}
14	13, 6, 2	copab 2055	. 2 class {<.x, y>. | y = |^|{z e. On | z ~~ x}}
15	1, 14	wceq 1091	1 wff card = {<.x, y>. | y = |^|{z e. On | z ~~ x}}

This definition is referenced by:  oncardval 3626  cardval 3633

metamath.org