Theorem rankon 9017

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.)

Assertion

Ref	Expression
rankon	⊢ (rank‘𝐴) ∈ On

Proof of Theorem rankon

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

Syntax hints:   ∈ wcel 2051  ∪ cuni 4709   “ cima 5407  Oncon0 6027  ‘cfv 6186  𝑅₁cr1 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