Metamath Proof Explorer

Theorem tsrlemax

Description: Two ways of saying a number is less than or equal to the maximum of two others. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypothesis istsr.1 
|- X = dom R
Assertion tsrlemax 
|- ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A R if ( B R C , C , B ) <-> ( A R B \/ A R C ) ) )

Proof

Step Hyp Ref Expression
1 istsr.1 
 |-  X = dom R
2 breq2 
 |-  ( C = if ( B R C , C , B ) -> ( A R C <-> A R if ( B R C , C , B ) ) )
3 2 bibi1d 
 |-  ( C = if ( B R C , C , B ) -> ( ( A R C <-> ( A R B \/ A R C ) ) <-> ( A R if ( B R C , C , B ) <-> ( A R B \/ A R C ) ) ) )
4 breq2 
 |-  ( B = if ( B R C , C , B ) -> ( A R B <-> A R if ( B R C , C , B ) ) )
5 4 bibi1d 
 |-  ( B = if ( B R C , C , B ) -> ( ( A R B <-> ( A R B \/ A R C ) ) <-> ( A R if ( B R C , C , B ) <-> ( A R B \/ A R C ) ) ) )
6 olc 
 |-  ( A R C -> ( A R B \/ A R C ) )
7 eqid 
 |-  dom R = dom R
8 7 istsr 
 |-  ( R e. TosetRel <-> ( R e. PosetRel /\ ( dom R X. dom R ) C_ ( R u. `' R ) ) )
9 8 simplbi 
 |-  ( R e. TosetRel -> R e. PosetRel )
10 pstr 
 |-  ( ( R e. PosetRel /\ A R B /\ B R C ) -> A R C )
11 10 3expib 
 |-  ( R e. PosetRel -> ( ( A R B /\ B R C ) -> A R C ) )
12 9 11 syl 
 |-  ( R e. TosetRel -> ( ( A R B /\ B R C ) -> A R C ) )
13 12 adantr 
 |-  ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A R B /\ B R C ) -> A R C ) )
14 13 expdimp 
 |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R B ) -> ( B R C -> A R C ) )
15 14 impancom 
 |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ B R C ) -> ( A R B -> A R C ) )
16 idd 
 |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ B R C ) -> ( A R C -> A R C ) )
17 15 16 jaod 
 |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ B R C ) -> ( ( A R B \/ A R C ) -> A R C ) )
18 6 17 impbid2 
 |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ B R C ) -> ( A R C <-> ( A R B \/ A R C ) ) )
19 orc 
 |-  ( A R B -> ( A R B \/ A R C ) )
20 idd 
 |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ -. B R C ) -> ( A R B -> A R B ) )
21 1 tsrlin 
 |-  ( ( R e. TosetRel /\ B e. X /\ C e. X ) -> ( B R C \/ C R B ) )
22 21 3adant3r1 
 |-  ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B R C \/ C R B ) )
23 22 orcanai 
 |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ -. B R C ) -> C R B )
24 pstr 
 |-  ( ( R e. PosetRel /\ A R C /\ C R B ) -> A R B )
25 24 3expib 
 |-  ( R e. PosetRel -> ( ( A R C /\ C R B ) -> A R B ) )
26 9 25 syl 
 |-  ( R e. TosetRel -> ( ( A R C /\ C R B ) -> A R B ) )
27 26 adantr 
 |-  ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A R C /\ C R B ) -> A R B ) )
28 27 expdimp 
 |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R C ) -> ( C R B -> A R B ) )
29 28 impancom 
 |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ C R B ) -> ( A R C -> A R B ) )
30 23 29 syldan 
 |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ -. B R C ) -> ( A R C -> A R B ) )
31 20 30 jaod 
 |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ -. B R C ) -> ( ( A R B \/ A R C ) -> A R B ) )
32 19 31 impbid2 
 |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ -. B R C ) -> ( A R B <-> ( A R B \/ A R C ) ) )
33 3 5 18 32 ifbothda 
 |-  ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A R if ( B R C , C , B ) <-> ( A R B \/ A R C ) ) )