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→ARifBRCCB↔ARB∨ARC

Proof

Step Hyp Ref Expression
1 istsr.1 ⊢X=dom⁡R
2 breq2 ⊢C=ifBRCCB→ARC↔ARifBRCCB
3 2 bibi1d ⊢C=ifBRCCB→ARC↔ARB∨ARC↔ARifBRCCB↔ARB∨ARC
4 breq2 ⊢B=ifBRCCB→ARB↔ARifBRCCB
5 4 bibi1d ⊢B=ifBRCCB→ARB↔ARB∨ARC↔ARifBRCCB↔ARB∨ARC
6 olc ⊢ARC→ARB∨ARC
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∧ARB∧BRC→ARC
11 10 3expib ⊢R∈PosetRel→ARB∧BRC→ARC
12 9 11 syl ⊢R∈TosetRel→ARB∧BRC→ARC
13 12 adantr ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X→ARB∧BRC→ARC
14 13 expdimp ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X∧ARB→BRC→ARC
15 14 impancom ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X∧BRC→ARB→ARC
16 idd ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X∧BRC→ARC→ARC
17 15 16 jaod ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X∧BRC→ARB∨ARC→ARC
18 6 17 impbid2 ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X∧BRC→ARC↔ARB∨ARC
19 orc ⊢ARB→ARB∨ARC
20 idd ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X∧¬BRC→ARB→ARB
21 1 tsrlin ⊢R∈TosetRel∧B∈X∧C∈X→BRC∨CRB
22 21 3adant3r1 ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X→BRC∨CRB
23 22 orcanai ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X∧¬BRC→CRB
24 pstr ⊢R∈PosetRel∧ARC∧CRB→ARB
25 24 3expib ⊢R∈PosetRel→ARC∧CRB→ARB
26 9 25 syl ⊢R∈TosetRel→ARC∧CRB→ARB
27 26 adantr ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X→ARC∧CRB→ARB
28 27 expdimp ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X∧ARC→CRB→ARB
29 28 impancom ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X∧CRB→ARC→ARB
30 23 29 syldan ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X∧¬BRC→ARC→ARB
31 20 30 jaod ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X∧¬BRC→ARB∨ARC→ARB
32 19 31 impbid2 ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X∧¬BRC→ARB↔ARB∨ARC
33 3 5 18 32 ifbothda ⊢R∈TosetRel∧A∈X∧B∈X∧C∈X→ARifBRCCB↔ARB∨ARC