Description: The half-line relation implies inequality. (Contributed by Thierry Arnoux, 22-Feb-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ishlg.p | |- P = ( Base ` G ) |
|
ishlg.i | |- I = ( Itv ` G ) |
||
ishlg.k | |- K = ( hlG ` G ) |
||
ishlg.a | |- ( ph -> A e. P ) |
||
ishlg.b | |- ( ph -> B e. P ) |
||
ishlg.c | |- ( ph -> C e. P ) |
||
ishlg.g | |- ( ph -> G e. V ) |
||
hlcomd.1 | |- ( ph -> A ( K ` C ) B ) |
||
Assertion | hlne2 | |- ( ph -> B =/= C ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ishlg.p | |- P = ( Base ` G ) |
|
2 | ishlg.i | |- I = ( Itv ` G ) |
|
3 | ishlg.k | |- K = ( hlG ` G ) |
|
4 | ishlg.a | |- ( ph -> A e. P ) |
|
5 | ishlg.b | |- ( ph -> B e. P ) |
|
6 | ishlg.c | |- ( ph -> C e. P ) |
|
7 | ishlg.g | |- ( ph -> G e. V ) |
|
8 | hlcomd.1 | |- ( ph -> A ( K ` C ) B ) |
|
9 | 1 2 3 4 5 6 7 | ishlg | |- ( ph -> ( A ( K ` C ) B <-> ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) ) |
10 | 8 9 | mpbid | |- ( ph -> ( A =/= C /\ B =/= C /\ ( A e. ( C I B ) \/ B e. ( C I A ) ) ) ) |
11 | 10 | simp2d | |- ( ph -> B =/= C ) |