This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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