Metamath Proof Explorer


Theorem cardprc

Description: The class of all cardinal numbers is not a set (i.e. is a proper class). Theorem 19.8 of Eisenberg p. 310. In this proof (which does not use AC), we cannot use Cantor's construction canth3 to ensure that there is always a cardinal larger than a given cardinal, but we can use Hartogs' construction hartogs to construct (effectively) ( alephsuc A ) from ( alephA ) , which achieves the same thing. (Contributed by Mario Carneiro, 22-Jan-2013)

Ref Expression
Assertion cardprc
|- { x | ( card ` x ) = x } e/ _V

Proof

Step Hyp Ref Expression
1 fveq2
 |-  ( x = y -> ( card ` x ) = ( card ` y ) )
2 id
 |-  ( x = y -> x = y )
3 1 2 eqeq12d
 |-  ( x = y -> ( ( card ` x ) = x <-> ( card ` y ) = y ) )
4 3 cbvabv
 |-  { x | ( card ` x ) = x } = { y | ( card ` y ) = y }
5 4 cardprclem
 |-  -. { x | ( card ` x ) = x } e. _V
6 5 nelir
 |-  { x | ( card ` x ) = x } e/ _V