Description: The covers relation implies inequality. (Contributed by NM, 13-Oct-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cvrne.b | |- B = ( Base ` K ) |
|
cvrne.c | |- C = ( |
||
Assertion | cvrne | |- ( ( ( K e. A /\ X e. B /\ Y e. B ) /\ X C Y ) -> X =/= Y ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cvrne.b | |- B = ( Base ` K ) |
|
2 | cvrne.c | |- C = ( |
|
3 | eqid | |- ( lt ` K ) = ( lt ` K ) |
|
4 | 1 3 2 | cvrlt | |- ( ( ( K e. A /\ X e. B /\ Y e. B ) /\ X C Y ) -> X ( lt ` K ) Y ) |
5 | eqid | |- ( le ` K ) = ( le ` K ) |
|
6 | 5 3 | pltval | |- ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X ( lt ` K ) Y <-> ( X ( le ` K ) Y /\ X =/= Y ) ) ) |
7 | 6 | simplbda | |- ( ( ( K e. A /\ X e. B /\ Y e. B ) /\ X ( lt ` K ) Y ) -> X =/= Y ) |
8 | 4 7 | syldan | |- ( ( ( K e. A /\ X e. B /\ Y e. B ) /\ X C Y ) -> X =/= Y ) |