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 e. _V |-> |^| { y e. On | y ~~ x } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccrd
 |-  card
1 vx
 |-  x
2 cvv
 |-  _V
3 vy
 |-  y
4 con0
 |-  On
5 3 cv
 |-  y
6 cen
 |-  ~~
7 1 cv
 |-  x
8 5 7 6 wbr
 |-  y ~~ x
9 8 3 4 crab
 |-  { y e. On | y ~~ x }
10 9 cint
 |-  |^| { y e. On | y ~~ x }
11 1 2 10 cmpt
 |-  ( x e. _V |-> |^| { y e. On | y ~~ x } )
12 0 11 wceq
 |-  card = ( x e. _V |-> |^| { y e. On | y ~~ x } )