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

Theorem orduniorsuc 7537
 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 𝐴 → (𝐴 = 𝐴𝐴 = suc 𝐴))

Proof of Theorem orduniorsuc
StepHypRef Expression
1 orduniss 6278 . . . . . 6 (Ord 𝐴 𝐴𝐴)
2 orduni 7501 . . . . . . . 8 (Ord 𝐴 → Ord 𝐴)
3 ordelssne 6211 . . . . . . . 8 ((Ord 𝐴 ∧ Ord 𝐴) → ( 𝐴𝐴 ↔ ( 𝐴𝐴 𝐴𝐴)))
42, 3mpancom 686 . . . . . . 7 (Ord 𝐴 → ( 𝐴𝐴 ↔ ( 𝐴𝐴 𝐴𝐴)))
54biimprd 250 . . . . . 6 (Ord 𝐴 → (( 𝐴𝐴 𝐴𝐴) → 𝐴𝐴))
61, 5mpand 693 . . . . 5 (Ord 𝐴 → ( 𝐴𝐴 𝐴𝐴))
7 ordsucss 7525 . . . . 5 (Ord 𝐴 → ( 𝐴𝐴 → suc 𝐴𝐴))
86, 7syld 47 . . . 4 (Ord 𝐴 → ( 𝐴𝐴 → suc 𝐴𝐴))
9 ordsucuni 7536 . . . 4 (Ord 𝐴𝐴 ⊆ suc 𝐴)
108, 9jctild 528 . . 3 (Ord 𝐴 → ( 𝐴𝐴 → (𝐴 ⊆ suc 𝐴 ∧ suc 𝐴𝐴)))
11 df-ne 3015 . . . 4 (𝐴 𝐴 ↔ ¬ 𝐴 = 𝐴)
12 necom 3067 . . . 4 (𝐴 𝐴 𝐴𝐴)
1311, 12bitr3i 279 . . 3 𝐴 = 𝐴 𝐴𝐴)
14 eqss 3980 . . 3 (𝐴 = suc 𝐴 ↔ (𝐴 ⊆ suc 𝐴 ∧ suc 𝐴𝐴))
1510, 13, 143imtr4g 298 . 2 (Ord 𝐴 → (¬ 𝐴 = 𝐴𝐴 = suc 𝐴))
1615orrd 859 1 (Ord 𝐴 → (𝐴 = 𝐴𝐴 = suc 𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1531   ∈ wcel 2108   ≠ wne 3014   ⊆ wss 3934  ∪ cuni 4830  Ord word 6183  suc csuc 6186 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7453 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-tr 5164  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-ord 6187  df-on 6188  df-suc 6190 This theorem is referenced by:  onuniorsuci  7546  oeeulem  8219  cantnfp1lem2  9134  cantnflem1  9144  cnfcom2lem  9156  dfac12lem1  9561  dfac12lem2  9562  ttukeylem3  9925  ttukeylem5  9927  ttukeylem6  9928  ordtoplem  33776  ordcmp  33788  onsucuni3  34640  aomclem5  39648  onsetreclem3  44799
 Copyright terms: Public domain W3C validator