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	$$⊢\underset{\dot{}}{\le }={\le }_O$$
Assertion	oduval	$$⊢D=O\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{\underset{\dot{}}{\le }}^{-1}⟩$$

Proof

Step	Hyp	Ref	Expression
1		oduval.d	$$⊢D=\mathrm{ODual}\left(O\right)$$
2		oduval.l	$$⊢\underset{\dot{}}{\le }={\le }_O$$
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	$$⊢\neg O\in \mathrm{V}\to \mathrm{ODual}\left(O\right)=\varnothing$$
12		reldmsets	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{sSet}$$
13	12	ovprc1	$$⊢\neg O\in \mathrm{V}\to O\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_O}^{-1}⟩=\varnothing$$
14	11 13	eqtr4d	$$⊢\neg 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	$$⊢{\underset{\dot{}}{\le }}^{-1}={{\le }_O}^{-1}$$
17	16	opeq2i	$$⊢⟨{\le }_{\mathrm{ndx}},{\underset{\dot{}}{\le }}^{-1}⟩=⟨{\le }_{\mathrm{ndx}},{{\le }_O}^{-1}⟩$$
18	17	oveq2i	$$⊢O\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{\underset{\dot{}}{\le }}^{-1}⟩=O\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_O}^{-1}⟩$$
19	15 1 18	3eqtr4i	$$⊢D=O\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{\underset{\dot{}}{\le }}^{-1}⟩$$