Metamath Proof Explorer


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 On C On A C b C A b

Proof

Step Hyp Ref Expression
1 ssid A A
2 sseq2 b = A A b A A
3 2 rspcev A C A A b C A b
4 1 3 mpan2 A C b C A b
5 ontr2 A On C On A b b C A C
6 5 expcomd A On C On b C A b A C
7 6 rexlimdv A On C On b C A b A C
8 4 7 impbid2 A On C On A C b C A b