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

Theorem onsssuc 4890
Description: A subset of an ordinal number belongs to its successor. (Contributed by NM, 15-Sep-1995.)
Assertion
Ref Expression
onsssuc  |-  ( ( A  e.  On  /\  B  e.  On )  ->  ( A  C_  B  <->  A  e.  suc  B ) )

Proof of Theorem onsssuc
StepHypRef Expression
1 eloni 4813 . 2  |-  ( B  e.  On  ->  Ord  B )
2 ordsssuc 4889 . 2  |-  ( ( A  e.  On  /\  Ord  B )  ->  ( A  C_  B  <->  A  e.  suc  B ) )
31, 2sylan2 474 1  |-  ( ( A  e.  On  /\  B  e.  On )  ->  ( A  C_  B  <->  A  e.  suc  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1757    C_ wss 3412   Ord word 4802   Oncon0 4803   suc csuc 4805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4497  ax-nul 4505  ax-pr 4615
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3056  df-sbc 3271  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-pss 3428  df-nul 3722  df-if 3876  df-sn 3962  df-pr 3964  df-op 3968  df-uni 4176  df-br 4377  df-opab 4435  df-tr 4470  df-eprel 4716  df-po 4725  df-so 4726  df-fr 4763  df-we 4765  df-ord 4806  df-on 4807  df-suc 4809
This theorem is referenced by:  ordsssuc2  4891  onmindif  4892  tfindsg  6557  dfom2  6564  findsg  6589  ondif2  7028  oeeui  7127  cantnflem1  7984  cantnflem1OLD  8007  rankr1bg  8097  rankr1c  8115  cofsmo  8525  cfsmolem  8526  cfcof  8530  fin1a2lem9  8664  alephreg  8833  winainflem  8947  nobndlem8  27960  onsuct0  28407  onint1  28415
  Copyright terms: Public domain W3C validator