Metamath Proof Explorer

Theorem suppr

Description: The supremum of a pair. (Contributed by NM, 17-Jun-2007) (Proof shortened by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion suppr 
|- ( ( R Or A /\ B e. A /\ C e. A ) -> sup ( { B , C } , A , R ) = if ( C R B , B , C ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> R Or A )
2 ifcl 
 |-  ( ( B e. A /\ C e. A ) -> if ( C R B , B , C ) e. A )
3 2 3adant1 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> if ( C R B , B , C ) e. A )
4 ifpr 
 |-  ( ( B e. A /\ C e. A ) -> if ( C R B , B , C ) e. { B , C } )
5 4 3adant1 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> if ( C R B , B , C ) e. { B , C } )
6 breq1 
 |-  ( B = if ( C R B , B , C ) -> ( B R B <-> if ( C R B , B , C ) R B ) )
7 6 notbid 
 |-  ( B = if ( C R B , B , C ) -> ( -. B R B <-> -. if ( C R B , B , C ) R B ) )
8 breq1 
 |-  ( C = if ( C R B , B , C ) -> ( C R B <-> if ( C R B , B , C ) R B ) )
9 8 notbid 
 |-  ( C = if ( C R B , B , C ) -> ( -. C R B <-> -. if ( C R B , B , C ) R B ) )
10 sonr 
 |-  ( ( R Or A /\ B e. A ) -> -. B R B )
11 10 3adant3 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> -. B R B )
12 11 adantr 
 |-  ( ( ( R Or A /\ B e. A /\ C e. A ) /\ C R B ) -> -. B R B )
13 simpr 
 |-  ( ( ( R Or A /\ B e. A /\ C e. A ) /\ -. C R B ) -> -. C R B )
14 7 9 12 13 ifbothda 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> -. if ( C R B , B , C ) R B )
15 breq1 
 |-  ( B = if ( C R B , B , C ) -> ( B R C <-> if ( C R B , B , C ) R C ) )
16 15 notbid 
 |-  ( B = if ( C R B , B , C ) -> ( -. B R C <-> -. if ( C R B , B , C ) R C ) )
17 breq1 
 |-  ( C = if ( C R B , B , C ) -> ( C R C <-> if ( C R B , B , C ) R C ) )
18 17 notbid 
 |-  ( C = if ( C R B , B , C ) -> ( -. C R C <-> -. if ( C R B , B , C ) R C ) )
19 so2nr 
 |-  ( ( R Or A /\ ( C e. A /\ B e. A ) ) -> -. ( C R B /\ B R C ) )
20 19 3impb 
 |-  ( ( R Or A /\ C e. A /\ B e. A ) -> -. ( C R B /\ B R C ) )
21 20 3com23 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> -. ( C R B /\ B R C ) )
22 imnan 
 |-  ( ( C R B -> -. B R C ) <-> -. ( C R B /\ B R C ) )
23 21 22 sylibr 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> ( C R B -> -. B R C ) )
24 23 imp 
 |-  ( ( ( R Or A /\ B e. A /\ C e. A ) /\ C R B ) -> -. B R C )
25 sonr 
 |-  ( ( R Or A /\ C e. A ) -> -. C R C )
26 25 3adant2 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> -. C R C )
27 26 adantr 
 |-  ( ( ( R Or A /\ B e. A /\ C e. A ) /\ -. C R B ) -> -. C R C )
28 16 18 24 27 ifbothda 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> -. if ( C R B , B , C ) R C )
29 breq2 
 |-  ( y = B -> ( if ( C R B , B , C ) R y <-> if ( C R B , B , C ) R B ) )
30 29 notbid 
 |-  ( y = B -> ( -. if ( C R B , B , C ) R y <-> -. if ( C R B , B , C ) R B ) )
31 breq2 
 |-  ( y = C -> ( if ( C R B , B , C ) R y <-> if ( C R B , B , C ) R C ) )
32 31 notbid 
 |-  ( y = C -> ( -. if ( C R B , B , C ) R y <-> -. if ( C R B , B , C ) R C ) )
33 30 32 ralprg 
 |-  ( ( B e. A /\ C e. A ) -> ( A. y e. { B , C } -. if ( C R B , B , C ) R y <-> ( -. if ( C R B , B , C ) R B /\ -. if ( C R B , B , C ) R C ) ) )
34 33 3adant1 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> ( A. y e. { B , C } -. if ( C R B , B , C ) R y <-> ( -. if ( C R B , B , C ) R B /\ -. if ( C R B , B , C ) R C ) ) )
35 14 28 34 mpbir2and 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> A. y e. { B , C } -. if ( C R B , B , C ) R y )
36 35 r19.21bi 
 |-  ( ( ( R Or A /\ B e. A /\ C e. A ) /\ y e. { B , C } ) -> -. if ( C R B , B , C ) R y )
37 1 3 5 36 supmax 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> sup ( { B , C } , A , R ) = if ( C R B , B , C ) )