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

Metamath Proof Explorer

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 )