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

Theorem ordelss 4735
Description: An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.)
Assertion
Ref Expression
ordelss  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  C_  A )

Proof of Theorem ordelss
StepHypRef Expression
1 ordtr 4733 . 2  |-  ( Ord 
A  ->  Tr  A
)
2 trss 4394 . . 3  |-  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) )
32imp 429 . 2  |-  ( ( Tr  A  /\  B  e.  A )  ->  B  C_  A )
41, 3sylan 471 1  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756    C_ wss 3328   Tr wtr 4385   Ord word 4718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2720  df-v 2974  df-in 3335  df-ss 3342  df-uni 4092  df-tr 4386  df-ord 4722
This theorem is referenced by:  onfr  4758  onelss  4761  ordtri2or2  4815  onfununi  6802  smores3  6814  tfrlem1  6835  tfrlem9a  6845  tz7.44-2  6863  tz7.44-3  6864  oaabslem  7082  oaabs2  7084  omabslem  7085  omabs  7086  findcard3  7555  nnsdomg  7571  ordiso2  7729  ordtypelem2  7733  ordtypelem6  7737  ordtypelem7  7738  cantnf  7901  cantnfOLD  7923  cnfcomlem  7932  cnfcomlemOLD  7940  cardmin2  8168  infxpenlem  8180  iunfictbso  8284  dfac12lem2  8313  dfac12lem3  8314  unctb  8374  ackbij2lem1  8388  ackbij1lem3  8391  ackbij1lem18  8406  ackbij2  8412  ttukeylem6  8683  ttukeylem7  8684  alephexp1  8743  fpwwe2lem8  8804  pwfseqlem3  8827  pwcdandom  8834  fz1isolem  12214  onsuct0  28287
  Copyright terms: Public domain W3C validator