Metamath Proof Explorer

Theorem infpr

Description: The infimum of a pair. (Contributed by AV, 4-Sep-2020)

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