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

Theorem ordelss 4883
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 4881 . 2  |-  ( Ord 
A  ->  Tr  A
)
2 trss 4541 . . 3  |-  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) )
32imp 427 . 2  |-  ( ( Tr  A  /\  B  e.  A )  ->  B  C_  A )
41, 3sylan 469 1  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1823    C_ wss 3461   Tr wtr 4532   Ord word 4866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-v 3108  df-in 3468  df-ss 3475  df-uni 4236  df-tr 4533  df-ord 4870
This theorem is referenced by:  onfr  4906  onelss  4909  ordtri2or2  4963  onfununi  7004  smores3  7016  tfrlem1  7037  tfrlem9a  7047  tz7.44-2  7065  tz7.44-3  7066  oaabslem  7284  oaabs2  7286  omabslem  7287  omabs  7288  findcard3  7755  nnsdomg  7771  ordiso2  7932  ordtypelem2  7936  ordtypelem6  7940  ordtypelem7  7941  cantnf  8103  cantnfOLD  8125  cnfcomlem  8134  cnfcomlemOLD  8142  cardmin2  8370  infxpenlem  8382  iunfictbso  8486  dfac12lem2  8515  dfac12lem3  8516  unctb  8576  ackbij2lem1  8590  ackbij1lem3  8593  ackbij1lem18  8608  ackbij2  8614  ttukeylem6  8885  ttukeylem7  8886  alephexp1  8945  fpwwe2lem8  9004  pwfseqlem3  9027  pwcdandom  9034  fz1isolem  12494  onsuct0  30134
  Copyright terms: Public domain W3C validator