Theorem ordsssucim

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 for a biimplication when A is a set. (Contributed by RP, 3-Jan-2025)

	Ref	Expression
Assertion	ordsssucim	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ suc 𝐵 → ( 𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ordsuc	⊢ ( Ord 𝐵 ↔ Ord suc 𝐵 )
2		ordsseleq	⊢ ( ( Ord 𝐴 ∧ Ord suc 𝐵 ) → ( 𝐴 ⊆ suc 𝐵 ↔ ( 𝐴 ∈ suc 𝐵 ∨ 𝐴 = suc 𝐵 ) ) )
3	1 2	sylan2b	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ suc 𝐵 ↔ ( 𝐴 ∈ suc 𝐵 ∨ 𝐴 = suc 𝐵 ) ) )
4		simpr	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → Ord 𝐵 )
5		ordtr	⊢ ( Ord 𝐵 → Tr 𝐵 )
6		trsucss	⊢ ( Tr 𝐵 → ( 𝐴 ∈ suc 𝐵 → 𝐴 ⊆ 𝐵 ) )
7	4 5 6	3syl	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ∈ suc 𝐵 → 𝐴 ⊆ 𝐵 ) )
8	7	orim1d	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ( 𝐴 ∈ suc 𝐵 ∨ 𝐴 = suc 𝐵 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵 ) ) )
9	3 8	sylbid	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 ⊆ suc 𝐵 → ( 𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵 ) ) )