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