Description: A join's second argument is less than or equal to the join. Special case of latlej2 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 | hlatlej2 | |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> Q .<_ ( P .\/ Q ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hlatlej.l | |- .<_ = ( le ` K ) |
|
| 2 | hlatlej.j | |- .\/ = ( join ` K ) |
|
| 3 | hlatlej.a | |- A = ( Atoms ` K ) |
|
| 4 | 1 2 3 | hlatlej1 | |- ( ( K e. HL /\ Q e. A /\ P e. A ) -> Q .<_ ( Q .\/ P ) ) |
| 5 | 4 | 3com23 | |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> Q .<_ ( Q .\/ P ) ) |
| 6 | 2 3 | hlatjcom | |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) = ( Q .\/ P ) ) |
| 7 | 5 6 | breqtrrd | |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> Q .<_ ( P .\/ Q ) ) |