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

Theorem ordsucss 6656
Description: The successor of an element of an ordinal class is a subset of it. (Contributed by NM, 21-Jun-1998.)
Assertion
Ref Expression
ordsucss  |-  ( Ord 
B  ->  ( A  e.  B  ->  suc  A  C_  B ) )

Proof of Theorem ordsucss
StepHypRef Expression
1 ordelord 5461 . . . . 5  |-  ( ( Ord  B  /\  A  e.  B )  ->  Ord  A )
2 ordnbtwn 5529 . . . . . . . 8  |-  ( Ord 
A  ->  -.  ( A  e.  B  /\  B  e.  suc  A ) )
3 imnan 423 . . . . . . . 8  |-  ( ( A  e.  B  ->  -.  B  e.  suc  A )  <->  -.  ( A  e.  B  /\  B  e. 
suc  A ) )
42, 3sylibr 215 . . . . . . 7  |-  ( Ord 
A  ->  ( A  e.  B  ->  -.  B  e.  suc  A ) )
54adantr 466 . . . . . 6  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  e.  B  ->  -.  B  e.  suc  A ) )
6 ordsuc 6652 . . . . . . 7  |-  ( Ord 
A  <->  Ord  suc  A )
7 ordtri1 5472 . . . . . . 7  |-  ( ( Ord  suc  A  /\  Ord  B )  ->  ( suc  A  C_  B  <->  -.  B  e.  suc  A ) )
86, 7sylanb 474 . . . . . 6  |-  ( ( Ord  A  /\  Ord  B )  ->  ( suc  A 
C_  B  <->  -.  B  e.  suc  A ) )
95, 8sylibrd 237 . . . . 5  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  e.  B  ->  suc  A  C_  B ) )
101, 9sylan 473 . . . 4  |-  ( ( ( Ord  B  /\  A  e.  B )  /\  Ord  B )  -> 
( A  e.  B  ->  suc  A  C_  B
) )
1110exp31 607 . . 3  |-  ( Ord 
B  ->  ( A  e.  B  ->  ( Ord 
B  ->  ( A  e.  B  ->  suc  A  C_  B ) ) ) )
1211pm2.43b 52 . 2  |-  ( A  e.  B  ->  ( Ord  B  ->  ( A  e.  B  ->  suc  A  C_  B ) ) )
1312pm2.43b 52 1  |-  ( Ord 
B  ->  ( A  e.  B  ->  suc  A  C_  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    e. wcel 1868    C_ wss 3436   Ord word 5438   suc csuc 5441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657  ax-un 6594
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-tr 4516  df-eprel 4761  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-ord 5442  df-on 5443  df-suc 5445
This theorem is referenced by:  ordelsuc  6658  ordsucelsuc  6660  orduniorsuc  6668  tfindsg2  6699  oaordi  7252  oawordeulem  7260  omeulem2  7289  oeworde  7299  oelimcl  7306  oeeui  7308  nnaordi  7324  nnawordex  7343  oaabs2  7351  omxpenlem  7676  inf3lem5  8140  cantnflt  8179  cantnflem1d  8195  cnfcom  8207  r1ordg  8251  rankr1ag  8275  cfslb2n  8699  cfsmolem  8701  fin23lem26  8756  isf32lem3  8786  ttukeylem7  8946  indpi  9333
  Copyright terms: Public domain W3C validator