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 ˙ = O
Assertion oduleval ˙ -1 = D

Proof

Step Hyp Ref Expression
1 oduval.d D = ODual O
2 oduval.l ˙ = O
3 fvex O V
4 3 cnvex O -1 V
5 pleid le = Slot ndx
6 5 setsid O V O -1 V O -1 = O sSet ndx O -1
7 4 6 mpan2 O V O -1 = O sSet ndx O -1
8 5 str0 =
9 fvprc ¬ O V O =
10 9 cnveqd ¬ O V O -1 = -1
11 cnv0 -1 =
12 10 11 syl6eq ¬ O V O -1 =
13 reldmsets Rel dom sSet
14 13 ovprc1 ¬ O V O sSet ndx O -1 =
15 14 fveq2d ¬ O V O sSet ndx O -1 =
16 8 12 15 3eqtr4a ¬ O V O -1 = O sSet ndx O -1
17 7 16 pm2.61i O -1 = O sSet ndx O -1
18 2 cnveqi ˙ -1 = O -1
19 eqid O = O
20 1 19 oduval D = O sSet ndx O -1
21 20 fveq2i D = O sSet ndx O -1
22 17 18 21 3eqtr4i ˙ -1 = D