Step |
Hyp |
Ref |
Expression |
1 |
|
pltnlt.b |
|- B = ( Base ` K ) |
2 |
|
pltnlt.s |
|- .< = ( lt ` K ) |
3 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
4 |
1 3 2
|
pltnle |
|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .< Y ) -> -. Y ( le ` K ) X ) |
5 |
3 2
|
pltle |
|- ( ( K e. Poset /\ Y e. B /\ X e. B ) -> ( Y .< X -> Y ( le ` K ) X ) ) |
6 |
5
|
3com23 |
|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( Y .< X -> Y ( le ` K ) X ) ) |
7 |
6
|
adantr |
|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .< Y ) -> ( Y .< X -> Y ( le ` K ) X ) ) |
8 |
4 7
|
mtod |
|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .< Y ) -> -. Y .< X ) |