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

Theorem ordsucss 6441
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 4753 . . . . 5  |-  ( ( Ord  B  /\  A  e.  B )  ->  Ord  A )
2 ordnbtwn 4821 . . . . . . . 8  |-  ( Ord 
A  ->  -.  ( A  e.  B  /\  B  e.  suc  A ) )
3 imnan 422 . . . . . . . 8  |-  ( ( A  e.  B  ->  -.  B  e.  suc  A )  <->  -.  ( A  e.  B  /\  B  e. 
suc  A ) )
42, 3sylibr 212 . . . . . . 7  |-  ( Ord 
A  ->  ( A  e.  B  ->  -.  B  e.  suc  A ) )
54adantr 465 . . . . . 6  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  e.  B  ->  -.  B  e.  suc  A ) )
6 ordsuc 6437 . . . . . . 7  |-  ( Ord 
A  <->  Ord  suc  A )
7 ordtri1 4764 . . . . . . 7  |-  ( ( Ord  suc  A  /\  Ord  B )  ->  ( suc  A  C_  B  <->  -.  B  e.  suc  A ) )
86, 7sylanb 472 . . . . . 6  |-  ( ( Ord  A  /\  Ord  B )  ->  ( suc  A 
C_  B  <->  -.  B  e.  suc  A ) )
95, 8sylibrd 234 . . . . 5  |-  ( ( Ord  A  /\  Ord  B )  ->  ( A  e.  B  ->  suc  A  C_  B ) )
101, 9sylan 471 . . . 4  |-  ( ( ( Ord  B  /\  A  e.  B )  /\  Ord  B )  -> 
( A  e.  B  ->  suc  A  C_  B
) )
1110exp31 604 . . 3  |-  ( Ord 
B  ->  ( A  e.  B  ->  ( Ord 
B  ->  ( A  e.  B  ->  suc  A  C_  B ) ) ) )
1211pm2.43b 50 . 2  |-  ( A  e.  B  ->  ( Ord  B  ->  ( A  e.  B  ->  suc  A  C_  B ) ) )
1312pm2.43b 50 1  |-  ( Ord 
B  ->  ( A  e.  B  ->  suc  A  C_  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1756    C_ wss 3340   Ord word 4730   suc csuc 4733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pr 4543  ax-un 6384
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-sbc 3199  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-pss 3356  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-tp 3894  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-tr 4398  df-eprel 4644  df-po 4653  df-so 4654  df-fr 4691  df-we 4693  df-ord 4734  df-on 4735  df-suc 4737
This theorem is referenced by:  ordelsuc  6443  ordsucelsuc  6445  orduniorsuc  6453  tfindsg2  6484  oaordi  6997  oawordeulem  7005  omeulem2  7034  oeworde  7044  oelimcl  7051  oeeui  7053  nnaordi  7069  nnawordex  7088  oaabs2  7096  omxpenlem  7424  inf3lem5  7850  cantnflt  7892  cantnflem1d  7908  cantnfltOLD  7922  cantnflem1dOLD  7931  cnfcom  7945  cnfcomOLD  7953  r1ordg  7997  rankr1ag  8021  cfslb2n  8449  cfsmolem  8451  fin23lem26  8506  isf32lem3  8536  ttukeylem7  8696  indpi  9088
  Copyright terms: Public domain W3C validator