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

Theorem onelss 4872
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 4840 . 2  |-  ( A  e.  On  ->  Ord  A )
2 ordelss 4846 . . 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 1758    C_ wss 3439   Ord word 4829   Oncon0 4830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-rex 2805  df-v 3080  df-in 3446  df-ss 3453  df-uni 4203  df-tr 4497  df-po 4752  df-so 4753  df-fr 4790  df-we 4792  df-ord 4833  df-on 4834
This theorem is referenced by:  ordunidif  4878  onelssi  4938  ssorduni  6510  suceloni  6537  tfisi  6582  tfrlem9  6957  tfrlem11  6960  oaordex  7110  oaass  7113  odi  7131  omass  7132  oewordri  7144  nnaordex  7190  domtriord  7570  hartogs  7873  card2on  7884  tskwe  8235  infxpenlem  8295  cfub  8533  cfsuc  8541  coflim  8545  hsmexlem2  8711  ondomon  8842  pwcfsdom  8862  inar1  9057  tskord  9062  grudomon  9099  gruina  9100  dfrdg2  27776  poseq  27881  sltres  27972  nobndup  28008  nobnddown  28009  aomclem6  29583
  Copyright terms: Public domain W3C validator