Metamath Proof Explorer

Theorem oduleval

Description: Value of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015)

Ref Expression
Hypotheses oduval.d 
|- D = ( ODual ` O )
oduval.l 
|- .<_ = ( le ` O )
Assertion oduleval 
|- `' .<_ = ( le ` D )

Proof

Step Hyp Ref Expression
1 oduval.d 
 |-  D = ( ODual ` O )
2 oduval.l 
 |-  .<_ = ( le ` O )
3 fvex 
 |-  ( le ` O ) e. _V
4 3 cnvex 
 |-  `' ( le ` O ) e. _V
5 pleid 
 |-  le = Slot ( le ` ndx )
6 5 setsid 
 |-  ( ( O e. _V /\ `' ( le ` O ) e. _V ) -> `' ( le ` O ) = ( le ` ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) ) )
7 4 6 mpan2 
 |-  ( O e. _V -> `' ( le ` O ) = ( le ` ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) ) )
8 5 str0 
 |-  (/) = ( le ` (/) )
9 fvprc 
 |-  ( -. O e. _V -> ( le ` O ) = (/) )
10 9 cnveqd 
 |-  ( -. O e. _V -> `' ( le ` O ) = `' (/) )
11 cnv0 
 |-  `' (/) = (/)
12 10 11 eqtrdi 
 |-  ( -. O e. _V -> `' ( le ` O ) = (/) )
13 reldmsets 
 |-  Rel dom sSet
14 13 ovprc1 
 |-  ( -. O e. _V -> ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) = (/) )
15 14 fveq2d 
 |-  ( -. O e. _V -> ( le ` ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) ) = ( le ` (/) ) )
16 8 12 15 3eqtr4a 
 |-  ( -. O e. _V -> `' ( le ` O ) = ( le ` ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) ) )
17 7 16 pm2.61i 
 |-  `' ( le ` O ) = ( le ` ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) )
18 2 cnveqi 
 |-  `' .<_ = `' ( le ` O )
19 eqid 
 |-  ( le ` O ) = ( le ` O )
20 1 19 oduval 
 |-  D = ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. )
21 20 fveq2i 
 |-  ( le ` D ) = ( le ` ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) )
22 17 18 21 3eqtr4i 
 |-  `' .<_ = ( le ` D )