Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ordsssucim Structured version   Visualization version   GIF version

Theorem ordsssucim 42734
Description: If an ordinal is less than or equal to the successor of another, then the first is either less than or equal to the second or the first is equal to the successor of the second. Theorem 1 in Grzegorz Bancerek, "Epsilon Numbers and Cantor Normal Form", Formalized Mathematics, Vol. 17, No. 4, Pages 249–256, 2009. DOI: 10.2478/v10037-009-0032-8 See also ordsssucb 42666 for a biimplication when 𝐴 is a set. (Contributed by RP, 3-Jan-2025.)
Assertion
Ref Expression
ordsssucim ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 → (𝐴𝐵𝐴 = suc 𝐵)))

Proof of Theorem ordsssucim
StepHypRef Expression
1 ordsuc 7798 . . 3 (Ord 𝐵 ↔ Ord suc 𝐵)
2 ordsseleq 6387 . . 3 ((Ord 𝐴 ∧ Ord suc 𝐵) → (𝐴 ⊆ suc 𝐵 ↔ (𝐴 ∈ suc 𝐵𝐴 = suc 𝐵)))
31, 2sylan2b 593 . 2 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 ↔ (𝐴 ∈ suc 𝐵𝐴 = suc 𝐵)))
4 simpr 484 . . . 4 ((Ord 𝐴 ∧ Ord 𝐵) → Ord 𝐵)
5 ordtr 6372 . . . 4 (Ord 𝐵 → Tr 𝐵)
6 trsucss 6446 . . . 4 (Tr 𝐵 → (𝐴 ∈ suc 𝐵𝐴𝐵))
74, 5, 63syl 18 . . 3 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ suc 𝐵𝐴𝐵))
87orim1d 962 . 2 ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ suc 𝐵𝐴 = suc 𝐵) → (𝐴𝐵𝐴 = suc 𝐵)))
93, 8sylbid 239 1 ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 → (𝐴𝐵𝐴 = suc 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wo 844   = wceq 1533  wcel 2098  wss 3943  Tr wtr 5258  Ord word 6357  suc csuc 6360
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-ne 2935  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-tr 5259  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-ord 6361  df-on 6362  df-suc 6364
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator