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 ⊢ 𝑋 = dom 𝑅
Assertion tsrlemax ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐶 , 𝐵 ) ↔ ( 𝐴 𝑅 𝐵 ∨ 𝐴 𝑅 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 istsr.1 ⊢ 𝑋 = dom 𝑅
2 breq2 ⊢ ( 𝐶 = if ( 𝐵 𝑅 𝐶 , 𝐶 , 𝐵 ) → ( 𝐴 𝑅 𝐶 ↔ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐶 , 𝐵 ) ) )
3 2 bibi1d ⊢ ( 𝐶 = if ( 𝐵 𝑅 𝐶 , 𝐶 , 𝐵 ) → ( ( 𝐴 𝑅 𝐶 ↔ ( 𝐴 𝑅 𝐵 ∨ 𝐴 𝑅 𝐶 ) ) ↔ ( 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐶 , 𝐵 ) ↔ ( 𝐴 𝑅 𝐵 ∨ 𝐴 𝑅 𝐶 ) ) ) )
4 breq2 ⊢ ( 𝐵 = if ( 𝐵 𝑅 𝐶 , 𝐶 , 𝐵 ) → ( 𝐴 𝑅 𝐵 ↔ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐶 , 𝐵 ) ) )
5 4 bibi1d ⊢ ( 𝐵 = if ( 𝐵 𝑅 𝐶 , 𝐶 , 𝐵 ) → ( ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 𝑅 𝐵 ∨ 𝐴 𝑅 𝐶 ) ) ↔ ( 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐶 , 𝐵 ) ↔ ( 𝐴 𝑅 𝐵 ∨ 𝐴 𝑅 𝐶 ) ) ) )
6 olc ⊢ ( 𝐴 𝑅 𝐶 → ( 𝐴 𝑅 𝐵 ∨ 𝐴 𝑅 𝐶 ) )
7 eqid ⊢ dom 𝑅 = dom 𝑅
8 7 istsr ⊢ ( 𝑅 ∈ TosetRel ↔ ( 𝑅 ∈ PosetRel ∧ ( dom 𝑅 × dom 𝑅 ) ⊆ ( 𝑅 ∪ ◡ 𝑅 ) ) )
9 8 simplbi ⊢ ( 𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel )
10 pstr ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 )
11 10 3expib ⊢ ( 𝑅 ∈ PosetRel → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) )
12 9 11 syl ⊢ ( 𝑅 ∈ TosetRel → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) )
13 12 adantr ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) )
14 13 expdimp ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 𝐵 ) → ( 𝐵 𝑅 𝐶 → 𝐴 𝑅 𝐶 ) )
15 14 impancom ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐵 𝑅 𝐶 ) → ( 𝐴 𝑅 𝐵 → 𝐴 𝑅 𝐶 ) )
16 idd ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐵 𝑅 𝐶 ) → ( 𝐴 𝑅 𝐶 → 𝐴 𝑅 𝐶 ) )
17 15 16 jaod ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐵 𝑅 𝐶 ) → ( ( 𝐴 𝑅 𝐵 ∨ 𝐴 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) )
18 6 17 impbid2 ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐵 𝑅 𝐶 ) → ( 𝐴 𝑅 𝐶 ↔ ( 𝐴 𝑅 𝐵 ∨ 𝐴 𝑅 𝐶 ) ) )
19 orc ⊢ ( 𝐴 𝑅 𝐵 → ( 𝐴 𝑅 𝐵 ∨ 𝐴 𝑅 𝐶 ) )
20 idd ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ ¬ 𝐵 𝑅 𝐶 ) → ( 𝐴 𝑅 𝐵 → 𝐴 𝑅 𝐵 ) )
21 1 tsrlin ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) )
22 21 3adant3r1 ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝑅 𝐶 ∨ 𝐶 𝑅 𝐵 ) )
23 22 orcanai ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ ¬ 𝐵 𝑅 𝐶 ) → 𝐶 𝑅 𝐵 )
24 pstr ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 𝑅 𝐶 ∧ 𝐶 𝑅 𝐵 ) → 𝐴 𝑅 𝐵 )
25 24 3expib ⊢ ( 𝑅 ∈ PosetRel → ( ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑅 𝐵 ) → 𝐴 𝑅 𝐵 ) )
26 9 25 syl ⊢ ( 𝑅 ∈ TosetRel → ( ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑅 𝐵 ) → 𝐴 𝑅 𝐵 ) )
27 26 adantr ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑅 𝐵 ) → 𝐴 𝑅 𝐵 ) )
28 27 expdimp ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 𝐶 ) → ( 𝐶 𝑅 𝐵 → 𝐴 𝑅 𝐵 ) )
29 28 impancom ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐶 𝑅 𝐵 ) → ( 𝐴 𝑅 𝐶 → 𝐴 𝑅 𝐵 ) )
30 23 29 syldan ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ ¬ 𝐵 𝑅 𝐶 ) → ( 𝐴 𝑅 𝐶 → 𝐴 𝑅 𝐵 ) )
31 20 30 jaod ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ ¬ 𝐵 𝑅 𝐶 ) → ( ( 𝐴 𝑅 𝐵 ∨ 𝐴 𝑅 𝐶 ) → 𝐴 𝑅 𝐵 ) )
32 19 31 impbid2 ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ ¬ 𝐵 𝑅 𝐶 ) → ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 𝑅 𝐵 ∨ 𝐴 𝑅 𝐶 ) ) )
33 3 5 18 32 ifbothda ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐶 , 𝐵 ) ↔ ( 𝐴 𝑅 𝐵 ∨ 𝐴 𝑅 𝐶 ) ) )