Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cardid2 Structured version   Visualization version   GIF version

Theorem cardid2 9374
 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 (𝐴 ∈ dom card → (card‘𝐴) ≈ 𝐴)

Proof of Theorem cardid2
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 cardval3 9373 . . 3 (𝐴 ∈ dom card → (card‘𝐴) = {𝑦 ∈ On ∣ 𝑦𝐴})
2 ssrab2 4059 . . . 4 {𝑦 ∈ On ∣ 𝑦𝐴} ⊆ On
3 fvex 6679 . . . . . 6 (card‘𝐴) ∈ V
41, 3syl6eqelr 2926 . . . . 5 (𝐴 ∈ dom card → {𝑦 ∈ On ∣ 𝑦𝐴} ∈ V)
5 intex 5236 . . . . 5 ({𝑦 ∈ On ∣ 𝑦𝐴} ≠ ∅ ↔ {𝑦 ∈ On ∣ 𝑦𝐴} ∈ V)
64, 5sylibr 235 . . . 4 (𝐴 ∈ dom card → {𝑦 ∈ On ∣ 𝑦𝐴} ≠ ∅)
7 onint 7501 . . . 4 (({𝑦 ∈ On ∣ 𝑦𝐴} ⊆ On ∧ {𝑦 ∈ On ∣ 𝑦𝐴} ≠ ∅) → {𝑦 ∈ On ∣ 𝑦𝐴} ∈ {𝑦 ∈ On ∣ 𝑦𝐴})
82, 6, 7sylancr 587 . . 3 (𝐴 ∈ dom card → {𝑦 ∈ On ∣ 𝑦𝐴} ∈ {𝑦 ∈ On ∣ 𝑦𝐴})
91, 8eqeltrd 2917 . 2 (𝐴 ∈ dom card → (card‘𝐴) ∈ {𝑦 ∈ On ∣ 𝑦𝐴})
10 breq1 5065 . . . 4 (𝑦 = (card‘𝐴) → (𝑦𝐴 ↔ (card‘𝐴) ≈ 𝐴))
1110elrab 3683 . . 3 ((card‘𝐴) ∈ {𝑦 ∈ On ∣ 𝑦𝐴} ↔ ((card‘𝐴) ∈ On ∧ (card‘𝐴) ≈ 𝐴))
1211simprbi 497 . 2 ((card‘𝐴) ∈ {𝑦 ∈ On ∣ 𝑦𝐴} → (card‘𝐴) ≈ 𝐴)
139, 12syl 17 1 (𝐴 ∈ dom card → (card‘𝐴) ≈ 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 3020  {crab 3146  Vcvv 3499   ⊆ wss 3939  ∅c0 4294  ∩ cint 4873   class class class wbr 5062  dom cdm 5553  Oncon0 6188  ‘cfv 6351   ≈ cen 8498  cardccrd 9356 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pr 5325  ax-un 7454 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-ord 6191  df-on 6192  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-fv 6359  df-en 8502  df-card 9360 This theorem is referenced by:  isnum3  9375  oncardid  9377  cardidm  9380  ficardom  9382  ficardid  9383  cardnn  9384  cardnueq0  9385  carden2a  9387  carden2b  9388  carddomi2  9391  sdomsdomcardi  9392  cardsdomelir  9394  cardsdomel  9395  infxpidm2  9435  dfac8b  9449  numdom  9456  alephnbtwn2  9490  alephsucdom  9497  infenaleph  9509  dfac12r  9564  cardadju  9612  pwsdompw  9618  cff1  9672  cfflb  9673  cflim2  9677  cfss  9679  cfslb  9680  domtriomlem  9856  cardid  9961  cardidg  9962  carden  9965  sdomsdomcard  9974  hargch  10087  gch2  10089  hashkf  13685
 Copyright terms: Public domain W3C validator