Metamath Proof Explorer

Theorem soltmin

Description: Being less than a minimum, for a general total order. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion soltmin 
|- ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A R if ( B R C , B , C ) <-> ( A R B /\ A R C ) ) )

Proof

Step Hyp Ref Expression
1 sopo 
 |-  ( R Or X -> R Po X )
2 1 ad2antrr 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R if ( B R C , B , C ) ) -> R Po X )
3 simplr1 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R if ( B R C , B , C ) ) -> A e. X )
4 simplr2 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R if ( B R C , B , C ) ) -> B e. X )
5 simplr3 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R if ( B R C , B , C ) ) -> C e. X )
6 4 5 ifcld 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R if ( B R C , B , C ) ) -> if ( B R C , B , C ) e. X )
7 3 6 4 3jca 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R if ( B R C , B , C ) ) -> ( A e. X /\ if ( B R C , B , C ) e. X /\ B e. X ) )
8 simpr 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R if ( B R C , B , C ) ) -> A R if ( B R C , B , C ) )
9 simpll 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R if ( B R C , B , C ) ) -> R Or X )
10 somin1 
 |-  ( ( R Or X /\ ( B e. X /\ C e. X ) ) -> if ( B R C , B , C ) ( R u. _I ) B )
11 9 4 5 10 syl12anc 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R if ( B R C , B , C ) ) -> if ( B R C , B , C ) ( R u. _I ) B )
12 poltletr 
 |-  ( ( R Po X /\ ( A e. X /\ if ( B R C , B , C ) e. X /\ B e. X ) ) -> ( ( A R if ( B R C , B , C ) /\ if ( B R C , B , C ) ( R u. _I ) B ) -> A R B ) )
13 12 imp 
 |-  ( ( ( R Po X /\ ( A e. X /\ if ( B R C , B , C ) e. X /\ B e. X ) ) /\ ( A R if ( B R C , B , C ) /\ if ( B R C , B , C ) ( R u. _I ) B ) ) -> A R B )
14 2 7 8 11 13 syl22anc 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R if ( B R C , B , C ) ) -> A R B )
15 3 6 5 3jca 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R if ( B R C , B , C ) ) -> ( A e. X /\ if ( B R C , B , C ) e. X /\ C e. X ) )
16 somin2 
 |-  ( ( R Or X /\ ( B e. X /\ C e. X ) ) -> if ( B R C , B , C ) ( R u. _I ) C )
17 9 4 5 16 syl12anc 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R if ( B R C , B , C ) ) -> if ( B R C , B , C ) ( R u. _I ) C )
18 poltletr 
 |-  ( ( R Po X /\ ( A e. X /\ if ( B R C , B , C ) e. X /\ C e. X ) ) -> ( ( A R if ( B R C , B , C ) /\ if ( B R C , B , C ) ( R u. _I ) C ) -> A R C ) )
19 18 imp 
 |-  ( ( ( R Po X /\ ( A e. X /\ if ( B R C , B , C ) e. X /\ C e. X ) ) /\ ( A R if ( B R C , B , C ) /\ if ( B R C , B , C ) ( R u. _I ) C ) ) -> A R C )
20 2 15 8 17 19 syl22anc 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R if ( B R C , B , C ) ) -> A R C )
21 14 20 jca 
 |-  ( ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R if ( B R C , B , C ) ) -> ( A R B /\ A R C ) )
22 21 ex 
 |-  ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A R if ( B R C , B , C ) -> ( A R B /\ A R C ) ) )
23 breq2 
 |-  ( B = if ( B R C , B , C ) -> ( A R B <-> A R if ( B R C , B , C ) ) )
24 breq2 
 |-  ( C = if ( B R C , B , C ) -> ( A R C <-> A R if ( B R C , B , C ) ) )
25 23 24 ifboth 
 |-  ( ( A R B /\ A R C ) -> A R if ( B R C , B , C ) )
26 22 25 impbid1 
 |-  ( ( R Or X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A R if ( B R C , B , C ) <-> ( A R B /\ A R C ) ) )