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 dom card card A A

Proof

Step Hyp Ref Expression
1 cardval3 A dom card card A = y On | y A
2 ssrab2 y On | y A On
3 fvex card A V
4 1 3 eqeltrrdi A dom card y On | y A V
5 intex y On | y A y On | y A V
6 4 5 sylibr A dom card y On | y A
7 onint y On | y A On y On | y A y On | y A y On | y A
8 2 6 7 sylancr A dom card y On | y A y On | y A
9 1 8 eqeltrd A dom card card A y On | y A
10 breq1 y = card A y A card A A
11 10 elrab card A y On | y A card A On card A A
12 11 simprbi card A y On | y A card A A
13 9 12 syl A dom card card A A