Metamath Proof Explorer

Definition df-card

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 for its value and cardval2 for a simpler version of its value. The principal theorem relating cardinality to equinumerosity is carden . Our notation is from Enderton. Other textbooks often use a double bar over the set to express this function. (Contributed by NM, 21-Oct-2003)

Ref Expression
Assertion df-card card = x V y On | y x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccrd class card
1 vx setvar x
2 cvv class V
3 vy setvar y
4 con0 class On
5 3 cv setvar y
6 cen class
7 1 cv setvar x
8 5 7 6 wbr wff y x
9 8 3 4 crab class y On | y x
10 9 cint class y On | y x
11 1 2 10 cmpt class x V y On | y x
12 0 11 wceq wff card = x V y On | y x