Theorem 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 e. On /\ C e. On ) -> ( A e. C <-> E. b e. C A C_ b ) )

Proof

Step	Hyp	Ref	Expression
1		ssid	|- A C_ A
2		sseq2	|- ( b = A -> ( A C_ b <-> A C_ A ) )
3	2	rspcev	|- ( ( A e. C /\ A C_ A ) -> E. b e. C A C_ b )
4	1 3	mpan2	|- ( A e. C -> E. b e. C A C_ b )
5		ontr2	|- ( ( A e. On /\ C e. On ) -> ( ( A C_ b /\ b e. C ) -> A e. C ) )
6	5	expcomd	|- ( ( A e. On /\ C e. On ) -> ( b e. C -> ( A C_ b -> A e. C ) ) )
7	6	rexlimdv	|- ( ( A e. On /\ C e. On ) -> ( E. b e. C A C_ b -> A e. C ) )
8	4 7	impbid2	|- ( ( A e. On /\ C e. On ) -> ( A e. C <-> E. b e. C A C_ b ) )