# 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}=\mathrm{dom}{R}$
Assertion tsrlemax ${⊢}\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{R}if\left({B}{R}{C},{C},{B}\right)↔\left({A}{R}{B}\vee {A}{R}{C}\right)\right)$

### Proof

Step Hyp Ref Expression
1 istsr.1 ${⊢}{X}=\mathrm{dom}{R}$
2 breq2 ${⊢}{C}=if\left({B}{R}{C},{C},{B}\right)\to \left({A}{R}{C}↔{A}{R}if\left({B}{R}{C},{C},{B}\right)\right)$
3 2 bibi1d ${⊢}{C}=if\left({B}{R}{C},{C},{B}\right)\to \left(\left({A}{R}{C}↔\left({A}{R}{B}\vee {A}{R}{C}\right)\right)↔\left({A}{R}if\left({B}{R}{C},{C},{B}\right)↔\left({A}{R}{B}\vee {A}{R}{C}\right)\right)\right)$
4 breq2 ${⊢}{B}=if\left({B}{R}{C},{C},{B}\right)\to \left({A}{R}{B}↔{A}{R}if\left({B}{R}{C},{C},{B}\right)\right)$
5 4 bibi1d ${⊢}{B}=if\left({B}{R}{C},{C},{B}\right)\to \left(\left({A}{R}{B}↔\left({A}{R}{B}\vee {A}{R}{C}\right)\right)↔\left({A}{R}if\left({B}{R}{C},{C},{B}\right)↔\left({A}{R}{B}\vee {A}{R}{C}\right)\right)\right)$
6 olc ${⊢}{A}{R}{C}\to \left({A}{R}{B}\vee {A}{R}{C}\right)$
7 eqid ${⊢}\mathrm{dom}{R}=\mathrm{dom}{R}$
8 7 istsr ${⊢}{R}\in \mathrm{TosetRel}↔\left({R}\in \mathrm{PosetRel}\wedge \mathrm{dom}{R}×\mathrm{dom}{R}\subseteq {R}\cup {{R}}^{-1}\right)$
9 8 simplbi ${⊢}{R}\in \mathrm{TosetRel}\to {R}\in \mathrm{PosetRel}$
10 pstr ${⊢}\left({R}\in \mathrm{PosetRel}\wedge {A}{R}{B}\wedge {B}{R}{C}\right)\to {A}{R}{C}$
11 10 3expib ${⊢}{R}\in \mathrm{PosetRel}\to \left(\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {A}{R}{C}\right)$
12 9 11 syl ${⊢}{R}\in \mathrm{TosetRel}\to \left(\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {A}{R}{C}\right)$
13 12 adantr ${⊢}\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left(\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {A}{R}{C}\right)$
14 13 expdimp ${⊢}\left(\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge {A}{R}{B}\right)\to \left({B}{R}{C}\to {A}{R}{C}\right)$
15 14 impancom ${⊢}\left(\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge {B}{R}{C}\right)\to \left({A}{R}{B}\to {A}{R}{C}\right)$
16 idd ${⊢}\left(\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge {B}{R}{C}\right)\to \left({A}{R}{C}\to {A}{R}{C}\right)$
17 15 16 jaod ${⊢}\left(\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge {B}{R}{C}\right)\to \left(\left({A}{R}{B}\vee {A}{R}{C}\right)\to {A}{R}{C}\right)$
18 6 17 impbid2 ${⊢}\left(\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge {B}{R}{C}\right)\to \left({A}{R}{C}↔\left({A}{R}{B}\vee {A}{R}{C}\right)\right)$
19 orc ${⊢}{A}{R}{B}\to \left({A}{R}{B}\vee {A}{R}{C}\right)$
20 idd ${⊢}\left(\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge ¬{B}{R}{C}\right)\to \left({A}{R}{B}\to {A}{R}{B}\right)$
21 1 tsrlin ${⊢}\left({R}\in \mathrm{TosetRel}\wedge {B}\in {X}\wedge {C}\in {X}\right)\to \left({B}{R}{C}\vee {C}{R}{B}\right)$
22 21 3adant3r1 ${⊢}\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({B}{R}{C}\vee {C}{R}{B}\right)$
23 22 orcanai ${⊢}\left(\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge ¬{B}{R}{C}\right)\to {C}{R}{B}$
24 pstr ${⊢}\left({R}\in \mathrm{PosetRel}\wedge {A}{R}{C}\wedge {C}{R}{B}\right)\to {A}{R}{B}$
25 24 3expib ${⊢}{R}\in \mathrm{PosetRel}\to \left(\left({A}{R}{C}\wedge {C}{R}{B}\right)\to {A}{R}{B}\right)$
26 9 25 syl ${⊢}{R}\in \mathrm{TosetRel}\to \left(\left({A}{R}{C}\wedge {C}{R}{B}\right)\to {A}{R}{B}\right)$
27 26 adantr ${⊢}\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left(\left({A}{R}{C}\wedge {C}{R}{B}\right)\to {A}{R}{B}\right)$
28 27 expdimp ${⊢}\left(\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge {A}{R}{C}\right)\to \left({C}{R}{B}\to {A}{R}{B}\right)$
29 28 impancom ${⊢}\left(\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge {C}{R}{B}\right)\to \left({A}{R}{C}\to {A}{R}{B}\right)$
30 23 29 syldan ${⊢}\left(\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge ¬{B}{R}{C}\right)\to \left({A}{R}{C}\to {A}{R}{B}\right)$
31 20 30 jaod ${⊢}\left(\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge ¬{B}{R}{C}\right)\to \left(\left({A}{R}{B}\vee {A}{R}{C}\right)\to {A}{R}{B}\right)$
32 19 31 impbid2 ${⊢}\left(\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\wedge ¬{B}{R}{C}\right)\to \left({A}{R}{B}↔\left({A}{R}{B}\vee {A}{R}{C}\right)\right)$
33 3 5 18 32 ifbothda ${⊢}\left({R}\in \mathrm{TosetRel}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{R}if\left({B}{R}{C},{C},{B}\right)↔\left({A}{R}{B}\vee {A}{R}{C}\right)\right)$