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

Proof

Step Hyp Ref Expression
1 oduval.d ${⊢}{D}=\mathrm{ODual}\left({O}\right)$
2 oduval.l
3 id ${⊢}{a}={O}\to {a}={O}$
4 fveq2 ${⊢}{a}={O}\to {\le }_{{a}}={\le }_{{O}}$
5 4 cnveqd ${⊢}{a}={O}\to {{\le }_{{a}}}^{-1}={{\le }_{{O}}}^{-1}$
6 5 opeq2d ${⊢}{a}={O}\to ⟨{\le }_{\mathrm{ndx}},{{\le }_{{a}}}^{-1}⟩=⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩$
7 3 6 oveq12d ${⊢}{a}={O}\to {a}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{a}}}^{-1}⟩={O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩$
8 df-odu ${⊢}\mathrm{ODual}=\left({a}\in \mathrm{V}⟼{a}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{a}}}^{-1}⟩\right)$
9 ovex ${⊢}{O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩\in \mathrm{V}$
10 7 8 9 fvmpt ${⊢}{O}\in \mathrm{V}\to \mathrm{ODual}\left({O}\right)={O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩$
11 fvprc ${⊢}¬{O}\in \mathrm{V}\to \mathrm{ODual}\left({O}\right)=\varnothing$
12 reldmsets ${⊢}\mathrm{Rel}\mathrm{dom}\mathrm{sSet}$
13 12 ovprc1 ${⊢}¬{O}\in \mathrm{V}\to {O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩=\varnothing$
14 11 13 eqtr4d ${⊢}¬{O}\in \mathrm{V}\to \mathrm{ODual}\left({O}\right)={O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩$
15 10 14 pm2.61i ${⊢}\mathrm{ODual}\left({O}\right)={O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩$
16 2 cnveqi
17 16 opeq2i
18 17 oveq2i
19 15 1 18 3eqtr4i