![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rankon | Structured version Visualization version GIF version |
Description: The rank of a set is an ordinal number. Proposition 9.15(1) of [TakeutiZaring] p. 79. (Contributed by NM, 5-Oct-2003.) (Revised by Mario Carneiro, 12-Sep-2013.) |
Ref | Expression |
---|---|
rankon | ⊢ (rank‘𝐴) ∈ On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rankf 9016 | . 2 ⊢ rank:∪ (𝑅1 “ On)⟶On | |
2 | 0elon 6080 | . 2 ⊢ ∅ ∈ On | |
3 | 1, 2 | f0cli 6686 | 1 ⊢ (rank‘𝐴) ∈ On |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2051 ∪ cuni 4709 “ cima 5407 Oncon0 6027 ‘cfv 6186 𝑅1cr1 8984 rankcrnk 8985 |
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-reu 3090 df-rab 3092 df-v 3412 df-sbc 3677 df-csb 3782 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-iun 4791 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-pred 5984 df-ord 6030 df-on 6031 df-lim 6032 df-suc 6033 df-iota 6150 df-fun 6188 df-fn 6189 df-f 6190 df-f1 6191 df-fo 6192 df-f1o 6193 df-fv 6194 df-om 7396 df-wrecs 7749 df-recs 7811 df-rdg 7849 df-r1 8986 df-rank 8987 |
This theorem is referenced by: rankr1ai 9020 rankr1bg 9025 rankr1clem 9042 rankr1c 9043 rankpwi 9045 rankelb 9046 wfelirr 9047 rankval3b 9048 ranksnb 9049 rankr1a 9058 bndrank 9063 unbndrank 9064 rankunb 9072 rankprb 9073 rankuni2b 9075 rankuni 9085 rankuniss 9088 rankval4 9089 rankbnd2 9091 rankc1 9092 rankc2 9093 rankelun 9094 rankelpr 9095 rankelop 9096 rankmapu 9100 rankxplim 9101 rankxplim3 9103 rankxpsuc 9104 tcrank 9106 scottex 9107 scott0 9108 dfac12lem2 9363 hsmexlem5 9649 r1limwun 9955 wunex3 9960 rankcf 9996 grur1 10039 elhf2 33190 hfuni 33199 dfac11 39092 gruex 40043 |
Copyright terms: Public domain | W3C validator |