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

Theorem ordsson 6625
Description: Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38. (Contributed by NM, 18-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
Assertion
Ref Expression
ordsson

Proof of Theorem ordsson
StepHypRef Expression
1 ordon 6618 . 2
2 ordeleqon 6624 . . . . 5
32biimpi 194 . . . 4
43adantr 465 . . 3
5 ordsseleq 4912 . . 3
64, 5mpbird 232 . 2
71, 6mpan2 671 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368  /\wa 369  =wceq 1395  e.wcel 1818  C_wss 3475  Ordword 4882   con0 4883
This theorem is referenced by:  onss  6626  orduni  6629  ordsucuniel  6659  ordsucuni  6664  iordsmo  7047  tfr2b  7084  tz7.44-2  7092  ordiso2  7961  ordtypelem7  7970  ordtypelem8  7971  oiid  7987  r1tr  8215  r1ordg  8217  r1ord3g  8218  r1pwss  8223  r1val1  8225  rankwflemb  8232  r1elwf  8235  rankr1ai  8237  cflim2  8664  cfss  8666  cfslb  8667  cfslbn  8668  cfslb2n  8669  cofsmo  8670  coftr  8674  inaprc  9235  rdgprc  29227  limsucncmpi  29910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691  ax-un 6592
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-tr 4546  df-eprel 4796  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887
  Copyright terms: Public domain W3C validator