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 ) , `' .<_ >. )