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

Theorem ordelss 4894
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 4892 . 2  |-  ( Ord 
A  ->  Tr  A
)
2 trss 4549 . . 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 1767    C_ wss 3476   Tr wtr 4540   Ord word 4877
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-v 3115  df-in 3483  df-ss 3490  df-uni 4246  df-tr 4541  df-ord 4881
This theorem is referenced by:  onfr  4917  onelss  4920  ordtri2or2  4974  onfununi  7012  smores3  7024  tfrlem1  7045  tfrlem9a  7055  tz7.44-2  7073  tz7.44-3  7074  oaabslem  7292  oaabs2  7294  omabslem  7295  omabs  7296  findcard3  7762  nnsdomg  7778  ordiso2  7939  ordtypelem2  7943  ordtypelem6  7947  ordtypelem7  7948  cantnf  8111  cantnfOLD  8133  cnfcomlem  8142  cnfcomlemOLD  8150  cardmin2  8378  infxpenlem  8390  iunfictbso  8494  dfac12lem2  8523  dfac12lem3  8524  unctb  8584  ackbij2lem1  8598  ackbij1lem3  8601  ackbij1lem18  8616  ackbij2  8622  ttukeylem6  8893  ttukeylem7  8894  alephexp1  8953  fpwwe2lem8  9014  pwfseqlem3  9037  pwcdandom  9044  fz1isolem  12475  onsuct0  29499
  Copyright terms: Public domain W3C validator