Description: The cardinality function is a function with domain the well-orderable sets. Assuming AC, this is the universe. (Contributed by Mario Carneiro, 6-Jun-2013) (Revised by Mario Carneiro, 13-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | cardf | |- card : _V --> On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cardf2 | |- card : { x | E. y e. On y ~~ x } --> On |
|
2 | 1 | fdmi | |- dom card = { x | E. y e. On y ~~ x } |
3 | cardeqv | |- dom card = _V |
|
4 | 2 3 | eqtr3i | |- { x | E. y e. On y ~~ x } = _V |
5 | 4 | feq2i | |- ( card : { x | E. y e. On y ~~ x } --> On <-> card : _V --> On ) |
6 | 1 5 | mpbi | |- card : _V --> On |