Theorem cardid2

Description: Any numerable set is equinumerous to its cardinal number. Proposition 10.5 of TakeutiZaring p. 85. (Contributed by Mario Carneiro, 7-Jan-2013)

	Ref	Expression
Assertion	cardid2	|- ( A e. dom card -> ( card ` A ) ~~ A )

Proof

Step	Hyp	Ref	Expression
1		cardval3	|- ( A e. dom card -> ( card ` A ) = |^| { y e. On | y ~~ A } )
2		ssrab2	|- { y e. On | y ~~ A } C_ On
3		fvex	|- ( card ` A ) e. _V
4	1 3	eqeltrrdi	|- ( A e. dom card -> |^| { y e. On | y ~~ A } e. _V )
5		intex	|- ( { y e. On | y ~~ A } =/= (/) <-> |^| { y e. On | y ~~ A } e. _V )
6	4 5	sylibr	|- ( A e. dom card -> { y e. On | y ~~ A } =/= (/) )
7		onint	|- ( ( { y e. On | y ~~ A } C_ On /\ { y e. On | y ~~ A } =/= (/) ) -> |^| { y e. On | y ~~ A } e. { y e. On | y ~~ A } )
8	2 6 7	sylancr	|- ( A e. dom card -> |^| { y e. On | y ~~ A } e. { y e. On | y ~~ A } )
9	1 8	eqeltrd	|- ( A e. dom card -> ( card ` A ) e. { y e. On | y ~~ A } )
10		breq1	|- ( y = ( card ` A ) -> ( y ~~ A <-> ( card ` A ) ~~ A ) )
11	10	elrab	|- ( ( card ` A ) e. { y e. On | y ~~ A } <-> ( ( card ` A ) e. On /\ ( card ` A ) ~~ A ) )
12	11	simprbi	|- ( ( card ` A ) e. { y e. On | y ~~ A } -> ( card ` A ) ~~ A )
13	9 12	syl	|- ( A e. dom card -> ( card ` A ) ~~ A )