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

Theorem ordelss 5446
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 5444 . 2  |-  ( Ord 
A  ->  Tr  A
)
2 trss 4499 . . 3  |-  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) )
32imp 436 . 2  |-  ( ( Tr  A  /\  B  e.  A )  ->  B  C_  A )
41, 3sylan 479 1  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    e. wcel 1904    C_ wss 3390   Tr wtr 4490   Ord word 5429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ral 2761  df-v 3033  df-in 3397  df-ss 3404  df-uni 4191  df-tr 4491  df-ord 5433
This theorem is referenced by:  onfr  5469  onelss  5472  ordtri2or2  5526  onfununi  7078  smores3  7090  tfrlem1  7112  tfrlem9a  7122  tz7.44-2  7143  tz7.44-3  7144  oaabslem  7362  oaabs2  7364  omabslem  7365  omabs  7366  findcard3  7832  nnsdomg  7848  ordiso2  8048  ordtypelem2  8052  ordtypelem6  8056  ordtypelem7  8057  cantnf  8216  cnfcomlem  8222  cardmin2  8450  infxpenlem  8462  iunfictbso  8563  dfac12lem2  8592  dfac12lem3  8593  unctb  8653  ackbij2lem1  8667  ackbij1lem3  8670  ackbij1lem18  8685  ackbij2  8691  ttukeylem6  8962  ttukeylem7  8963  alephexp1  9022  fpwwe2lem8  9080  pwfseqlem3  9103  pwcdandom  9110  fz1isolem  12665  onsuct0  31172  finxpreclem4  31856
  Copyright terms: Public domain W3C validator