Theorem ordtprsuni

Description: Value of the order topology. (Contributed 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)$$
	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	ordtprsuni	$$⊢K\in \mathrm{Proset}\to B=\bigcup \left(\left\{B\right\}\cup \left(E\cup F\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	1 2	prsdm	$$⊢K\in \mathrm{Proset}\to \mathrm{dom}\underset{\dot{}}{\le }=B$$
6	5	sneqd	$$⊢K\in \mathrm{Proset}\to \left\{\mathrm{dom}\underset{\dot{}}{\le }\right\}=\left\{B\right\}$$
7		biidd	$$⊢K\in \mathrm{Proset}\to \left(\neg y\underset{\dot{}}{\le }x\leftrightarrow \neg y\underset{\dot{}}{\le }x\right)$$
8	5 7	rabeqbidv	$$⊢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\}$$
9	5 8	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)$$
10	9	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)$$
11		biidd	$$⊢K\in \mathrm{Proset}\to \left(\neg x\underset{\dot{}}{\le }y\leftrightarrow \neg x\underset{\dot{}}{\le }y\right)$$
12	5 11	rabeqbidv	$$⊢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\}$$
13	5 12	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)$$
14	13	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)$$
15	10 14	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)=\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)$$
16	6 15	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(\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)$$
17	16	unieqd	$$⊢K\in \mathrm{Proset}\to \bigcup \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)=\bigcup \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)$$
18		fvex	$$⊢{\le }_K\in \mathrm{V}$$
19	18	inex1	$$⊢{\le }_K\cap \left(B\times B\right)\in \mathrm{V}$$
20	2 19	eqeltri	$$⊢\underset{\dot{}}{\le }\in \mathrm{V}$$
21		eqid	$$⊢\mathrm{dom}\underset{\dot{}}{\le }=\mathrm{dom}\underset{\dot{}}{\le }$$
22		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)$$
23		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)$$
24	21 22 23	ordtuni	$$⊢\underset{\dot{}}{\le }\in \mathrm{V}\to \mathrm{dom}\underset{\dot{}}{\le }=\bigcup \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)$$
25	20 24	ax-mp	$$⊢\mathrm{dom}\underset{\dot{}}{\le }=\bigcup \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)$$
26	5 25	eqtr3di	$$⊢K\in \mathrm{Proset}\to B=\bigcup \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)$$
27	3 4	uneq12i	$$⊢E\cup F=\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)$$
28	27	a1i	$$⊢K\in \mathrm{Proset}\to E\cup F=\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)$$
29	28	uneq2d	$$⊢K\in \mathrm{Proset}\to \left\{B\right\}\cup \left(E\cup F\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)$$
30	29	unieqd	$$⊢K\in \mathrm{Proset}\to \bigcup \left(\left\{B\right\}\cup \left(E\cup F\right)\right)=\bigcup \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)$$
31	17 26 30	3eqtr4d	$$⊢K\in \mathrm{Proset}\to B=\bigcup \left(\left\{B\right\}\cup \left(E\cup F\right)\right)$$