Theorem onenon 9171

Description: Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)

Assertion

Ref	Expression
onenon	⊢ (𝐴 ∈ On → 𝐴 ∈ dom card)

Proof of Theorem onenon

Step	Hyp	Ref	Expression
1		enrefg 8337	. 2 ⊢ (𝐴 ∈ On → 𝐴 ≈ 𝐴)
2		isnumi 9168	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐴 ≈ 𝐴) → 𝐴 ∈ dom card)
3	1, 2	mpdan 675	1 ⊢ (𝐴 ∈ On → 𝐴 ∈ dom card)

Syntax hints:   → wi 4   ∈ wcel 2051   class class class wbr 4926  dom cdm 5404  Oncon0 6027   ≈ cen 8302  cardccrd 9157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-sbc 3677  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-int 4747  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-ord 6030  df-on 6031  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-en 8306  df-card 9161

This theorem is referenced by:  oncardval  9177  oncardid  9178  cardnn  9185  iscard  9197  carduni  9203  nnsdomel  9212  harsdom  9217  pm54.43lem  9221  infxpenlem  9232  infxpidm2  9236  onssnum  9259  alephnbtwn  9290  alephnbtwn2  9291  alephordilem1  9292  alephord2  9295  alephsdom  9305  cardaleph  9308  infenaleph  9310  alephinit  9314  iunfictbso  9333  ficardun2  9422  pwsdompw  9423  infunsdom1  9432  ackbij2  9462  cfflb  9478  sdom2en01  9521  fin23lem22  9546  iunctb  9793  alephadd  9796  alephmul  9797  alephexp1  9798  alephsuc3  9799  canthp1lem2  9872  pwfseqlem4a  9880  pwfseqlem4  9881  pwfseqlem5  9882  gchaleph  9890  gchaleph2  9891  hargch  9892  cygctb  18779  ttac  39063  numinfctb  39133  isnumbasgrplem2  39134  isnumbasabl  39136