Theorem onenon 10011

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 8995	. 2 ⊢ (𝐴 ∈ On → 𝐴 ≈ 𝐴)
2		isnumi 10008	. 2 ⊢ ((𝐴 ∈ On ∧ 𝐴 ≈ 𝐴) → 𝐴 ∈ dom card)
3	1, 2	mpdan 700	1 ⊢ (𝐴 ∈ On → 𝐴 ∈ dom card)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  dom cdm 5651  Oncon0 6355   ≈ cen 8954  cardccrd 9997

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-ord 6358  df-on 6359  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-en 8958  df-card 10001

This theorem is used by:  oncardval  10017  oncardid  10018  cardnn  10025  iscard  10037  carduni  10043  nnsdomel  10052  harsdom  10057  harsucnn  10060  pm54.43lem  10062  infxpenlem  10073  infxpidm2  10077  onssnum  10100  alephnbtwn  10131  alephnbtwn2  10132  alephordilem1  10133  alephord2  10136  alephsdom  10146  cardaleph  10149  infenaleph  10151  alephinit  10155  iunfictbso  10174  ficardun2  10261  pwsdompw  10262  infunsdom1  10271  ackbij2  10301  cfflb  10318  sdom2en01  10361  fin23lem22  10386  iunctb  10640  alephadd  10643  alephmul  10644  alephexp1  10645  alephsuc3  10646  canthp1lem2  10719  pwfseqlem4a  10727  pwfseqlem4  10728  pwfseqlem5  10729  gchaleph  10737  gchaleph2  10738  hargch  10739  cygctb  20086  ttac  43996  numinfctb  44063  isnumbasgrplem2  44064  isnumbasabl  44066  iscard4  44492  minregex2  44494  harval3  44497  harval3on  44498  aleph1min  44516