# 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}=\mathrm{ODual}\left({O}\right)$
oduval.l
Assertion oduleval

### Proof

Step Hyp Ref Expression
1 oduval.d ${⊢}{D}=\mathrm{ODual}\left({O}\right)$
2 oduval.l
3 fvex ${⊢}{\le }_{{O}}\in \mathrm{V}$
4 3 cnvex ${⊢}{{\le }_{{O}}}^{-1}\in \mathrm{V}$
5 pleid ${⊢}\mathrm{le}=\mathrm{Slot}{\le }_{\mathrm{ndx}}$
6 5 setsid ${⊢}\left({O}\in \mathrm{V}\wedge {{\le }_{{O}}}^{-1}\in \mathrm{V}\right)\to {{\le }_{{O}}}^{-1}={\le }_{\left({O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩\right)}$
7 4 6 mpan2 ${⊢}{O}\in \mathrm{V}\to {{\le }_{{O}}}^{-1}={\le }_{\left({O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩\right)}$
8 5 str0 ${⊢}\varnothing ={\le }_{\varnothing }$
9 fvprc ${⊢}¬{O}\in \mathrm{V}\to {\le }_{{O}}=\varnothing$
10 9 cnveqd ${⊢}¬{O}\in \mathrm{V}\to {{\le }_{{O}}}^{-1}={\varnothing }^{-1}$
11 cnv0 ${⊢}{\varnothing }^{-1}=\varnothing$
12 10 11 syl6eq ${⊢}¬{O}\in \mathrm{V}\to {{\le }_{{O}}}^{-1}=\varnothing$
13 reldmsets ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{sSet}$
14 13 ovprc1 ${⊢}¬{O}\in \mathrm{V}\to {O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩=\varnothing$
15 14 fveq2d ${⊢}¬{O}\in \mathrm{V}\to {\le }_{\left({O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩\right)}={\le }_{\varnothing }$
16 8 12 15 3eqtr4a ${⊢}¬{O}\in \mathrm{V}\to {{\le }_{{O}}}^{-1}={\le }_{\left({O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩\right)}$
17 7 16 pm2.61i ${⊢}{{\le }_{{O}}}^{-1}={\le }_{\left({O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩\right)}$
18 2 cnveqi
19 eqid ${⊢}{\le }_{{O}}={\le }_{{O}}$
20 1 19 oduval ${⊢}{D}={O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩$
21 20 fveq2i ${⊢}{\le }_{{D}}={\le }_{\left({O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩\right)}$
22 17 18 21 3eqtr4i