onelssex

Description: Ordinal less than is equivalent to having an ordinal between them. (Contributed by Scott Fenton, 8-Aug-2024)

		Ref	Expression
	Assertion	onelssex	$⊢ (A \in On \land C \in On) \to (A \in C \leftrightarrow \exists b \in C A \subseteq b)$

Step	Hyp	Ref	Expression
1		ssid	$⊢ A \subseteq A$
2		sseq2	$⊢ b = A \to (A \subseteq b \leftrightarrow A \subseteq A)$
3	2	rspcev	$⊢ (A \in C \land A \subseteq A) \to \exists b \in C A \subseteq b$
4	1 3	mpan2	$⊢ A \in C \to \exists b \in C A \subseteq b$
5		ontr2	$⊢ (A \in On \land C \in On) \to ((A \subseteq b \land b \in C) \to A \in C)$
6	5	expcomd	$⊢ (A \in On \land C \in On) \to (b \in C \to (A \subseteq b \to A \in C))$
7	6	rexlimdv	$⊢ (A \in On \land C \in On) \to (\exists b \in C A \subseteq b \to A \in C)$
8	4 7	impbid2	$⊢ (A \in On \land C \in On) \to (A \in C \leftrightarrow \exists b \in C A \subseteq b)$

Metamath Proof Explorer