Description: The covers relation implies the "less than or equal to" relation. (Contributed by NM, 12-Oct-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cvrle.b | |- B = ( Base ` K ) |
|
cvrle.l | |- .<_ = ( le ` K ) |
||
cvrle.c | |- C = ( |
||
Assertion | cvrle | |- ( ( ( K e. A /\ X e. B /\ Y e. B ) /\ X C Y ) -> X .<_ Y ) |
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. A /\ X e. B /\ Y e. B ) /\ X C Y ) -> X ( lt ` K ) Y ) |
6 | 2 4 | pltval | |- ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X ( lt ` K ) Y <-> ( X .<_ Y /\ X =/= Y ) ) ) |
7 | 6 | simprbda | |- ( ( ( K e. A /\ X e. B /\ Y e. B ) /\ X ( lt ` K ) Y ) -> X .<_ Y ) |
8 | 5 7 | syldan | |- ( ( ( K e. A /\ X e. B /\ Y e. B ) /\ X C Y ) -> X .<_ Y ) |