![]() |
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 9023 | . 2 ⊢ (𝐴 ∈ On → 𝐴 ≈ 𝐴) | |
2 | isnumi 9984 | . 2 ⊢ ((𝐴 ∈ On ∧ 𝐴 ≈ 𝐴) → 𝐴 ∈ dom card) | |
3 | 1, 2 | mpdan 687 | 1 ⊢ (𝐴 ∈ On → 𝐴 ∈ dom card) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 class class class wbr 5148 dom cdm 5689 Oncon0 6386 ≈ cen 8981 cardccrd 9973 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-int 4952 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-ord 6389 df-on 6390 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-en 8985 df-card 9977 |
This theorem is referenced by: oncardval 9993 oncardid 9994 cardnn 10001 iscard 10013 carduni 10019 nnsdomel 10028 harsdom 10033 harsucnn 10036 pm54.43lem 10038 infxpenlem 10051 infxpidm2 10055 onssnum 10078 alephnbtwn 10109 alephnbtwn2 10110 alephordilem1 10111 alephord2 10114 alephsdom 10124 cardaleph 10127 infenaleph 10129 alephinit 10133 iunfictbso 10152 ficardun2 10240 pwsdompw 10241 infunsdom1 10250 ackbij2 10280 cfflb 10297 sdom2en01 10340 fin23lem22 10365 iunctb 10612 alephadd 10615 alephmul 10616 alephexp1 10617 alephsuc3 10618 canthp1lem2 10691 pwfseqlem4a 10699 pwfseqlem4 10700 pwfseqlem5 10701 gchaleph 10709 gchaleph2 10710 hargch 10711 cygctb 19925 ttac 43025 numinfctb 43092 isnumbasgrplem2 43093 isnumbasabl 43095 iscard4 43523 minregex2 43525 harval3 43528 harval3on 43529 aleph1min 43547 |
Copyright terms: Public domain | W3C validator |