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	$$⊢\underset{\dot{}}{\le }={\le }_O$$
Assertion	oduleval	$$⊢{\underset{\dot{}}{\le }}^{-1}={\le }_D$$

Proof

Step	Hyp	Ref	Expression
1		oduval.d	$$⊢D=\mathrm{ODual}\left(O\right)$$
2		oduval.l	$$⊢\underset{\dot{}}{\le }={\le }_O$$
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	$$⊢\neg O\in \mathrm{V}\to {\le }_O=\varnothing$$
10	9	cnveqd	$$⊢\neg O\in \mathrm{V}\to {{\le }_O}^{-1}={\varnothing }^{-1}$$
11		cnv0	$$⊢{\varnothing }^{-1}=\varnothing$$
12	10 11	eqtrdi	$$⊢\neg O\in \mathrm{V}\to {{\le }_O}^{-1}=\varnothing$$
13		reldmsets	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{sSet}$$
14	13	ovprc1	$$⊢\neg O\in \mathrm{V}\to O\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_O}^{-1}⟩=\varnothing$$
15	14	fveq2d	$$⊢\neg O\in \mathrm{V}\to {\le }_{\left(O\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_O}^{-1}⟩\right)}={\le }_{\varnothing }$$
16	8 12 15	3eqtr4a	$$⊢\neg 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	$$⊢{\underset{\dot{}}{\le }}^{-1}={{\le }_O}^{-1}$$
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	$$⊢{\underset{\dot{}}{\le }}^{-1}={\le }_D$$