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 
|- .< = ( lt ` K )
cvrfval.c 
|- C = (
Assertion cvrfval 
|- ( K e. A -> C = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) } )

Proof

Step Hyp Ref Expression
1 cvrfval.b 
 |-  B = ( Base ` K )
2 cvrfval.s 
 |-  .< = ( lt ` K )
3 cvrfval.c 
 |-  C = (
4 elex 
 |-  ( K e. A -> K e. _V )
5 fveq2 
 |-  ( p = K -> ( Base ` p ) = ( Base ` K ) )
6 5 1 eqtr4di 
 |-  ( p = K -> ( Base ` p ) = B )
7 6 eleq2d 
 |-  ( p = K -> ( x e. ( Base ` p ) <-> x e. B ) )
8 6 eleq2d 
 |-  ( p = K -> ( y e. ( Base ` p ) <-> y e. B ) )
9 7 8 anbi12d 
 |-  ( p = K -> ( ( x e. ( Base ` p ) /\ y e. ( Base ` p ) ) <-> ( x e. B /\ y e. B ) ) )
10 fveq2 
 |-  ( p = K -> ( lt ` p ) = ( lt ` K ) )
11 10 2 eqtr4di 
 |-  ( p = K -> ( lt ` p ) = .< )
12 11 breqd 
 |-  ( p = K -> ( x ( lt ` p ) y <-> x .< y ) )
13 11 breqd 
 |-  ( p = K -> ( x ( lt ` p ) z <-> x .< z ) )
14 11 breqd 
 |-  ( p = K -> ( z ( lt ` p ) y <-> z .< y ) )
15 13 14 anbi12d 
 |-  ( p = K -> ( ( x ( lt ` p ) z /\ z ( lt ` p ) y ) <-> ( x .< z /\ z .< y ) ) )
16 6 15 rexeqbidv 
 |-  ( p = K -> ( E. z e. ( Base ` p ) ( x ( lt ` p ) z /\ z ( lt ` p ) y ) <-> E. z e. B ( x .< z /\ z .< y ) ) )
17 16 notbid 
 |-  ( p = K -> ( -. E. z e. ( Base ` p ) ( x ( lt ` p ) z /\ z ( lt ` p ) y ) <-> -. E. z e. B ( x .< z /\ z .< y ) ) )
18 9 12 17 3anbi123d 
 |-  ( p = K -> ( ( ( x e. ( Base ` p ) /\ y e. ( Base ` p ) ) /\ x ( lt ` p ) y /\ -. E. z e. ( Base ` p ) ( x ( lt ` p ) z /\ z ( lt ` p ) y ) ) <-> ( ( x e. B /\ y e. B ) /\ x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) )
19 18 opabbidv 
 |-  ( p = K -> { <. x , y >. | ( ( x e. ( Base ` p ) /\ y e. ( Base ` p ) ) /\ x ( lt ` p ) y /\ -. E. z e. ( Base ` p ) ( x ( lt ` p ) z /\ z ( lt ` p ) y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) } )
20 df-covers 
 |-   { <. x , y >. | ( ( x e. ( Base ` p ) /\ y e. ( Base ` p ) ) /\ x ( lt ` p ) y /\ -. E. z e. ( Base ` p ) ( x ( lt ` p ) z /\ z ( lt ` p ) y ) ) } )
21 3anass 
 |-  ( ( ( x e. B /\ y e. B ) /\ x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) <-> ( ( x e. B /\ y e. B ) /\ ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) )
22 21 opabbii 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) }
23 1 fvexi 
 |-  B e. _V
24 23 23 xpex 
 |-  ( B X. B ) e. _V
25 opabssxp 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) } C_ ( B X. B )
26 24 25 ssexi 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) ) } e. _V
27 22 26 eqeltri 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) } e. _V
28 19 20 27 fvmpt 
 |-  ( K e. _V -> ( . | ( ( x e. B /\ y e. B ) /\ x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) } )
29 3 28 syl5eq 
 |-  ( K e. _V -> C = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) } )
30 4 29 syl 
 |-  ( K e. A -> C = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) } )