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 ) )