Metamath Proof Explorer

Theorem infsupprpr

Description: The infimum of a proper pair is less than the supremum of this pair. (Contributed by AV, 13-Mar-2023)

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

Proof

Step Hyp Ref Expression
1 solin 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C \/ B = C \/ C R B ) )
2 1 3adantr3 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> ( B R C \/ B = C \/ C R B ) )
3 iftrue 
 |-  ( B R C -> if ( B R C , B , C ) = B )
4 3 adantr 
 |-  ( ( B R C /\ ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) ) -> if ( B R C , B , C ) = B )
5 sotric 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C <-> -. ( B = C \/ C R B ) ) )
6 5 3adantr3 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> ( B R C <-> -. ( B = C \/ C R B ) ) )
7 6 biimpac 
 |-  ( ( B R C /\ ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) ) -> -. ( B = C \/ C R B ) )
8 ioran 
 |-  ( -. ( B = C \/ C R B ) <-> ( -. B = C /\ -. C R B ) )
9 simprl 
 |-  ( ( -. C R B /\ ( B R C /\ ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) ) ) -> B R C )
10 iffalse 
 |-  ( -. C R B -> if ( C R B , B , C ) = C )
11 10 adantr 
 |-  ( ( -. C R B /\ ( B R C /\ ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) ) ) -> if ( C R B , B , C ) = C )
12 9 11 breqtrrd 
 |-  ( ( -. C R B /\ ( B R C /\ ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) ) ) -> B R if ( C R B , B , C ) )
13 12 ex 
 |-  ( -. C R B -> ( ( B R C /\ ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) ) -> B R if ( C R B , B , C ) ) )
14 8 13 simplbiim 
 |-  ( -. ( B = C \/ C R B ) -> ( ( B R C /\ ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) ) -> B R if ( C R B , B , C ) ) )
15 7 14 mpcom 
 |-  ( ( B R C /\ ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) ) -> B R if ( C R B , B , C ) )
16 4 15 eqbrtrd 
 |-  ( ( B R C /\ ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) ) -> if ( B R C , B , C ) R if ( C R B , B , C ) )
17 16 ex 
 |-  ( B R C -> ( ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> if ( B R C , B , C ) R if ( C R B , B , C ) ) )
18 eqneqall 
 |-  ( B = C -> ( B =/= C -> if ( B R C , B , C ) R if ( C R B , B , C ) ) )
19 18 2a1d 
 |-  ( B = C -> ( B e. A -> ( C e. A -> ( B =/= C -> if ( B R C , B , C ) R if ( C R B , B , C ) ) ) ) )
20 19 3impd 
 |-  ( B = C -> ( ( B e. A /\ C e. A /\ B =/= C ) -> if ( B R C , B , C ) R if ( C R B , B , C ) ) )
21 20 adantld 
 |-  ( B = C -> ( ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> if ( B R C , B , C ) R if ( C R B , B , C ) ) )
22 pm3.22 
 |-  ( ( B e. A /\ C e. A ) -> ( C e. A /\ B e. A ) )
23 22 3adant3 
 |-  ( ( B e. A /\ C e. A /\ B =/= C ) -> ( C e. A /\ B e. A ) )
24 sotric 
 |-  ( ( R Or A /\ ( C e. A /\ B e. A ) ) -> ( C R B <-> -. ( C = B \/ B R C ) ) )
25 24 biimpd 
 |-  ( ( R Or A /\ ( C e. A /\ B e. A ) ) -> ( C R B -> -. ( C = B \/ B R C ) ) )
26 23 25 sylan2 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> ( C R B -> -. ( C = B \/ B R C ) ) )
27 26 impcom 
 |-  ( ( C R B /\ ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) ) -> -. ( C = B \/ B R C ) )
28 ioran 
 |-  ( -. ( C = B \/ B R C ) <-> ( -. C = B /\ -. B R C ) )
29 simpr 
 |-  ( ( -. B R C /\ C R B ) -> C R B )
30 iffalse 
 |-  ( -. B R C -> if ( B R C , B , C ) = C )
31 iftrue 
 |-  ( C R B -> if ( C R B , B , C ) = B )
32 30 31 breqan12d 
 |-  ( ( -. B R C /\ C R B ) -> ( if ( B R C , B , C ) R if ( C R B , B , C ) <-> C R B ) )
33 29 32 mpbird 
 |-  ( ( -. B R C /\ C R B ) -> if ( B R C , B , C ) R if ( C R B , B , C ) )
34 33 a1d 
 |-  ( ( -. B R C /\ C R B ) -> ( ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> if ( B R C , B , C ) R if ( C R B , B , C ) ) )
35 34 expimpd 
 |-  ( -. B R C -> ( ( C R B /\ ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) ) -> if ( B R C , B , C ) R if ( C R B , B , C ) ) )
36 28 35 simplbiim 
 |-  ( -. ( C = B \/ B R C ) -> ( ( C R B /\ ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) ) -> if ( B R C , B , C ) R if ( C R B , B , C ) ) )
37 27 36 mpcom 
 |-  ( ( C R B /\ ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) ) -> if ( B R C , B , C ) R if ( C R B , B , C ) )
38 37 ex 
 |-  ( C R B -> ( ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> if ( B R C , B , C ) R if ( C R B , B , C ) ) )
39 17 21 38 3jaoi 
 |-  ( ( B R C \/ B = C \/ C R B ) -> ( ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> if ( B R C , B , C ) R if ( C R B , B , C ) ) )
40 2 39 mpcom 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> if ( B R C , B , C ) R if ( C R B , B , C ) )
41 infpr 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> inf ( { B , C } , A , R ) = if ( B R C , B , C ) )
42 suppr 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> sup ( { B , C } , A , R ) = if ( C R B , B , C ) )
43 41 42 breq12d 
 |-  ( ( R Or A /\ B e. A /\ C e. A ) -> ( inf ( { B , C } , A , R ) R sup ( { B , C } , A , R ) <-> if ( B R C , B , C ) R if ( C R B , B , C ) ) )
44 43 3adant3r3 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> ( inf ( { B , C } , A , R ) R sup ( { B , C } , A , R ) <-> if ( B R C , B , C ) R if ( C R B , B , C ) ) )
45 40 44 mpbird 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> inf ( { B , C } , A , R ) R sup ( { B , C } , A , R ) )