Theorem rankon 9708

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 9707	. 2 ⊢ rank:∪ (𝑅1 “ On)⟶On
2		0elon 6367	. 2 ⊢ ∅ ∈ On
3	1, 2	f0cli 7039	1 ⊢ (rank‘𝐴) ∈ On

Syntax hints:   ∈ wcel 2114  ∪ cuni 4840   “ cima 5623  Oncon0 6312  ‘cfv 6487  𝑅₁cr1 9675  rankcrnk 9676

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-ral 3050  df-rex 3060  df-reu 3341  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-int 4880  df-iun 4925  df-br 5075  df-opab 5137  df-mpt 5156  df-tr 5182  df-id 5515  df-eprel 5520  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6254  df-ord 6315  df-on 6316  df-lim 6317  df-suc 6318  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-r1 9677  df-rank 9678

This theorem is referenced by:  rankr1ai  9711  rankr1bg  9716  rankr1clem  9733  rankr1c  9734  rankpwi  9736  rankelb  9737  wfelirr  9738  rankval3b  9739  ranksnb  9740  rankr1a  9749  bndrank  9754  unbndrank  9755  rankunb  9763  rankprb  9764  rankuni2b  9766  rankuni  9776  rankuniss  9779  rankval4  9780  rankbnd2  9782  rankc1  9783  rankc2  9784  rankelun  9785  rankelpr  9786  rankelop  9787  rankmapu  9791  rankxplim  9792  rankxplim3  9794  rankxpsuc  9795  tcrank  9797  scottex  9798  scott0  9799  dfac12lem2  10056  hsmexlem5  10341  r1limwun  10648  wunex3  10653  rankcf  10689  grur1  10732  rankval4b  35231  onvf1odlem4  35276  elhf2  36345  hfuni  36354  dfac11  43478  gruex  44713