Theorem ordtprsval

Description: Value of the order topology for a proset. (Contributed by Thierry Arnoux, 11-Sep-2015)

	Ref	Expression
Hypotheses	ordtNEW.b	$$⊢B={\mathrm{Base}}_K$$
	ordtNEW.l	$$⊢\underset{\dot{}}{\le }={\le }_K\cap \left(B\times B\right)$$
	ordtposval.e	$$⊢E=\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)$$
	ordtposval.f	$$⊢F=\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)$$
Assertion	ordtprsval	$$⊢K\in \mathrm{Proset}\to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(E\cup F\right)\right)\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		ordtposval.e	$$⊢E=\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)$$
4		ordtposval.f	$$⊢F=\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)$$
5		fvex	$$⊢{\le }_K\in \mathrm{V}$$
6	5	inex1	$$⊢{\le }_K\cap \left(B\times B\right)\in \mathrm{V}$$
7	2 6	eqeltri	$$⊢\underset{\dot{}}{\le }\in \mathrm{V}$$
8		eqid	$$⊢\mathrm{dom}\underset{\dot{}}{\le }=\mathrm{dom}\underset{\dot{}}{\le }$$
9		eqid	$$⊢\mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg y\underset{\dot{}}{\le }x\right\}\right)=\mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg y\underset{\dot{}}{\le }x\right\}\right)$$
10		eqid	$$⊢\mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg x\underset{\dot{}}{\le }y\right\}\right)=\mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg x\underset{\dot{}}{\le }y\right\}\right)$$
11	8 9 10	ordtval	$$⊢\underset{\dot{}}{\le }\in \mathrm{V}\to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{\mathrm{dom}\underset{\dot{}}{\le }\right\}\cup \left(\mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg y\underset{\dot{}}{\le }x\right\}\right)\cup \mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg x\underset{\dot{}}{\le }y\right\}\right)\right)\right)\right)$$
12	7 11	ax-mp	$$⊢\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{\mathrm{dom}\underset{\dot{}}{\le }\right\}\cup \left(\mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg y\underset{\dot{}}{\le }x\right\}\right)\cup \mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg x\underset{\dot{}}{\le }y\right\}\right)\right)\right)\right)$$
13	1 2	prsdm	$$⊢K\in \mathrm{Proset}\to \mathrm{dom}\underset{\dot{}}{\le }=B$$
14	13	sneqd	$$⊢K\in \mathrm{Proset}\to \left\{\mathrm{dom}\underset{\dot{}}{\le }\right\}=\left\{B\right\}$$
15	13	rabeqdv	$$⊢K\in \mathrm{Proset}\to \left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg y\underset{\dot{}}{\le }x\right\}=\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}$$
16	13 15	mpteq12dv	$$⊢K\in \mathrm{Proset}\to \left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg y\underset{\dot{}}{\le }x\right\}\right)=\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)$$
17	16	rneqd	$$⊢K\in \mathrm{Proset}\to \mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\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)$$
18	17 3	syl6eqr	$$⊢K\in \mathrm{Proset}\to \mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg y\underset{\dot{}}{\le }x\right\}\right)=E$$
19	13	rabeqdv	$$⊢K\in \mathrm{Proset}\to \left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg x\underset{\dot{}}{\le }y\right\}=\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}$$
20	13 19	mpteq12dv	$$⊢K\in \mathrm{Proset}\to \left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg x\underset{\dot{}}{\le }y\right\}\right)=\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)$$
21	20	rneqd	$$⊢K\in \mathrm{Proset}\to \mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\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)$$
22	21 4	syl6eqr	$$⊢K\in \mathrm{Proset}\to \mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg x\underset{\dot{}}{\le }y\right\}\right)=F$$
23	18 22	uneq12d	$$⊢K\in \mathrm{Proset}\to \mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg y\underset{\dot{}}{\le }x\right\}\right)\cup \mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg x\underset{\dot{}}{\le }y\right\}\right)=E\cup F$$
24	14 23	uneq12d	$$⊢K\in \mathrm{Proset}\to \left\{\mathrm{dom}\underset{\dot{}}{\le }\right\}\cup \left(\mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg y\underset{\dot{}}{\le }x\right\}\right)\cup \mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg x\underset{\dot{}}{\le }y\right\}\right)\right)=\left\{B\right\}\cup \left(E\cup F\right)$$
25	24	fveq2d	$$⊢K\in \mathrm{Proset}\to \mathrm{fi}\left(\left\{\mathrm{dom}\underset{\dot{}}{\le }\right\}\cup \left(\mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg y\underset{\dot{}}{\le }x\right\}\right)\cup \mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg x\underset{\dot{}}{\le }y\right\}\right)\right)\right)=\mathrm{fi}\left(\left\{B\right\}\cup \left(E\cup F\right)\right)$$
26	25	fveq2d	$$⊢K\in \mathrm{Proset}\to \mathrm{topGen}\left(\mathrm{fi}\left(\left\{\mathrm{dom}\underset{\dot{}}{\le }\right\}\cup \left(\mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg y\underset{\dot{}}{\le }x\right\}\right)\cup \mathrm{ran}\left(x\in \mathrm{dom}\underset{\dot{}}{\le }⟼\left\{y\in \mathrm{dom}\underset{\dot{}}{\le }|\neg x\underset{\dot{}}{\le }y\right\}\right)\right)\right)\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(E\cup F\right)\right)\right)$$
27	12 26	syl5eq	$$⊢K\in \mathrm{Proset}\to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(E\cup F\right)\right)\right)$$