This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: A join is less than or equal to a third value iff each argument is less than or equal to the third value. ( chlub analog.) (Contributed by NM, 17-Sep-2011)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | latlej.b | ||
| latlej.l | |||
| latlej.j | |||
| Assertion | latjle12 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | latlej.b | ||
| 2 | latlej.l | ||
| 3 | latlej.j | ||
| 4 | latpos | ||
| 5 | 4 | adantr | |
| 6 | simpr1 | ||
| 7 | simpr2 | ||
| 8 | simpr3 | ||
| 9 | eqid | ||
| 10 | simpl | ||
| 11 | 1 3 9 10 6 7 | latcl2 | |
| 12 | 11 | simpld | |
| 13 | 1 2 3 5 6 7 8 12 | joinle |