Metamath Proof Explorer

Theorem ordtri2or3

Description: A consequence of total ordering for ordinal classes. Similar to ordtri2or2 . (Contributed by David Moews, 1-May-2017)

Ref Expression
Assertion ordtri2or3 
|- ( ( Ord A /\ Ord B ) -> ( A = ( A i^i B ) \/ B = ( A i^i B ) ) )

Proof

Step Hyp Ref Expression
1 ordtri2or2 
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B \/ B C_ A ) )
2 dfss 
 |-  ( A C_ B <-> A = ( A i^i B ) )
3 sseqin2 
 |-  ( B C_ A <-> ( A i^i B ) = B )
4 eqcom 
 |-  ( ( A i^i B ) = B <-> B = ( A i^i B ) )
5 3 4 bitri 
 |-  ( B C_ A <-> B = ( A i^i B ) )
6 2 5 orbi12i 
 |-  ( ( A C_ B \/ B C_ A ) <-> ( A = ( A i^i B ) \/ B = ( A i^i B ) ) )
7 1 6 sylib 
 |-  ( ( Ord A /\ Ord B ) -> ( A = ( A i^i B ) \/ B = ( A i^i B ) ) )