This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) )