Metamath Proof Explorer


Theorem cvrval

Description: Binary relation expressing B covers A , which means that B is larger than A and there is nothing in between. Definition 3.2.18 of PtakPulmannova p. 68. ( cvbr analog.) (Contributed by NM, 18-Sep-2011)

Ref Expression
Hypotheses cvrfval.b B = Base K
cvrfval.s < ˙ = < K
cvrfval.c C = K
Assertion cvrval K A X B Y B X C Y X < ˙ Y ¬ z B X < ˙ z z < ˙ Y

Proof

Step Hyp Ref Expression
1 cvrfval.b B = Base K
2 cvrfval.s < ˙ = < K
3 cvrfval.c C = K
4 1 2 3 cvrfval K A C = x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y
5 3anass x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y
6 5 opabbii x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y = x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y
7 4 6 syl6eq K A C = x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y
8 7 breqd K A X C Y X x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y Y
9 8 3ad2ant1 K A X B Y B X C Y X x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y Y
10 df-br X x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y Y X Y x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y
11 breq1 x = X x < ˙ y X < ˙ y
12 breq1 x = X x < ˙ z X < ˙ z
13 12 anbi1d x = X x < ˙ z z < ˙ y X < ˙ z z < ˙ y
14 13 rexbidv x = X z B x < ˙ z z < ˙ y z B X < ˙ z z < ˙ y
15 14 notbid x = X ¬ z B x < ˙ z z < ˙ y ¬ z B X < ˙ z z < ˙ y
16 11 15 anbi12d x = X x < ˙ y ¬ z B x < ˙ z z < ˙ y X < ˙ y ¬ z B X < ˙ z z < ˙ y
17 breq2 y = Y X < ˙ y X < ˙ Y
18 breq2 y = Y z < ˙ y z < ˙ Y
19 18 anbi2d y = Y X < ˙ z z < ˙ y X < ˙ z z < ˙ Y
20 19 rexbidv y = Y z B X < ˙ z z < ˙ y z B X < ˙ z z < ˙ Y
21 20 notbid y = Y ¬ z B X < ˙ z z < ˙ y ¬ z B X < ˙ z z < ˙ Y
22 17 21 anbi12d y = Y X < ˙ y ¬ z B X < ˙ z z < ˙ y X < ˙ Y ¬ z B X < ˙ z z < ˙ Y
23 16 22 opelopab2 X B Y B X Y x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y X < ˙ Y ¬ z B X < ˙ z z < ˙ Y
24 10 23 syl5bb X B Y B X x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y Y X < ˙ Y ¬ z B X < ˙ z z < ˙ Y
25 24 3adant1 K A X B Y B X x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y Y X < ˙ Y ¬ z B X < ˙ z z < ˙ Y
26 9 25 bitrd K A X B Y B X C Y X < ˙ Y ¬ z B X < ˙ z z < ˙ Y