![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > onenon | Structured version Visualization version GIF version |
Description: Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
Ref | Expression |
---|---|
onenon | ⊢ (𝐴 ∈ On → 𝐴 ∈ dom card) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | enrefg 8882 | . 2 ⊢ (𝐴 ∈ On → 𝐴 ≈ 𝐴) | |
2 | isnumi 9840 | . 2 ⊢ ((𝐴 ∈ On ∧ 𝐴 ≈ 𝐴) → 𝐴 ∈ dom card) | |
3 | 1, 2 | mpdan 685 | 1 ⊢ (𝐴 ∈ On → 𝐴 ∈ dom card) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 class class class wbr 5103 dom cdm 5631 Oncon0 6315 ≈ cen 8838 cardccrd 9829 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5254 ax-nul 5261 ax-pow 5318 ax-pr 5382 ax-un 7664 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3927 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-int 4906 df-br 5104 df-opab 5166 df-mpt 5187 df-tr 5221 df-id 5529 df-eprel 5535 df-po 5543 df-so 5544 df-fr 5586 df-we 5588 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-ord 6318 df-on 6319 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-en 8842 df-card 9833 |
This theorem is referenced by: oncardval 9849 oncardid 9850 cardnn 9857 iscard 9869 carduni 9875 nnsdomel 9884 harsdom 9889 harsucnn 9892 pm54.43lem 9894 infxpenlem 9907 infxpidm2 9911 onssnum 9934 alephnbtwn 9965 alephnbtwn2 9966 alephordilem1 9967 alephord2 9970 alephsdom 9980 cardaleph 9983 infenaleph 9985 alephinit 9989 iunfictbso 10008 ficardun2 10096 ficardun2OLD 10097 pwsdompw 10098 infunsdom1 10107 ackbij2 10137 cfflb 10153 sdom2en01 10196 fin23lem22 10221 iunctb 10468 alephadd 10471 alephmul 10472 alephexp1 10473 alephsuc3 10474 canthp1lem2 10547 pwfseqlem4a 10555 pwfseqlem4 10556 pwfseqlem5 10557 gchaleph 10565 gchaleph2 10566 hargch 10567 cygctb 19622 ttac 41263 numinfctb 41333 isnumbasgrplem2 41334 isnumbasabl 41336 iscard4 41710 minregex2 41712 harval3 41715 harval3on 41716 aleph1min 41734 |
Copyright terms: Public domain | W3C validator |