ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ordelss Unicode version

Theorem ordelss 4162
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 4161 . 2  |-  ( Ord 
A  ->  Tr  A
)
2 trss 3904 . . 3  |-  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) )
32imp 122 . 2  |-  ( ( Tr  A  /\  B  e.  A )  ->  B  C_  A )
41, 3sylan 277 1  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    e. wcel 1434    C_ wss 2982   Tr wtr 3895   Ord word 4145
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-v 2612  df-in 2988  df-ss 2995  df-uni 3622  df-tr 3896  df-iord 4149
This theorem is referenced by:  ordelord  4164  onelss  4170  ordsuc  4334  smores3  5962  tfrlem1  5977  tfrlemisucaccv  5994  tfrlemiubacc  5999  tfr1onlemsucaccv  6010  tfr1onlemubacc  6015  tfrcllemsucaccv  6023  tfrcllemubacc  6028  nntri1  6160  nnsseleq  6165  fict  6424  infnfi  6451  isinfinf  6453  ordiso2  6540  hashinfuni  9853
  Copyright terms: Public domain W3C validator