Theorem cardid2 8405

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

Assertion

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

Proof of Theorem cardid2

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cardval3 8404	. . 3 |- ( A e. dom card -> ( card ` A ) = |^| { y e. On | y ~~ A } )
2		ssrab2 3500	. . . 4 |- { y e. On | y ~~ A } C_ On
3		fvex 5889	. . . . . 6 |- ( card ` A ) e. _V
4	1, 3	syl6eqelr 2558	. . . . 5 |- ( A e. dom card -> |^| { y e. On | y ~~ A } e. _V )
5		intex 4557	. . . . 5 |- ( { y e. On | y ~~ A } =/= (/) <-> |^| { y e. On | y ~~ A } e. _V )
6	4, 5	sylibr 217	. . . 4 |- ( A e. dom card -> { y e. On | y ~~ A } =/= (/) )
7		onint 6641	. . . 4 |- ( ( { 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 676	. . 3 |- ( A e. dom card -> |^| { y e. On | y ~~ A } e. { y e. On | y ~~ A } )
9	1, 8	eqeltrd 2549	. 2 |- ( A e. dom card -> ( card ` A ) e. { y e. On | y ~~ A } )
10		breq1 4398	. . . 4 |- ( y = ( card ` A ) -> ( y ~~ A <-> ( card ` A ) ~~ A ) )
11	10	elrab 3184	. . 3 |- ( ( card ` A ) e. { y e. On | y ~~ A } <-> ( ( card ` A ) e. On /\ ( card ` A ) ~~ A ) )
12	11	simprbi 471	. 2 |- ( ( card ` A ) e. { y e. On | y ~~ A } -> ( card ` A ) ~~ A )
13	9, 12	syl 17	1 |- ( A e. dom card -> ( card ` A ) ~~ A )

Syntax hints:   -> wi 4   e. wcel 1904   =/= wne 2641   {crab 2760   _Vcvv 3031   C_ wss 3390   (/)c0 3722   |^|cint 4226   class class class wbr 4395   dom cdm 4839   Oncon0 5430   ` cfv 5589   ~~ cen 7584   cardccrd 8387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639  ax-un 6602

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-ord 5433  df-on 5434  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-fv 5597  df-en 7588  df-card 8391

This theorem is referenced by:  isnum3  8406  oncardid  8408  cardidm  8411  ficardom  8413  ficardid  8414  cardnn  8415  cardnueq0  8416  carden2a  8418  carden2b  8419  carddomi2  8422  sdomsdomcardi  8423  cardsdomelir  8425  cardsdomel  8426  infxpidm2  8466  dfac8b  8480  numdom  8487  alephnbtwn2  8521  alephsucdom  8528  infenaleph  8540  dfac12r  8594  cardacda  8646  pwsdompw  8652  cff1  8706  cfflb  8707  cflim2  8711  cfss  8713  cfslb  8714  domtriomlem  8890  cardid  8990  cardidg  8991  carden  8994  sdomsdomcard  9003  hargch  9116  gch2  9118  hashkf  12555