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 ˙ = K
cvrletr.s < ˙ = < K
cvrletr.c C = K
Assertion cvrnbtwn3 K Poset X B Y B Z B X C Y X ˙ Z Z < ˙ Y X = Z

Proof

Step Hyp Ref Expression
1 cvrletr.b B = Base K
2 cvrletr.l ˙ = K
3 cvrletr.s < ˙ = < K
4 cvrletr.c C = K
5 1 3 4 cvrnbtwn K Poset X B Y B Z B X C Y ¬ X < ˙ Z Z < ˙ Y
6 2 3 pltval K Poset X B Z B X < ˙ Z X ˙ Z X Z
7 6 3adant3r2 K Poset X B Y B Z B X < ˙ Z X ˙ Z X Z
8 7 3adant3 K Poset X B Y B Z B X C Y X < ˙ Z X ˙ Z X Z
9 8 anbi1d K Poset X B Y B Z B X C Y X < ˙ Z Z < ˙ Y X ˙ Z X Z Z < ˙ Y
10 9 notbid K Poset X B Y B Z 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 Poset X B Y B Z B X C Y ¬ X < ˙ Z Z < ˙ Y X ˙ Z Z < ˙ Y X = Z
19 5 18 mpbid K Poset X B Y B Z B X C Y X ˙ Z Z < ˙ Y X = Z
20 1 2 posref K Poset X B X ˙ X
21 breq2 X = Z X ˙ X X ˙ Z
22 20 21 syl5ibcom K Poset X B X = Z X ˙ Z
23 22 3ad2antr1 K Poset X B Y B Z B X = Z X ˙ Z
24 23 3adant3 K Poset X B Y B Z B X C Y X = Z X ˙ Z
25 simp1 K Poset X B Y B Z B X C Y K Poset
26 simp21 K Poset X B Y B Z B X C Y X B
27 simp22 K Poset X B Y B Z B X C Y Y B
28 simp3 K Poset X B Y B Z B X C Y X C Y
29 1 3 4 cvrlt K Poset X B Y B X C Y X < ˙ Y
30 25 26 27 28 29 syl31anc K Poset X B Y B Z B X C Y X < ˙ Y
31 breq1 X = Z X < ˙ Y Z < ˙ Y
32 30 31 syl5ibcom K Poset X B Y B Z B X C Y X = Z Z < ˙ Y
33 24 32 jcad K Poset X B Y B Z B X C Y X = Z X ˙ Z Z < ˙ Y
34 19 33 impbid K Poset X B Y B Z B X C Y X ˙ Z Z < ˙ Y X = Z