| Step |
Hyp |
Ref |
Expression |
| 1 |
|
latnle.b |
|- B = ( Base ` K ) |
| 2 |
|
latnle.l |
|- .<_ = ( le ` K ) |
| 3 |
|
latnle.s |
|- .< = ( lt ` K ) |
| 4 |
|
latnle.j |
|- .\/ = ( join ` K ) |
| 5 |
1 2 4
|
latlej1 |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X .<_ ( X .\/ Y ) ) |
| 6 |
5
|
biantrurd |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X =/= ( X .\/ Y ) <-> ( X .<_ ( X .\/ Y ) /\ X =/= ( X .\/ Y ) ) ) ) |
| 7 |
1 2 4
|
latleeqj1 |
|- ( ( K e. Lat /\ Y e. B /\ X e. B ) -> ( Y .<_ X <-> ( Y .\/ X ) = X ) ) |
| 8 |
7
|
3com23 |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( Y .<_ X <-> ( Y .\/ X ) = X ) ) |
| 9 |
|
eqcom |
|- ( ( Y .\/ X ) = X <-> X = ( Y .\/ X ) ) |
| 10 |
8 9
|
bitrdi |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( Y .<_ X <-> X = ( Y .\/ X ) ) ) |
| 11 |
1 4
|
latjcom |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) = ( Y .\/ X ) ) |
| 12 |
11
|
eqeq2d |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X = ( X .\/ Y ) <-> X = ( Y .\/ X ) ) ) |
| 13 |
10 12
|
bitr4d |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( Y .<_ X <-> X = ( X .\/ Y ) ) ) |
| 14 |
13
|
necon3bbid |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( -. Y .<_ X <-> X =/= ( X .\/ Y ) ) ) |
| 15 |
1 4
|
latjcl |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .\/ Y ) e. B ) |
| 16 |
2 3
|
pltval |
|- ( ( K e. Lat /\ X e. B /\ ( X .\/ Y ) e. B ) -> ( X .< ( X .\/ Y ) <-> ( X .<_ ( X .\/ Y ) /\ X =/= ( X .\/ Y ) ) ) ) |
| 17 |
15 16
|
syld3an3 |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .< ( X .\/ Y ) <-> ( X .<_ ( X .\/ Y ) /\ X =/= ( X .\/ Y ) ) ) ) |
| 18 |
6 14 17
|
3bitr4d |
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( -. Y .<_ X <-> X .< ( X .\/ Y ) ) ) |