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 ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ 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 ∈ TosetRel ↔ R ∈ PosetRel ∧ dom ⁡ R × dom ⁡ R ⊆ R ∪ R -1
9 8 simplbi ⊢ R ∈ TosetRel → R ∈ PosetRel
10 pstr ⊢ R ∈ PosetRel ∧ A R B ∧ B R C → A R C
11 10 3expib ⊢ R ∈ PosetRel → A R B ∧ B R C → A R C
12 9 11 syl ⊢ R ∈ TosetRel → A R B ∧ B R C → A R C
13 12 adantr ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A R B ∧ B R C → A R C
14 13 expdimp ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ A R B → B R C → A R C
15 14 impancom ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ B R C → A R B → A R C
16 idd ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ B R C → A R C → A R C
17 15 16 jaod ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ B R C → A R B ∨ A R C → A R C
18 6 17 impbid2 ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ 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 ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ ¬ B R C → A R B → A R B
21 1 tsrlin ⊢ R ∈ TosetRel ∧ B ∈ X ∧ C ∈ X → B R C ∨ C R B
22 21 3adant3r1 ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B R C ∨ C R B
23 22 orcanai ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ ¬ B R C → C R B
24 pstr ⊢ R ∈ PosetRel ∧ A R C ∧ C R B → A R B
25 24 3expib ⊢ R ∈ PosetRel → A R C ∧ C R B → A R B
26 9 25 syl ⊢ R ∈ TosetRel → A R C ∧ C R B → A R B
27 26 adantr ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A R C ∧ C R B → A R B
28 27 expdimp ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ A R C → C R B → A R B
29 28 impancom ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ C R B → A R C → A R B
30 23 29 syldan ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ ¬ B R C → A R C → A R B
31 20 30 jaod ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ ¬ B R C → A R B ∨ A R C → A R B
32 19 31 impbid2 ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ ¬ B R C → A R B ↔ A R B ∨ A R C
33 3 5 18 32 ifbothda ⊢ R ∈ TosetRel ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A R if B R C C B ↔ A R B ∨ A R C