Metamath Proof Explorer

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 ⁡ A ∧ Ord ⁡ B → A ⊆ suc ⁡ B → A ⊆ B ∨ A = suc ⁡ B

Proof

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