Metamath Proof Explorer

Theorem cvrnbtwn4

Description: The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of MaedaMaeda p. 31. ( cvnbtwn4 analog.) (Contributed by NM, 18-Oct-2011)

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

Proof

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 cvrnbtwn 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> -. ( X ( lt ` K ) Z /\ Z ( lt ` K ) Y ) )
6 iman 
 |-  ( ( ( X .<_ Z /\ Z .<_ Y ) -> ( X = Z \/ Z = Y ) ) <-> -. ( ( X .<_ Z /\ Z .<_ Y ) /\ -. ( X = Z \/ Z = Y ) ) )
7 neanior 
 |-  ( ( X =/= Z /\ Z =/= Y ) <-> -. ( X = Z \/ Z = Y ) )
8 7 anbi2i 
 |-  ( ( ( X .<_ Z /\ Z .<_ Y ) /\ ( X =/= Z /\ Z =/= Y ) ) <-> ( ( X .<_ Z /\ Z .<_ Y ) /\ -. ( X = Z \/ Z = Y ) ) )
9 an4 
 |-  ( ( ( X .<_ Z /\ Z .<_ Y ) /\ ( X =/= Z /\ Z =/= Y ) ) <-> ( ( X .<_ Z /\ X =/= Z ) /\ ( Z .<_ Y /\ Z =/= Y ) ) )
10 8 9 bitr3i 
 |-  ( ( ( X .<_ Z /\ Z .<_ Y ) /\ -. ( X = Z \/ Z = Y ) ) <-> ( ( X .<_ Z /\ X =/= Z ) /\ ( Z .<_ Y /\ Z =/= Y ) ) )
11 2 4 pltval 
 |-  ( ( K e. Poset /\ X e. B /\ Z e. B ) -> ( X ( lt ` K ) Z <-> ( X .<_ Z /\ X =/= Z ) ) )
12 11 3adant3r2 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ( lt ` K ) Z <-> ( X .<_ Z /\ X =/= Z ) ) )
13 2 4 pltval 
 |-  ( ( K e. Poset /\ Z e. B /\ Y e. B ) -> ( Z ( lt ` K ) Y <-> ( Z .<_ Y /\ Z =/= Y ) ) )
14 13 3com23 
 |-  ( ( K e. Poset /\ Y e. B /\ Z e. B ) -> ( Z ( lt ` K ) Y <-> ( Z .<_ Y /\ Z =/= Y ) ) )
15 14 3adant3r1 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Z ( lt ` K ) Y <-> ( Z .<_ Y /\ Z =/= Y ) ) )
16 12 15 anbi12d 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ( lt ` K ) Z /\ Z ( lt ` K ) Y ) <-> ( ( X .<_ Z /\ X =/= Z ) /\ ( Z .<_ Y /\ Z =/= Y ) ) ) )
17 10 16 bitr4id 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( X .<_ Z /\ Z .<_ Y ) /\ -. ( X = Z \/ Z = Y ) ) <-> ( X ( lt ` K ) Z /\ Z ( lt ` K ) Y ) ) )
18 17 notbid 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( -. ( ( X .<_ Z /\ Z .<_ Y ) /\ -. ( X = Z \/ Z = Y ) ) <-> -. ( X ( lt ` K ) Z /\ Z ( lt ` K ) Y ) ) )
19 6 18 bitr2id 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( -. ( X ( lt ` K ) Z /\ Z ( lt ` K ) Y ) <-> ( ( X .<_ Z /\ Z .<_ Y ) -> ( X = Z \/ Z = Y ) ) ) )
20 19 3adant3 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( -. ( X ( lt ` K ) Z /\ Z ( lt ` K ) Y ) <-> ( ( X .<_ Z /\ Z .<_ Y ) -> ( X = Z \/ Z = Y ) ) ) )
21 5 20 mpbid 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( ( X .<_ Z /\ Z .<_ Y ) -> ( X = Z \/ Z = Y ) ) )
22 1 2 posref 
 |-  ( ( K e. Poset /\ Z e. B ) -> Z .<_ Z )
23 22 3ad2antr3 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z .<_ Z )
24 23 3adant3 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> Z .<_ Z )
25 breq1 
 |-  ( X = Z -> ( X .<_ Z <-> Z .<_ Z ) )
26 24 25 syl5ibrcom 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( X = Z -> X .<_ Z ) )
27 1 2 3 cvrle 
 |-  ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X C Y ) -> X .<_ Y )
28 27 ex 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X C Y -> X .<_ Y ) )
29 28 3adant3r3 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X C Y -> X .<_ Y ) )
30 29 3impia 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> X .<_ Y )
31 breq2 
 |-  ( Z = Y -> ( X .<_ Z <-> X .<_ Y ) )
32 30 31 syl5ibrcom 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( Z = Y -> X .<_ Z ) )
33 26 32 jaod 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( ( X = Z \/ Z = Y ) -> X .<_ Z ) )
34 breq1 
 |-  ( X = Z -> ( X .<_ Y <-> Z .<_ Y ) )
35 30 34 syl5ibcom 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( X = Z -> Z .<_ Y ) )
36 breq2 
 |-  ( Z = Y -> ( Z .<_ Z <-> Z .<_ Y ) )
37 24 36 syl5ibcom 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( Z = Y -> Z .<_ Y ) )
38 35 37 jaod 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( ( X = Z \/ Z = Y ) -> Z .<_ Y ) )
39 33 38 jcad 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( ( X = Z \/ Z = Y ) -> ( X .<_ Z /\ Z .<_ Y ) ) )
40 21 39 impbid 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( ( X .<_ Z /\ Z .<_ Y ) <-> ( X = Z \/ Z = Y ) ) )