Metamath Proof Explorer


Theorem cvrfval

Description: Value of covers relation "is covered by". (Contributed by NM, 18-Sep-2011)

Ref Expression
Hypotheses cvrfval.b B = Base K
cvrfval.s < ˙ = < K
cvrfval.c C = K
Assertion cvrfval K A C = x y | x B y B 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 elex K A K V
5 fveq2 p = K Base p = Base K
6 5 1 eqtr4di p = K Base p = B
7 6 eleq2d p = K x Base p x B
8 6 eleq2d p = K y Base p y B
9 7 8 anbi12d p = K x Base p y Base p x B y B
10 fveq2 p = K < p = < K
11 10 2 eqtr4di p = K < p = < ˙
12 11 breqd p = K x < p y x < ˙ y
13 11 breqd p = K x < p z x < ˙ z
14 11 breqd p = K z < p y z < ˙ y
15 13 14 anbi12d p = K x < p z z < p y x < ˙ z z < ˙ y
16 6 15 rexeqbidv p = K z Base p x < p z z < p y z B x < ˙ z z < ˙ y
17 16 notbid p = K ¬ z Base p x < p z z < p y ¬ z B x < ˙ z z < ˙ y
18 9 12 17 3anbi123d p = K x Base p y Base p x < p y ¬ z Base p x < p z z < p y x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y
19 18 opabbidv p = K x y | x Base p y Base p x < p y ¬ z Base p x < p z z < p y = x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y
20 df-covers = p V x y | x Base p y Base p x < p y ¬ z Base p x < p z z < p y
21 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
22 21 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
23 1 fvexi B V
24 23 23 xpex B × B V
25 opabssxp x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y B × B
26 24 25 ssexi x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y V
27 22 26 eqeltri x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y V
28 19 20 27 fvmpt K V K = x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y
29 3 28 syl5eq K V C = x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y
30 4 29 syl K A C = x y | x B y B x < ˙ y ¬ z B x < ˙ z z < ˙ y