Metamath Proof Explorer

Theorem ordunmax

Description: The union of two ordinals is equal to their maximum. (Contributed by BTernaryTau, 7-Oct-2026)

Ref Expression
Assertion ordunmax 
|- ( ( Ord A /\ Ord B ) -> ( A u. B ) = if ( A C_ B , B , A ) )

Proof

Step Hyp Ref Expression
1 ordtri2or2 
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B \/ B C_ A ) )
2 1 ord 
 |-  ( ( Ord A /\ Ord B ) -> ( -. A C_ B -> B C_ A ) )
3 ssequn2 
 |-  ( B C_ A <-> ( A u. B ) = A )
4 2 3 imbitrdi 
 |-  ( ( Ord A /\ Ord B ) -> ( -. A C_ B -> ( A u. B ) = A ) )
5 iffalse 
 |-  ( -. A C_ B -> if ( A C_ B , B , A ) = A )
6 4 5 jca2 
 |-  ( ( Ord A /\ Ord B ) -> ( -. A C_ B -> ( ( A u. B ) = A /\ if ( A C_ B , B , A ) = A ) ) )
7 eqtr3 
 |-  ( ( ( A u. B ) = A /\ if ( A C_ B , B , A ) = A ) -> ( A u. B ) = if ( A C_ B , B , A ) )
8 6 7 syl6 
 |-  ( ( Ord A /\ Ord B ) -> ( -. A C_ B -> ( A u. B ) = if ( A C_ B , B , A ) ) )
9 ssequn1 
 |-  ( A C_ B <-> ( A u. B ) = B )
10 9 biimpi 
 |-  ( A C_ B -> ( A u. B ) = B )
11 iftrue 
 |-  ( A C_ B -> if ( A C_ B , B , A ) = B )
12 10 11 eqtr4d 
 |-  ( A C_ B -> ( A u. B ) = if ( A C_ B , B , A ) )
13 8 12 pm2.61d2 
 |-  ( ( Ord A /\ Ord B ) -> ( A u. B ) = if ( A C_ B , B , A ) )