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 )