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	$⊢ (A \in On \land Ord B) \to (A \subseteq suc B \leftrightarrow (A \subseteq B \lor A = suc B))$

Proof

Step	Hyp	Ref	Expression
1		sspss	$⊢ A \subseteq suc B \leftrightarrow (A \subset suc B \lor A = suc B)$
2		ordsssuc	$⊢ (A \in On \land Ord B) \to (A \subseteq B \leftrightarrow A \in suc B)$
3		eloni	$⊢ A \in On \to Ord A$
4		ordsuci	$⊢ Ord B \to Ord suc B$
5		ordelpss	$⊢ (Ord A \land Ord suc B) \to (A \in suc B \leftrightarrow A \subset suc B)$
6	3 4 5	syl2an	$⊢ (A \in On \land Ord B) \to (A \in suc B \leftrightarrow A \subset suc B)$
7	2 6	bitrd	$⊢ (A \in On \land Ord B) \to (A \subseteq B \leftrightarrow A \subset suc B)$
8	7	orbi1d	$⊢ (A \in On \land Ord B) \to ((A \subseteq B \lor A = suc B) \leftrightarrow (A \subset suc B \lor A = suc B))$
9	1 8	bitr4id	$⊢ (A \in On \land Ord B) \to (A \subseteq suc B \leftrightarrow (A \subseteq B \lor A = suc B))$

Metamath Proof Explorer

Theorem ordsssucb

Proof