Description: The covers relation implies the negation of the converse "less than or equal to" relation. (Contributed by NM, 18-Oct-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cvrle.b | |- B = ( Base ` K ) |
|
cvrle.l | |- .<_ = ( le ` K ) |
||
cvrle.c | |- C = ( |
||
Assertion | cvrnle | |- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X C Y ) -> -. Y .<_ X ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cvrle.b | |- B = ( Base ` K ) |
|
2 | cvrle.l | |- .<_ = ( le ` K ) |
|
3 | cvrle.c | |- C = ( |
|
4 | eqid | |- ( lt ` K ) = ( lt ` K ) |
|
5 | 1 4 3 | cvrlt | |- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X C Y ) -> X ( lt ` K ) Y ) |
6 | 1 2 4 | pltnle | |- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X ( lt ` K ) Y ) -> -. Y .<_ X ) |
7 | 5 6 | syldan | |- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X C Y ) -> -. Y .<_ X ) |