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 ) ) |