Theorem ordsssucb

Description: An ordinal number is less than or equal to the successor of an ordinal class iff the ordinal number is either less than or equal to the ordinal class or the ordinal number is equal to the successor of the ordinal class. See also ordsssucim , limsssuc . (Contributed by RP, 22-Feb-2025)

	Ref	Expression
Assertion	ordsssucb	⊢ ( ( 𝐴 ∈ On ∧ Ord 𝐵 ) → ( 𝐴 ⊆ suc 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sspss	⊢ ( 𝐴 ⊆ suc 𝐵 ↔ ( 𝐴 ⊊ suc 𝐵 ∨ 𝐴 = suc 𝐵 ) )
2		ordsssuc	⊢ ( ( 𝐴 ∈ On ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵 ) )
3		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
4		ordsuci	⊢ ( Ord 𝐵 → Ord suc 𝐵 )
5		ordelpss	⊢ ( ( Ord 𝐴 ∧ Ord suc 𝐵 ) → ( 𝐴 ∈ suc 𝐵 ↔ 𝐴 ⊊ suc 𝐵 ) )
6	3 4 5	syl2an	⊢ ( ( 𝐴 ∈ On ∧ Ord 𝐵 ) → ( 𝐴 ∈ suc 𝐵 ↔ 𝐴 ⊊ suc 𝐵 ) )
7	2 6	bitrd	⊢ ( ( 𝐴 ∈ On ∧ Ord 𝐵 ) → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ⊊ suc 𝐵 ) )
8	7	orbi1d	⊢ ( ( 𝐴 ∈ On ∧ Ord 𝐵 ) → ( ( 𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵 ) ↔ ( 𝐴 ⊊ suc 𝐵 ∨ 𝐴 = suc 𝐵 ) ) )
9	1 8	bitr4id	⊢ ( ( 𝐴 ∈ On ∧ Ord 𝐵 ) → ( 𝐴 ⊆ suc 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∨ 𝐴 = suc 𝐵 ) ) )