Theorem finnum 9764

Description: Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)

Assertion

Ref	Expression
finnum	⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card)

Proof of Theorem finnum

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfi 8802	. 2 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
2		nnon 7754	. . . 4 ⊢ (𝑥 ∈ ω → 𝑥 ∈ On)
3		ensym 8829	. . . 4 ⊢ (𝐴 ≈ 𝑥 → 𝑥 ≈ 𝐴)
4		isnumi 9762	. . . 4 ⊢ ((𝑥 ∈ On ∧ 𝑥 ≈ 𝐴) → 𝐴 ∈ dom card)
5	2, 3, 4	syl2an 596	. . 3 ⊢ ((𝑥 ∈ ω ∧ 𝐴 ≈ 𝑥) → 𝐴 ∈ dom card)
6	5	rexlimiva 3139	. 2 ⊢ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 → 𝐴 ∈ dom card)
7	1, 6	sylbi 216	1 ⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card)

Syntax hints:   → wi 4   ∈ wcel 2103  ∃wrex 3069   class class class wbr 5080  dom cdm 5600  Oncon0 6281  ωcom 7748   ≈ cen 8766  Fincfn 8769  cardccrd 9751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-10 2134  ax-11 2151  ax-12 2168  ax-ext 2706  ax-sep 5231  ax-nul 5238  ax-pow 5296  ax-pr 5360  ax-un 7621

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2727  df-clel 2813  df-nfc 2885  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3357  df-v 3438  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4844  df-int 4886  df-br 5081  df-opab 5143  df-mpt 5164  df-tr 5198  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-ord 6284  df-on 6285  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-om 7749  df-er 8534  df-en 8770  df-fin 8773  df-card 9755

This theorem is referenced by:  ficardom  9777  ficardid  9778  fidomtri  9809  numwdom  9875  fodomfi2  9876  dfac12k  9963  ficardunOLD  10017  ficardun2  10018  ficardun2OLD  10019  pwsdompw  10020  ackbij2  10059  sdom2en01  10118  dfacfin7  10215  fin1a2lem9  10224  domtriomlem  10258  zornn0g  10321  canthnum  10465  pwfseqlem4  10478  uzindi  13762  hashkf  14106  hashgval  14107  hashen  14121  hashdom  14153  symggen  19137  pgpfac1lem5  19741  fiufl  23130  fineqvacALT  33163  finixpnum  35820  poimirlem32  35867  ttac  41067