Metamath Proof Explorer

Theorem onsucwordi

Description: The successor operation preserves the less-than-or-equal relationship between ordinals. Lemma 3.1 of Schloeder p. 7. (Contributed by RP, 29-Jan-2025)

		Ref	Expression
	Assertion	onsucwordi	$⊢ (A \in On \land B \in On) \to (A \subseteq B \to suc A \subseteq suc B)$

Proof

Step	Hyp	Ref	Expression
1		eloni	$⊢ A \in On \to Ord A$
2		eloni	$⊢ B \in On \to Ord B$
3		ordsucsssuc	$⊢ (Ord A \land Ord B) \to (A \subseteq B \leftrightarrow suc A \subseteq suc B)$
4	1 2 3	syl2an	$⊢ (A \in On \land B \in On) \to (A \subseteq B \leftrightarrow suc A \subseteq suc B)$
5	4	biimpd	$⊢ (A \in On \land B \in On) \to (A \subseteq B \to suc A \subseteq suc B)$