Metamath Proof Explorer

Theorem ordequn

Description: The maximum (i.e. union) of two ordinals is either one or the other. Similar to Exercise 14 of TakeutiZaring p. 40. (Contributed by NM, 28-Nov-2003)

Ref Expression
Assertion ordequn 
|- ( ( Ord B /\ Ord C ) -> ( A = ( B u. C ) -> ( A = B \/ A = C ) ) )

Proof

Step Hyp Ref Expression
1 ordtri2or2 
 |-  ( ( Ord B /\ Ord C ) -> ( B C_ C \/ C C_ B ) )
2 1 orcomd 
 |-  ( ( Ord B /\ Ord C ) -> ( C C_ B \/ B C_ C ) )
3 ssequn2 
 |-  ( C C_ B <-> ( B u. C ) = B )
4 eqeq1 
 |-  ( A = ( B u. C ) -> ( A = B <-> ( B u. C ) = B ) )
5 3 4 bitr4id 
 |-  ( A = ( B u. C ) -> ( C C_ B <-> A = B ) )
6 ssequn1 
 |-  ( B C_ C <-> ( B u. C ) = C )
7 eqeq1 
 |-  ( A = ( B u. C ) -> ( A = C <-> ( B u. C ) = C ) )
8 6 7 bitr4id 
 |-  ( A = ( B u. C ) -> ( B C_ C <-> A = C ) )
9 5 8 orbi12d 
 |-  ( A = ( B u. C ) -> ( ( C C_ B \/ B C_ C ) <-> ( A = B \/ A = C ) ) )
10 2 9 syl5ibcom 
 |-  ( ( Ord B /\ Ord C ) -> ( A = ( B u. C ) -> ( A = B \/ A = C ) ) )