Theorem ordsssucim 43980

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 43913 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

Step	Hyp	Ref	Expression
1		ordsuc 7795	. . 3 ⊢ (Ord 𝐵 ↔ Ord suc 𝐵)
2		ordsseleq 6376	. . 3 ⊢ ((Ord 𝐴 ∧ Ord suc 𝐵) → (𝐴 ⊆ suc 𝐵 ↔ (𝐴 ∈ suc 𝐵 ∨ 𝐴 = suc 𝐵)))
3	1, 2	sylan2b 603	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 ↔ (𝐴 ∈ suc 𝐵 ∨ 𝐴 = suc 𝐵)))
4		simpr 488	. . . 4 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → Ord 𝐵)
5		ordtr 6361	. . . 4 ⊢ (Ord 𝐵 → Tr 𝐵)
6		trsucss 6437	. . . 4 ⊢ (Tr 𝐵 → (𝐴 ∈ suc 𝐵 → 𝐴 ⊆ 𝐵))
7	4, 5, 6	3syl 18	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ suc 𝐵 → 𝐴 ⊆ 𝐵))
8	7	orim1d 979	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ suc 𝐵 ∨ 𝐴 = suc 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵)))
9	3, 8	sylbid 242	1 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ suc 𝐵 → (𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   = wceq 1561   ∈ wcel 2143   ⊆ wss 3905  Tr wtr 5208  Ord word 6346  suc csuc 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5247  ax-pr 5391

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-tr 5209  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-ord 6350  df-on 6351  df-suc 6353

This theorem is referenced by: (None)