Theorem rankon 9714

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

Syntax hints:   ∈ wcel 2114  ∪ cuni 4851   “ cima 5629  Oncon0 6319  ‘cfv 6494  𝑅₁cr1 9681  rankcrnk 9682

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 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5521  df-eprel 5526  df-po 5534  df-so 5535  df-fr 5579  df-we 5581  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-pred 6261  df-ord 6322  df-on 6323  df-lim 6324  df-suc 6325  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-ov 7365  df-om 7813  df-2nd 7938  df-frecs 8226  df-wrecs 8257  df-recs 8306  df-rdg 8344  df-r1 9683  df-rank 9684

This theorem is referenced by:  rankr1ai  9717  rankr1bg  9722  rankr1clem  9739  rankr1c  9740  rankpwi  9742  rankelb  9743  wfelirr  9744  rankval3b  9745  ranksnb  9746  rankr1a  9755  bndrank  9760  unbndrank  9761  rankunb  9769  rankprb  9770  rankuni2b  9772  rankuni  9782  rankuniss  9785  rankval4  9786  rankbnd2  9788  rankc1  9789  rankc2  9790  rankelun  9791  rankelpr  9792  rankelop  9793  rankmapu  9797  rankxplim  9798  rankxplim3  9800  rankxpsuc  9801  tcrank  9803  scottex  9804  scott0  9805  dfac12lem2  10062  hsmexlem5  10347  r1limwun  10654  wunex3  10659  rankcf  10695  grur1  10738  rankval4b  35263  onvf1odlem4  35308  elhf2  36377  hfuni  36386  dfac11  43514  gruex  44749