This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: A join's first argument is less than or equal to the join. ( chub1 analog.) (Contributed by NM, 17-Sep-2011)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | latlej.b | ||
| latlej.l | |||
| latlej.j | |||
| Assertion | latlej1 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | latlej.b | ||
| 2 | latlej.l | ||
| 3 | latlej.j | ||
| 4 | simp1 | ||
| 5 | simp2 | ||
| 6 | simp3 | ||
| 7 | eqid | ||
| 8 | 1 3 7 4 5 6 | latcl2 | |
| 9 | 8 | simpld | |
| 10 | 1 2 3 4 5 6 9 | lejoin1 |