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

Theorem onelss 4757
Description: An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
onelss  |-  ( A  e.  On  ->  ( B  e.  A  ->  B 
C_  A ) )

Proof of Theorem onelss
StepHypRef Expression
1 eloni 4725 . 2  |-  ( A  e.  On  ->  Ord  A )
2 ordelss 4731 . . 3  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  C_  A )
32ex 434 . 2  |-  ( Ord 
A  ->  ( B  e.  A  ->  B  C_  A ) )
41, 3syl 16 1  |-  ( A  e.  On  ->  ( B  e.  A  ->  B 
C_  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761    C_ wss 3325   Ord word 4714   Oncon0 4715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-v 2972  df-in 3332  df-ss 3339  df-uni 4089  df-tr 4383  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719
This theorem is referenced by:  ordunidif  4763  onelssi  4823  ssorduni  6396  suceloni  6423  tfisi  6468  tfrlem9  6840  tfrlem11  6843  oaordex  6993  oaass  6996  odi  7014  omass  7015  oewordri  7027  nnaordex  7073  domtriord  7453  hartogs  7754  card2on  7765  tskwe  8116  infxpenlem  8176  cfub  8414  cfsuc  8422  coflim  8426  hsmexlem2  8592  ondomon  8723  pwcfsdom  8743  inar1  8938  tskord  8943  grudomon  8980  gruina  8981  dfrdg2  27522  poseq  27627  sltres  27718  nobndup  27754  nobnddown  27755  aomclem6  29321
  Copyright terms: Public domain W3C validator