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

Theorem ordelss 4884
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 4882 . 2  |-  ( Ord 
A  ->  Tr  A
)
2 trss 4539 . . 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 1804    C_ wss 3461   Tr wtr 4530   Ord word 4867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-v 3097  df-in 3468  df-ss 3475  df-uni 4235  df-tr 4531  df-ord 4871
This theorem is referenced by:  onfr  4907  onelss  4910  ordtri2or2  4964  onfununi  7014  smores3  7026  tfrlem1  7047  tfrlem9a  7057  tz7.44-2  7075  tz7.44-3  7076  oaabslem  7294  oaabs2  7296  omabslem  7297  omabs  7298  findcard3  7765  nnsdomg  7781  ordiso2  7943  ordtypelem2  7947  ordtypelem6  7951  ordtypelem7  7952  cantnf  8115  cantnfOLD  8137  cnfcomlem  8146  cnfcomlemOLD  8154  cardmin2  8382  infxpenlem  8394  iunfictbso  8498  dfac12lem2  8527  dfac12lem3  8528  unctb  8588  ackbij2lem1  8602  ackbij1lem3  8605  ackbij1lem18  8620  ackbij2  8626  ttukeylem6  8897  ttukeylem7  8898  alephexp1  8957  fpwwe2lem8  9018  pwfseqlem3  9041  pwcdandom  9048  fz1isolem  12489  onsuct0  29881
  Copyright terms: Public domain W3C validator