# 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 ) )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 ) )`
` |-  ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A R C /\ C R B ) -> A R B ) )`
` |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A R C ) -> ( C R B -> A R B ) )`
` |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ C R B ) -> ( A R C -> A R B ) )`
` |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ -. B R C ) -> ( A R C -> A R B ) )`
` |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ -. B R C ) -> ( ( A R B \/ A R C ) -> A R B ) )`
` |-  ( ( ( R e. TosetRel /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ -. B R C ) -> ( A R B <-> ( A R B \/ A R C ) ) )`
` |-  ( ( 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 ) ) )`