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

Metamath Proof Explorer

Theorem oncard

Description: A set is a cardinal number iff it equals its own cardinal number. Proposition 10.9 of TakeutiZaring p. 85. (Contributed by Mario Carneiro, 7-Jan-2013)

Ref Expression
Assertion oncard 
|- ( E. x A = ( card ` x ) <-> A = ( card ` A ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A = ( card ` x ) -> A = ( card ` x ) )
2 fveq2 
 |-  ( A = ( card ` x ) -> ( card ` A ) = ( card ` ( card ` x ) ) )
3 cardidm 
 |-  ( card ` ( card ` x ) ) = ( card ` x )
4 2 3 eqtrdi 
 |-  ( A = ( card ` x ) -> ( card ` A ) = ( card ` x ) )
5 1 4 eqtr4d 
 |-  ( A = ( card ` x ) -> A = ( card ` A ) )
6 5 exlimiv 
 |-  ( E. x A = ( card ` x ) -> A = ( card ` A ) )
7 fvex 
 |-  ( card ` A ) e. _V
8 eleq1 
 |-  ( A = ( card ` A ) -> ( A e. _V <-> ( card ` A ) e. _V ) )
9 7 8 mpbiri 
 |-  ( A = ( card ` A ) -> A e. _V )
10 fveq2 
 |-  ( x = A -> ( card ` x ) = ( card ` A ) )
11 10 eqeq2d 
 |-  ( x = A -> ( A = ( card ` x ) <-> A = ( card ` A ) ) )
12 11 spcegv 
 |-  ( A e. _V -> ( A = ( card ` A ) -> E. x A = ( card ` x ) ) )
13 9 12 mpcom 
 |-  ( A = ( card ` A ) -> E. x A = ( card ` x ) )
14 6 13 impbii 
 |-  ( E. x A = ( card ` x ) <-> A = ( card ` A ) )