# Metamath Proof Explorer

## Theorem oduval

Description: Value of 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 oduval
`|- D = ( O sSet <. ( le ` ndx ) , `' .<_ >. )`

### Proof

Step Hyp Ref Expression
1 oduval.d
` |-  D = ( ODual ` O )`
2 oduval.l
` |-  .<_ = ( le ` O )`
3 id
` |-  ( a = O -> a = O )`
4 fveq2
` |-  ( a = O -> ( le ` a ) = ( le ` O ) )`
5 4 cnveqd
` |-  ( a = O -> `' ( le ` a ) = `' ( le ` O ) )`
6 5 opeq2d
` |-  ( a = O -> <. ( le ` ndx ) , `' ( le ` a ) >. = <. ( le ` ndx ) , `' ( le ` O ) >. )`
7 3 6 oveq12d
` |-  ( a = O -> ( a sSet <. ( le ` ndx ) , `' ( le ` a ) >. ) = ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) )`
8 df-odu
` |-  ODual = ( a e. _V |-> ( a sSet <. ( le ` ndx ) , `' ( le ` a ) >. ) )`
9 ovex
` |-  ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) e. _V`
10 7 8 9 fvmpt
` |-  ( O e. _V -> ( ODual ` O ) = ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) )`
11 fvprc
` |-  ( -. O e. _V -> ( ODual ` O ) = (/) )`
12 reldmsets
` |-  Rel dom sSet`
13 12 ovprc1
` |-  ( -. O e. _V -> ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) = (/) )`
14 11 13 eqtr4d
` |-  ( -. O e. _V -> ( ODual ` O ) = ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) )`
15 10 14 pm2.61i
` |-  ( ODual ` O ) = ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. )`
16 2 cnveqi
` |-  `' .<_ = `' ( le ` O )`
17 16 opeq2i
` |-  <. ( le ` ndx ) , `' .<_ >. = <. ( le ` ndx ) , `' ( le ` O ) >.`
18 17 oveq2i
` |-  ( O sSet <. ( le ` ndx ) , `' .<_ >. ) = ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. )`
19 15 1 18 3eqtr4i
` |-  D = ( O sSet <. ( le ` ndx ) , `' .<_ >. )`