# 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 syl6eq
` |-  ( -. 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 )`