MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rankon Structured version   Unicode version

Theorem rankon 8148
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 `  A )  e.  On

Proof of Theorem rankon
StepHypRef Expression
1 rankf 8147 . 2  |-  rank : U. ( R1 " On ) --> On
2 0elon 4862 . 2  |-  (/)  e.  On
31, 2f0cli 5961 1  |-  ( rank `  A )  e.  On
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1836   U.cuni 4180   Oncon0 4809   "cima 4933   ` cfv 5513   R1cr1 8115   rankcrnk 8116
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-ral 2751  df-rex 2752  df-reu 2753  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4181  df-int 4217  df-iun 4262  df-br 4385  df-opab 4443  df-mpt 4444  df-tr 4478  df-eprel 4722  df-id 4726  df-po 4731  df-so 4732  df-fr 4769  df-we 4771  df-ord 4812  df-on 4813  df-lim 4814  df-suc 4815  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-om 6622  df-recs 6982  df-rdg 7016  df-r1 8117  df-rank 8118
This theorem is referenced by:  rankr1ai  8151  rankr1bg  8156  rankr1clem  8173  rankr1c  8174  rankpwi  8176  rankelb  8177  wfelirr  8178  rankval3b  8179  ranksnb  8180  rankr1a  8189  bndrank  8194  unbndrank  8195  rankunb  8203  rankprb  8204  rankuni2b  8206  rankuni  8216  rankuniss  8219  rankval4  8220  rankbnd2  8222  rankc1  8223  rankc2  8224  rankelun  8225  rankelpr  8226  rankelop  8227  rankmapu  8231  rankxplim  8232  rankxplim3  8234  rankxpsuc  8235  tcrank  8237  scottex  8238  scott0  8239  dfac12lem2  8459  hsmexlem5  8745  r1limwun  9047  wunex3  9052  rankcf  9088  grur1  9131  elhf2  30025  hfuni  30034  dfac11  31214
  Copyright terms: Public domain W3C validator