Description: A join's first argument is less than or equal to the join. Special case of latlej1 to show an atom is on a line. (Contributed by NM, 15-May-2013)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hlatlej.l | |- .<_ = ( le ` K ) |
|
| hlatlej.j | |- .\/ = ( join ` K ) |
||
| hlatlej.a | |- A = ( Atoms ` K ) |
||
| Assertion | hlatlej1 | |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> P .<_ ( P .\/ Q ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hlatlej.l | |- .<_ = ( le ` K ) |
|
| 2 | hlatlej.j | |- .\/ = ( join ` K ) |
|
| 3 | hlatlej.a | |- A = ( Atoms ` K ) |
|
| 4 | hllat | |- ( K e. HL -> K e. Lat ) |
|
| 5 | eqid | |- ( Base ` K ) = ( Base ` K ) |
|
| 6 | 5 3 | atbase | |- ( P e. A -> P e. ( Base ` K ) ) |
| 7 | 5 3 | atbase | |- ( Q e. A -> Q e. ( Base ` K ) ) |
| 8 | 5 1 2 | latlej1 | |- ( ( K e. Lat /\ P e. ( Base ` K ) /\ Q e. ( Base ` K ) ) -> P .<_ ( P .\/ Q ) ) |
| 9 | 4 6 7 8 | syl3an | |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> P .<_ ( P .\/ Q ) ) |