Definition df-card 5862

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 5975 for its value, cardval2 6007 for a simpler version of its value. The principle theorem relating cardinality to equinumerosity is carden 5981. 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 5859	. 2 class card
2		vy	. . . . 5 set y
3	2	cv 1297	. . . 4 class y
4		vz	. . . . . . . 8 set z
5	4	cv 1297	. . . . . . 7 class z
6		vx	. . . . . . . 8 set x
7	6	cv 1297	. . . . . . 7 class x
8		cen 5423	. . . . . . 7 class ~~
9	5, 7, 8	wbr 3338	. . . . . 6 wff z ~~ x
10		con0 3657	. . . . . 6 class On
11	9, 4, 10	crab 2108	. . . . 5 class {z e. On | z ~~ x}
12	11	cint 3214	. . . 4 class |^|{z e. On | z ~~ x}
13	3, 12	wceq 1298	. . 3 wff y = |^|{z e. On | z ~~ x}
14	13, 6, 2	copab 3395	. 2 class {<.x, y>. | y = |^|{z e. On | z ~~ x}}
15	1, 14	wceq 1298	1 wff card = {<.x, y>. | y = |^|{z e. On | z ~~ x}}

This definition is referenced by:  oncardval 5865  cardval 5975  hashgval 8230

Copyright terms: Public domain