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

Theorem orduniorsuc 6436
Description: An ordinal class is either its union or the successor of its union. If we adopt the view that zero is a limit ordinal, this means every ordinal class is either a limit or a successor. (Contributed by NM, 13-Sep-2003.)
Assertion
Ref Expression
orduniorsuc  |-  ( Ord 
A  ->  ( A  =  U. A  \/  A  =  suc  U. A ) )

Proof of Theorem orduniorsuc
StepHypRef Expression
1 orduniss 4808 . . . . . 6  |-  ( Ord 
A  ->  U. A  C_  A )
2 orduni 6400 . . . . . . . 8  |-  ( Ord 
A  ->  Ord  U. A
)
3 ordelssne 4741 . . . . . . . 8  |-  ( ( Ord  U. A  /\  Ord  A )  ->  ( U. A  e.  A  <->  ( U. A  C_  A  /\  U. A  =/=  A
) ) )
42, 3mpancom 669 . . . . . . 7  |-  ( Ord 
A  ->  ( U. A  e.  A  <->  ( U. A  C_  A  /\  U. A  =/=  A ) ) )
54biimprd 223 . . . . . 6  |-  ( Ord 
A  ->  ( ( U. A  C_  A  /\  U. A  =/=  A )  ->  U. A  e.  A
) )
61, 5mpand 675 . . . . 5  |-  ( Ord 
A  ->  ( U. A  =/=  A  ->  U. A  e.  A ) )
7 ordsucss 6424 . . . . 5  |-  ( Ord 
A  ->  ( U. A  e.  A  ->  suc  U. A  C_  A ) )
86, 7syld 44 . . . 4  |-  ( Ord 
A  ->  ( U. A  =/=  A  ->  suc  U. A  C_  A )
)
9 ordsucuni 6435 . . . 4  |-  ( Ord 
A  ->  A  C_  suc  U. A )
108, 9jctild 543 . . 3  |-  ( Ord 
A  ->  ( U. A  =/=  A  ->  ( A  C_  suc  U. A  /\  suc  U. A  C_  A ) ) )
11 df-ne 2603 . . . 4  |-  ( A  =/=  U. A  <->  -.  A  =  U. A )
12 necom 2688 . . . 4  |-  ( A  =/=  U. A  <->  U. A  =/= 
A )
1311, 12bitr3i 251 . . 3  |-  ( -.  A  =  U. A  <->  U. A  =/=  A )
14 eqss 3366 . . 3  |-  ( A  =  suc  U. A  <->  ( A  C_  suc  U. A  /\  suc  U. A  C_  A ) )
1510, 13, 143imtr4g 270 . 2  |-  ( Ord 
A  ->  ( -.  A  =  U. A  ->  A  =  suc  U. A
) )
1615orrd 378 1  |-  ( Ord 
A  ->  ( A  =  U. A  \/  A  =  suc  U. A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1369    e. wcel 1756    =/= wne 2601    C_ wss 3323   U.cuni 4086   Ord word 4713   suc csuc 4716
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 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526  ax-un 6367
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 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-tr 4381  df-eprel 4627  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-suc 4720
This theorem is referenced by:  onuniorsuci  6445  oeeulem  7032  cantnfp1lem2  7879  cantnflem1  7889  cantnfp1lem2OLD  7905  cantnflem1OLD  7912  cnfcom2lem  7926  cnfcom2lemOLD  7934  dfac12lem1  8304  dfac12lem2  8305  ttukeylem3  8672  ttukeylem5  8674  ttukeylem6  8675  ordtoplem  28251  ordcmp  28263  aomclem5  29382
  Copyright terms: Public domain W3C validator