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

Theorem ordsson 4539
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  |-  ( Ord 
A  ->  A  C_  On )

Proof of Theorem ordsson
StepHypRef Expression
1 ordon 4532 . 2  |-  Ord  On
2 ordeleqon 4538 . . . . 5  |-  ( Ord 
A  <->  ( A  e.  On  \/  A  =  On ) )
32biimpi 188 . . . 4  |-  ( Ord 
A  ->  ( A  e.  On  \/  A  =  On ) )
43adantr 453 . . 3  |-  ( ( Ord  A  /\  Ord  On )  ->  ( A  e.  On  \/  A  =  On ) )
5 ordsseleq 4379 . . 3  |-  ( ( Ord  A  /\  Ord  On )  ->  ( A  C_  On  <->  ( A  e.  On  \/  A  =  On ) ) )
64, 5mpbird 225 . 2  |-  ( ( Ord  A  /\  Ord  On )  ->  A  C_  On )
71, 6mpan2 655 1  |-  ( Ord 
A  ->  A  C_  On )
Colors of variables: wff set class
Syntax hints:    -> wi 6    \/ wo 359    /\ wa 360    = wceq 1619    e. wcel 1621    C_ wss 3113   Ord word 4349   Oncon0 4350
This theorem is referenced by:  onss  4540  orduni  4543  ordsucuniel  4573  ordsucuni  4578  iordsmo  6328  tfr2b  6366  tz7.44-2  6374  ordiso2  7184  ordtypelem7  7193  ordtypelem8  7194  oiid  7210  r1tr  7402  r1ordg  7404  r1ord3g  7405  r1pwss  7410  r1val1  7412  rankwflemb  7419  r1elwf  7422  rankr1ai  7424  cflim2  7843  cfss  7845  cfslb  7846  cfslbn  7847  cfslb2n  7848  cofsmo  7849  coftr  7853  inaprc  8412  rdgprc  23506  tfrALTlem  23631  limsucncmpi  24245
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pr 4172  ax-un 4470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-rab 2525  df-v 2759  df-sbc 2953  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-pss 3129  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-tp 3608  df-op 3609  df-uni 3788  df-br 3984  df-opab 4038  df-tr 4074  df-eprel 4263  df-po 4272  df-so 4273  df-fr 4310  df-we 4312  df-ord 4353  df-on 4354
  Copyright terms: Public domain W3C validator