Theorem cvrnbtwn

Description: There is no element between the two arguments of the covers relation. ( cvnbtwn analog.) (Contributed by NM, 18-Oct-2011)

	Ref	Expression
Hypotheses	cvrfval.b	|- B = ( Base ` K )
	cvrfval.s	|- .< = ( lt ` K )
	cvrfval.c	|- C = (
Assertion	cvrnbtwn	|- ( ( K e. A /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> -. ( X .< Z /\ Z .< Y ) )

Proof

Step	Hyp	Ref	Expression
1		cvrfval.b	|- B = ( Base ` K )
2		cvrfval.s	|- .< = ( lt ` K )
3		cvrfval.c	|- C = (
4	1 2 3	cvrval	|- ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X .< Y /\ -. E. z e. B ( X .< z /\ z .< Y ) ) ) )
5	4	3adant3r3	|- ( ( K e. A /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C Y <-> ( X .< Y /\ -. E. z e. B ( X .< z /\ z .< Y ) ) ) )
6		ralnex	|- ( A. z e. B -. ( X .< z /\ z .< Y ) <-> -. E. z e. B ( X .< z /\ z .< Y ) )
7		breq2	|- ( z = Z -> ( X .< z <-> X .< Z ) )
8		breq1	|- ( z = Z -> ( z .< Y <-> Z .< Y ) )
9	7 8	anbi12d	|- ( z = Z -> ( ( X .< z /\ z .< Y ) <-> ( X .< Z /\ Z .< Y ) ) )
10	9	notbid	|- ( z = Z -> ( -. ( X .< z /\ z .< Y ) <-> -. ( X .< Z /\ Z .< Y ) ) )
11	10	rspcv	|- ( Z e. B -> ( A. z e. B -. ( X .< z /\ z .< Y ) -> -. ( X .< Z /\ Z .< Y ) ) )
12	6 11	syl5bir	|- ( Z e. B -> ( -. E. z e. B ( X .< z /\ z .< Y ) -> -. ( X .< Z /\ Z .< Y ) ) )
13	12	adantld	|- ( Z e. B -> ( ( X .< Y /\ -. E. z e. B ( X .< z /\ z .< Y ) ) -> -. ( X .< Z /\ Z .< Y ) ) )
14	13	3ad2ant3	|- ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( X .< Y /\ -. E. z e. B ( X .< z /\ z .< Y ) ) -> -. ( X .< Z /\ Z .< Y ) ) )
15	14	adantl	|- ( ( K e. A /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ -. E. z e. B ( X .< z /\ z .< Y ) ) -> -. ( X .< Z /\ Z .< Y ) ) )
16	5 15	sylbid	|- ( ( K e. A /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C Y -> -. ( X .< Z /\ Z .< Y ) ) )
17	16	3impia	|- ( ( K e. A /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> -. ( X .< Z /\ Z .< Y ) )