Theorem ordtcnvNEW

Description: The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015) (Revised by Thierry Arnoux, 13-Sep-2018)

	Ref	Expression
Hypotheses	ordtNEW.b	$$⊢B={\mathrm{Base}}_K$$
	ordtNEW.l	$$⊢\underset{\dot{}}{\le }={\le }_K\cap \left(B\times B\right)$$
Assertion	ordtcnvNEW	$$⊢K\in \mathrm{Proset}\to \mathrm{ordTop}\left({\underset{\dot{}}{\le }}^{-1}\right)=\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)$$

Proof

Step	Hyp	Ref	Expression
1		ordtNEW.b	$$⊢B={\mathrm{Base}}_K$$
2		ordtNEW.l	$$⊢\underset{\dot{}}{\le }={\le }_K\cap \left(B\times B\right)$$
3		vex	$$⊢y\in \mathrm{V}$$
4		vex	$$⊢x\in \mathrm{V}$$
5	3 4	brcnv	$$⊢y{\underset{\dot{}}{\le }}^{-1}x\leftrightarrow x\underset{\dot{}}{\le }y$$
6	5	a1i	$$⊢K\in \mathrm{Proset}\to \left(y{\underset{\dot{}}{\le }}^{-1}x\leftrightarrow x\underset{\dot{}}{\le }y\right)$$
7	6	notbid	$$⊢K\in \mathrm{Proset}\to \left(\neg y{\underset{\dot{}}{\le }}^{-1}x\leftrightarrow \neg x\underset{\dot{}}{\le }y\right)$$
8	7	rabbidv	$$⊢K\in \mathrm{Proset}\to \left\{y\in B|\neg y{\underset{\dot{}}{\le }}^{-1}x\right\}=\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}$$
9	8	mpteq2dv	$$⊢K\in \mathrm{Proset}\to \left(x\in B⟼\left\{y\in B|\neg y{\underset{\dot{}}{\le }}^{-1}x\right\}\right)=\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)$$
10	9	rneqd	$$⊢K\in \mathrm{Proset}\to \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y{\underset{\dot{}}{\le }}^{-1}x\right\}\right)=\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)$$
11	4 3	brcnv	$$⊢x{\underset{\dot{}}{\le }}^{-1}y\leftrightarrow y\underset{\dot{}}{\le }x$$
12	11	a1i	$$⊢K\in \mathrm{Proset}\to \left(x{\underset{\dot{}}{\le }}^{-1}y\leftrightarrow y\underset{\dot{}}{\le }x\right)$$
13	12	notbid	$$⊢K\in \mathrm{Proset}\to \left(\neg x{\underset{\dot{}}{\le }}^{-1}y\leftrightarrow \neg y\underset{\dot{}}{\le }x\right)$$
14	13	rabbidv	$$⊢K\in \mathrm{Proset}\to \left\{y\in B|\neg x{\underset{\dot{}}{\le }}^{-1}y\right\}=\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}$$
15	14	mpteq2dv	$$⊢K\in \mathrm{Proset}\to \left(x\in B⟼\left\{y\in B|\neg x{\underset{\dot{}}{\le }}^{-1}y\right\}\right)=\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)$$
16	15	rneqd	$$⊢K\in \mathrm{Proset}\to \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x{\underset{\dot{}}{\le }}^{-1}y\right\}\right)=\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)$$
17	10 16	uneq12d	$$⊢K\in \mathrm{Proset}\to \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y{\underset{\dot{}}{\le }}^{-1}x\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x{\underset{\dot{}}{\le }}^{-1}y\right\}\right)=\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)$$
18		uncom	$$⊢\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)=\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)$$
19	17 18	eqtrdi	$$⊢K\in \mathrm{Proset}\to \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y{\underset{\dot{}}{\le }}^{-1}x\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x{\underset{\dot{}}{\le }}^{-1}y\right\}\right)=\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)$$
20	19	uneq2d	$$⊢K\in \mathrm{Proset}\to \left\{B\right\}\cup \left(\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y{\underset{\dot{}}{\le }}^{-1}x\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x{\underset{\dot{}}{\le }}^{-1}y\right\}\right)\right)=\left\{B\right\}\cup \left(\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)\right)$$
21	20	fveq2d	$$⊢K\in \mathrm{Proset}\to \mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y{\underset{\dot{}}{\le }}^{-1}x\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x{\underset{\dot{}}{\le }}^{-1}y\right\}\right)\right)\right)=\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)\right)\right)$$
22	21	fveq2d	$$⊢K\in \mathrm{Proset}\to \mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y{\underset{\dot{}}{\le }}^{-1}x\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x{\underset{\dot{}}{\le }}^{-1}y\right\}\right)\right)\right)\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)\right)\right)\right)$$
23		eqid	$$⊢\mathrm{ODual}\left(K\right)=\mathrm{ODual}\left(K\right)$$
24	23	oduprs	$$⊢K\in \mathrm{Proset}\to \mathrm{ODual}\left(K\right)\in \mathrm{Proset}$$
25	23 1	odubas	$$⊢B={\mathrm{Base}}_{\mathrm{ODual}\left(K\right)}$$
26	2	cnveqi	$$⊢{\underset{\dot{}}{\le }}^{-1}={\left({\le }_K\cap \left(B\times B\right)\right)}^{-1}$$
27		cnvin	$$⊢{\left({\le }_K\cap \left(B\times B\right)\right)}^{-1}={{\le }_K}^{-1}\cap {\left(B\times B\right)}^{-1}$$
28		eqid	$$⊢{\le }_K={\le }_K$$
29	23 28	oduleval	$$⊢{{\le }_K}^{-1}={\le }_{\mathrm{ODual}\left(K\right)}$$
30		cnvxp	$$⊢{\left(B\times B\right)}^{-1}=B\times B$$
31	29 30	ineq12i	$$⊢{{\le }_K}^{-1}\cap {\left(B\times B\right)}^{-1}={\le }_{\mathrm{ODual}\left(K\right)}\cap \left(B\times B\right)$$
32	26 27 31	3eqtri	$$⊢{\underset{\dot{}}{\le }}^{-1}={\le }_{\mathrm{ODual}\left(K\right)}\cap \left(B\times B\right)$$
33		eqid	$$⊢\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y{\underset{\dot{}}{\le }}^{-1}x\right\}\right)=\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y{\underset{\dot{}}{\le }}^{-1}x\right\}\right)$$
34		eqid	$$⊢\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x{\underset{\dot{}}{\le }}^{-1}y\right\}\right)=\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x{\underset{\dot{}}{\le }}^{-1}y\right\}\right)$$
35	25 32 33 34	ordtprsval	$$⊢\mathrm{ODual}\left(K\right)\in \mathrm{Proset}\to \mathrm{ordTop}\left({\underset{\dot{}}{\le }}^{-1}\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y{\underset{\dot{}}{\le }}^{-1}x\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x{\underset{\dot{}}{\le }}^{-1}y\right\}\right)\right)\right)\right)$$
36	24 35	syl	$$⊢K\in \mathrm{Proset}\to \mathrm{ordTop}\left({\underset{\dot{}}{\le }}^{-1}\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y{\underset{\dot{}}{\le }}^{-1}x\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x{\underset{\dot{}}{\le }}^{-1}y\right\}\right)\right)\right)\right)$$
37		eqid	$$⊢\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)=\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)$$
38		eqid	$$⊢\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)=\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)$$
39	1 2 37 38	ordtprsval	$$⊢K\in \mathrm{Proset}\to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)\right)\right)\right)$$
40	22 36 39	3eqtr4d	$$⊢K\in \mathrm{Proset}\to \mathrm{ordTop}\left({\underset{\dot{}}{\le }}^{-1}\right)=\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)$$