This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cvrnbtwn3

Description: The covers relation implies no in-betweenness. ( cvnbtwn3 analog.) (Contributed by NM, 4-Nov-2011)

Ref Expression
Hypotheses cvrletr.b 
|- B = ( Base ` K )
cvrletr.l 
|- .<_ = ( le ` K )
cvrletr.s 
|- .< = ( lt ` K )
cvrletr.c 
|- C = (
Assertion cvrnbtwn3 
|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( ( X .<_ Z /\ Z .< Y ) <-> X = Z ) )

Proof

Step Hyp Ref Expression
1 cvrletr.b 
 |-  B = ( Base ` K )
2 cvrletr.l 
 |-  .<_ = ( le ` K )
3 cvrletr.s 
 |-  .< = ( lt ` K )
4 cvrletr.c 
 |-  C = (
5 1 3 4 cvrnbtwn 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> -. ( X .< Z /\ Z .< Y ) )
6 2 3 pltval 
 |-  ( ( K e. Poset /\ X e. B /\ Z e. B ) -> ( X .< Z <-> ( X .<_ Z /\ X =/= Z ) ) )
7 6 3adant3r2 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .< Z <-> ( X .<_ Z /\ X =/= Z ) ) )
8 7 3adant3 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( X .< Z <-> ( X .<_ Z /\ X =/= Z ) ) )
9 8 anbi1d 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( ( X .< Z /\ Z .< Y ) <-> ( ( X .<_ Z /\ X =/= Z ) /\ Z .< Y ) ) )
10 9 notbid 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( -. ( X .< Z /\ Z .< Y ) <-> -. ( ( X .<_ Z /\ X =/= Z ) /\ Z .< Y ) ) )
11 an32 
 |-  ( ( ( X .<_ Z /\ X =/= Z ) /\ Z .< Y ) <-> ( ( X .<_ Z /\ Z .< Y ) /\ X =/= Z ) )
12 df-ne 
 |-  ( X =/= Z <-> -. X = Z )
13 12 anbi2i 
 |-  ( ( ( X .<_ Z /\ Z .< Y ) /\ X =/= Z ) <-> ( ( X .<_ Z /\ Z .< Y ) /\ -. X = Z ) )
14 11 13 bitri 
 |-  ( ( ( X .<_ Z /\ X =/= Z ) /\ Z .< Y ) <-> ( ( X .<_ Z /\ Z .< Y ) /\ -. X = Z ) )
15 14 notbii 
 |-  ( -. ( ( X .<_ Z /\ X =/= Z ) /\ Z .< Y ) <-> -. ( ( X .<_ Z /\ Z .< Y ) /\ -. X = Z ) )
16 iman 
 |-  ( ( ( X .<_ Z /\ Z .< Y ) -> X = Z ) <-> -. ( ( X .<_ Z /\ Z .< Y ) /\ -. X = Z ) )
17 15 16 bitr4i 
 |-  ( -. ( ( X .<_ Z /\ X =/= Z ) /\ Z .< Y ) <-> ( ( X .<_ Z /\ Z .< Y ) -> X = Z ) )
18 10 17 bitrdi 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( -. ( X .< Z /\ Z .< Y ) <-> ( ( X .<_ Z /\ Z .< Y ) -> X = Z ) ) )
19 5 18 mpbid 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( ( X .<_ Z /\ Z .< Y ) -> X = Z ) )
20 1 2 posref 
 |-  ( ( K e. Poset /\ X e. B ) -> X .<_ X )
21 breq2 
 |-  ( X = Z -> ( X .<_ X <-> X .<_ Z ) )
22 20 21 syl5ibcom 
 |-  ( ( K e. Poset /\ X e. B ) -> ( X = Z -> X .<_ Z ) )
23 22 3ad2antr1 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X = Z -> X .<_ Z ) )
24 23 3adant3 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( X = Z -> X .<_ Z ) )
25 simp1 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> K e. Poset )
26 simp21 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> X e. B )
27 simp22 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> Y e. B )
28 simp3 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> X C Y )
29 1 3 4 cvrlt 
 |-  ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X C Y ) -> X .< Y )
30 25 26 27 28 29 syl31anc 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> X .< Y )
31 breq1 
 |-  ( X = Z -> ( X .< Y <-> Z .< Y ) )
32 30 31 syl5ibcom 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( X = Z -> Z .< Y ) )
33 24 32 jcad 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( X = Z -> ( X .<_ Z /\ Z .< Y ) ) )
34 19 33 impbid 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( ( X .<_ Z /\ Z .< Y ) <-> X = Z ) )