Theorem cardid2 9984

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.

Step	Hyp	Ref	Expression
1		cardval3 9983	. . 3 ⊢ (𝐴 ∈ dom card → (card‘𝐴) = ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴})
2		ssrab2 4077	. . . 4 ⊢ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ⊆ On
3		fvex 6915	. . . . . 6 ⊢ (card‘𝐴) ∈ V
4	1, 3	eqeltrrdi 2838	. . . . 5 ⊢ (𝐴 ∈ dom card → ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ∈ V)
5		intex 5343	. . . . 5 ⊢ ({𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ≠ ∅ ↔ ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ∈ V)
6	4, 5	sylibr 233	. . . 4 ⊢ (𝐴 ∈ dom card → {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ≠ ∅)
7		onint 7799	. . . 4 ⊢ (({𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ⊆ On ∧ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ≠ ∅) → ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴})
8	2, 6, 7	sylancr 585	. . 3 ⊢ (𝐴 ∈ dom card → ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴})
9	1, 8	eqeltrd 2829	. 2 ⊢ (𝐴 ∈ dom card → (card‘𝐴) ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴})
10		breq1 5155	. . . 4 ⊢ (𝑦 = (card‘𝐴) → (𝑦 ≈ 𝐴 ↔ (card‘𝐴) ≈ 𝐴))
11	10	elrab 3684	. . 3 ⊢ ((card‘𝐴) ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} ↔ ((card‘𝐴) ∈ On ∧ (card‘𝐴) ≈ 𝐴))
12	11	simprbi 495	. 2 ⊢ ((card‘𝐴) ∈ {𝑦 ∈ On ∣ 𝑦 ≈ 𝐴} → (card‘𝐴) ≈ 𝐴)
13	9, 12	syl 17	1 ⊢ (𝐴 ∈ dom card → (card‘𝐴) ≈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2098   ≠ wne 2937  {crab 3430  Vcvv 3473   ⊆ wss 3949  ∅c0 4326  ∩ cint 4953   class class class wbr 5152  dom cdm 5682  Oncon0 6374  ‘cfv 6553   ≈ cen 8967  cardccrd 9966

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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-ord 6377  df-on 6378  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-fv 6561  df-en 8971  df-card 9970

This theorem is referenced by:  isnum3  9985  oncardid  9987  cardidm  9990  ficardom  9992  ficardid  9993  cardnn  9994  cardnueq0  9995  carden2a  9997  carden2b  9998  carddomi2  10001  sdomsdomcardi  10002  cardsdomelir  10004  cardsdomel  10005  infxpidm2  10048  dfac8b  10062  numdom  10069  alephnbtwn2  10103  alephsucdom  10110  infenaleph  10122  dfac12r  10177  cardadju  10225  pwsdompw  10235  cff1  10289  cfflb  10290  cflim2  10294  cfss  10296  cfslb  10297  domtriomlem  10473  cardid  10578  cardidg  10579  carden  10582  sdomsdomcard  10591  hargch  10704  gch2  10706  hashkf  14331