Theorem ordtrest2NEW

Description: An interval-closed set A in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in RR , but in other sets like QQ there are interval-closed sets like ( _pi , +oo ) i^i QQ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015) (Revised by Thierry Arnoux, 11-Sep-2018)

	Ref	Expression
Hypotheses	ordtNEW.b	$$⊢B={\mathrm{Base}}_K$$
	ordtNEW.l	$$⊢\underset{\dot{}}{\le }={\le }_K\cap \left(B\times B\right)$$
	ordtrest2NEW.2	$$⊢\phi \to K\in \mathrm{Toset}$$
	ordtrest2NEW.3	$$⊢\phi \to A\subseteq B$$
	ordtrest2NEW.4	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in A\right)\right)\to \left\{z\in B|\left(x\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }y\right)\right\}\subseteq A$$
Assertion	ordtrest2NEW	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)=\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right){\upharpoonright }_{𝑡}A$$

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		ordtrest2NEW.2	$$⊢\phi \to K\in \mathrm{Toset}$$
4		ordtrest2NEW.3	$$⊢\phi \to A\subseteq B$$
5		ordtrest2NEW.4	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in A\right)\right)\to \left\{z\in B|\left(x\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }y\right)\right\}\subseteq A$$
6		tospos	$$⊢K\in \mathrm{Toset}\to K\in \mathrm{Poset}$$
7		posprs	$$⊢K\in \mathrm{Poset}\to K\in \mathrm{Proset}$$
8	3 6 7	3syl	$$⊢\phi \to K\in \mathrm{Proset}$$
9	1 2	ordtrestNEW	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\subseteq \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right){\upharpoonright }_{𝑡}A$$
10	8 4 9	syl2anc	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\subseteq \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right){\upharpoonright }_{𝑡}A$$
11		eqid	$$⊢\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)=\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)$$
12		eqid	$$⊢\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)=\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)$$
13	1 2 11 12	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(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)\right)$$
14	8 13	syl	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)\right)$$
15	14	oveq1d	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right){\upharpoonright }_{𝑡}A=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)\right){\upharpoonright }_{𝑡}A$$
16		fibas	$$⊢\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)\in \mathrm{TopBases}$$
17	1	fvexi	$$⊢B\in \mathrm{V}$$
18	17	a1i	$$⊢\phi \to B\in \mathrm{V}$$
19	18 4	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
20		tgrest	$$⊢\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)\in \mathrm{TopBases}\wedge A\in \mathrm{V}\right)\to \mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right){\upharpoonright }_{𝑡}A\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)\right){\upharpoonright }_{𝑡}A$$
21	16 19 20	sylancr	$$⊢\phi \to \mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right){\upharpoonright }_{𝑡}A\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)\right){\upharpoonright }_{𝑡}A$$
22	15 21	eqtr4d	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right){\upharpoonright }_{𝑡}A=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right){\upharpoonright }_{𝑡}A\right)$$
23		firest	$$⊢\mathrm{fi}\left(\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right){\upharpoonright }_{𝑡}A\right)=\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right){\upharpoonright }_{𝑡}A$$
24	23	fveq2i	$$⊢\mathrm{topGen}\left(\mathrm{fi}\left(\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right){\upharpoonright }_{𝑡}A\right)\right)=\mathrm{topGen}\left(\mathrm{fi}\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right){\upharpoonright }_{𝑡}A\right)$$
25	22 24	eqtr4di	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right){\upharpoonright }_{𝑡}A=\mathrm{topGen}\left(\mathrm{fi}\left(\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right){\upharpoonright }_{𝑡}A\right)\right)$$
26		fvex	$$⊢{\le }_K\in \mathrm{V}$$
27	26	inex1	$$⊢{\le }_K\cap \left(B\times B\right)\in \mathrm{V}$$
28	2 27	eqeltri	$$⊢\underset{\dot{}}{\le }\in \mathrm{V}$$
29	28	inex1	$$⊢\underset{\dot{}}{\le }\cap \left(A\times A\right)\in \mathrm{V}$$
30		ordttop	$$⊢\underset{\dot{}}{\le }\cap \left(A\times A\right)\in \mathrm{V}\to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\in \mathrm{Top}$$
31	29 30	mp1i	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\in \mathrm{Top}$$
32	1 2 11 12	ordtprsuni	$$⊢K\in \mathrm{Proset}\to B=\bigcup \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)$$
33	8 32	syl	$$⊢\phi \to B=\bigcup \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)$$
34	33 18	eqeltrrd	$$⊢\phi \to \bigcup \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)\in \mathrm{V}$$
35		uniexb	$$⊢\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\in \mathrm{V}\leftrightarrow \bigcup \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)\in \mathrm{V}$$
36	34 35	sylibr	$$⊢\phi \to \left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\in \mathrm{V}$$
37		restval	$$⊢\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\in \mathrm{V}\wedge A\in \mathrm{V}\right)\to \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right){\upharpoonright }_{𝑡}A=\mathrm{ran}\left(v\in \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)⟼v\cap A\right)$$
38	36 19 37	syl2anc	$$⊢\phi \to \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right){\upharpoonright }_{𝑡}A=\mathrm{ran}\left(v\in \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)⟼v\cap A\right)$$
39		sseqin2	$$⊢A\subseteq B\leftrightarrow B\cap A=A$$
40	4 39	sylib	$$⊢\phi \to B\cap A=A$$
41		eqid	$$⊢\mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)=\mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
42	41	ordttopon	$$⊢\underset{\dot{}}{\le }\cap \left(A\times A\right)\in \mathrm{V}\to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\in \mathrm{TopOn}\left(\mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
43	29 42	mp1i	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\in \mathrm{TopOn}\left(\mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
44	1 2	prsssdm	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to \mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)=A$$
45	8 4 44	syl2anc	$$⊢\phi \to \mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)=A$$
46	45	fveq2d	$$⊢\phi \to \mathrm{TopOn}\left(\mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)=\mathrm{TopOn}\left(A\right)$$
47	43 46	eleqtrd	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\in \mathrm{TopOn}\left(A\right)$$
48		toponmax	$$⊢\mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\in \mathrm{TopOn}\left(A\right)\to A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
49	47 48	syl	$$⊢\phi \to A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
50	40 49	eqeltrd	$$⊢\phi \to B\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
51		elsni	$$⊢v\in \left\{B\right\}\to v=B$$
52	51	ineq1d	$$⊢v\in \left\{B\right\}\to v\cap A=B\cap A$$
53	52	eleq1d	$$⊢v\in \left\{B\right\}\to \left(v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\leftrightarrow B\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
54	50 53	syl5ibrcom	$$⊢\phi \to \left(v\in \left\{B\right\}\to v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
55	54	ralrimiv	$$⊢\phi \to \forall v\in \left\{B\right\}v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
56	1 2 3 4 5	ordtrest2NEWlem	$$⊢\phi \to \forall v\in \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
57		eqid	$$⊢\mathrm{ODual}\left(K\right)=\mathrm{ODual}\left(K\right)$$
58	57 1	odubas	$$⊢B={\mathrm{Base}}_{\mathrm{ODual}\left(K\right)}$$
59	2	cnveqi	$$⊢{\underset{\dot{}}{\le }}^{-1}={\left({\le }_K\cap \left(B\times B\right)\right)}^{-1}$$
60		cnvin	$$⊢{\left({\le }_K\cap \left(B\times B\right)\right)}^{-1}={{\le }_K}^{-1}\cap {\left(B\times B\right)}^{-1}$$
61		cnvxp	$$⊢{\left(B\times B\right)}^{-1}=B\times B$$
62	61	ineq2i	$$⊢{{\le }_K}^{-1}\cap {\left(B\times B\right)}^{-1}={{\le }_K}^{-1}\cap \left(B\times B\right)$$
63		eqid	$$⊢{\le }_K={\le }_K$$
64	57 63	oduleval	$$⊢{{\le }_K}^{-1}={\le }_{\mathrm{ODual}\left(K\right)}$$
65	64	ineq1i	$$⊢{{\le }_K}^{-1}\cap \left(B\times B\right)={\le }_{\mathrm{ODual}\left(K\right)}\cap \left(B\times B\right)$$
66	60 62 65	3eqtri	$$⊢{\left({\le }_K\cap \left(B\times B\right)\right)}^{-1}={\le }_{\mathrm{ODual}\left(K\right)}\cap \left(B\times B\right)$$
67	59 66	eqtri	$$⊢{\underset{\dot{}}{\le }}^{-1}={\le }_{\mathrm{ODual}\left(K\right)}\cap \left(B\times B\right)$$
68	57	odutos	$$⊢K\in \mathrm{Toset}\to \mathrm{ODual}\left(K\right)\in \mathrm{Toset}$$
69	3 68	syl	$$⊢\phi \to \mathrm{ODual}\left(K\right)\in \mathrm{Toset}$$
70		vex	$$⊢y\in \mathrm{V}$$
71		vex	$$⊢z\in \mathrm{V}$$
72	70 71	brcnv	$$⊢y{\underset{\dot{}}{\le }}^{-1}z\leftrightarrow z\underset{\dot{}}{\le }y$$
73		vex	$$⊢x\in \mathrm{V}$$
74	71 73	brcnv	$$⊢z{\underset{\dot{}}{\le }}^{-1}x\leftrightarrow x\underset{\dot{}}{\le }z$$
75	72 74	anbi12ci	$$⊢\left(y{\underset{\dot{}}{\le }}^{-1}z\wedge z{\underset{\dot{}}{\le }}^{-1}x\right)\leftrightarrow \left(x\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }y\right)$$
76	75	rabbii	$$⊢\left\{z\in B|\left(y{\underset{\dot{}}{\le }}^{-1}z\wedge z{\underset{\dot{}}{\le }}^{-1}x\right)\right\}=\left\{z\in B|\left(x\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }y\right)\right\}$$
77	76 5	eqsstrid	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in A\right)\right)\to \left\{z\in B|\left(y{\underset{\dot{}}{\le }}^{-1}z\wedge z{\underset{\dot{}}{\le }}^{-1}x\right)\right\}\subseteq A$$
78	77	ancom2s	$$⊢\left(\phi \wedge \left(y\in A\wedge x\in A\right)\right)\to \left\{z\in B|\left(y{\underset{\dot{}}{\le }}^{-1}z\wedge z{\underset{\dot{}}{\le }}^{-1}x\right)\right\}\subseteq A$$
79	58 67 69 4 78	ordtrest2NEWlem	$$⊢\phi \to \forall v\in \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w{\underset{\dot{}}{\le }}^{-1}z\right\}\right)v\cap A\in \mathrm{ordTop}\left({\underset{\dot{}}{\le }}^{-1}\cap \left(A\times A\right)\right)$$
80		vex	$$⊢w\in \mathrm{V}$$
81	80 71	brcnv	$$⊢w{\underset{\dot{}}{\le }}^{-1}z\leftrightarrow z\underset{\dot{}}{\le }w$$
82	81	bicomi	$$⊢z\underset{\dot{}}{\le }w\leftrightarrow w{\underset{\dot{}}{\le }}^{-1}z$$
83	82	a1i	$$⊢\phi \to \left(z\underset{\dot{}}{\le }w\leftrightarrow w{\underset{\dot{}}{\le }}^{-1}z\right)$$
84	83	notbid	$$⊢\phi \to \left(\neg z\underset{\dot{}}{\le }w\leftrightarrow \neg w{\underset{\dot{}}{\le }}^{-1}z\right)$$
85	84	rabbidv	$$⊢\phi \to \left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}=\left\{w\in B|\neg w{\underset{\dot{}}{\le }}^{-1}z\right\}$$
86	85	mpteq2dv	$$⊢\phi \to \left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)=\left(z\in B⟼\left\{w\in B|\neg w{\underset{\dot{}}{\le }}^{-1}z\right\}\right)$$
87	86	rneqd	$$⊢\phi \to \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)=\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w{\underset{\dot{}}{\le }}^{-1}z\right\}\right)$$
88	1	ressprs	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to K{\upharpoonright }_{𝑠}A\in \mathrm{Proset}$$
89	8 4 88	syl2anc	$$⊢\phi \to K{\upharpoonright }_{𝑠}A\in \mathrm{Proset}$$
90		eqid	$$⊢{\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}={\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
91		eqid	$$⊢{\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)={\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)$$
92	90 91	ordtcnvNEW	$$⊢K{\upharpoonright }_{𝑠}A\in \mathrm{Proset}\to \mathrm{ordTop}\left({\left({\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)\right)}^{-1}\right)=\mathrm{ordTop}\left({\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)\right)$$
93	89 92	syl	$$⊢\phi \to \mathrm{ordTop}\left({\left({\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)\right)}^{-1}\right)=\mathrm{ordTop}\left({\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)\right)$$
94	1 2	prsss	$$⊢\left(K\in \mathrm{Proset}\wedge A\subseteq B\right)\to \underset{\dot{}}{\le }\cap \left(A\times A\right)={\le }_K\cap \left(A\times A\right)$$
95	8 4 94	syl2anc	$$⊢\phi \to \underset{\dot{}}{\le }\cap \left(A\times A\right)={\le }_K\cap \left(A\times A\right)$$
96		eqid	$$⊢K{\upharpoonright }_{𝑠}A=K{\upharpoonright }_{𝑠}A$$
97	96 63	ressle	$$⊢A\in \mathrm{V}\to {\le }_K={\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
98	19 97	syl	$$⊢\phi \to {\le }_K={\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
99	96 1	ressbas2	$$⊢A\subseteq B\to A={\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
100	4 99	syl	$$⊢\phi \to A={\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
101	100	sqxpeqd	$$⊢\phi \to A\times A={\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}$$
102	98 101	ineq12d	$$⊢\phi \to {\le }_K\cap \left(A\times A\right)={\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)$$
103	95 102	eqtrd	$$⊢\phi \to \underset{\dot{}}{\le }\cap \left(A\times A\right)={\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)$$
104	103	cnveqd	$$⊢\phi \to {\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)}^{-1}={\left({\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)\right)}^{-1}$$
105	104	fveq2d	$$⊢\phi \to \mathrm{ordTop}\left({\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)}^{-1}\right)=\mathrm{ordTop}\left({\left({\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)\right)}^{-1}\right)$$
106	103	fveq2d	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)=\mathrm{ordTop}\left({\le }_{\left(K{\upharpoonright }_{𝑠}A\right)}\cap \left({\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\times {\mathrm{Base}}_{\left(K{\upharpoonright }_{𝑠}A\right)}\right)\right)$$
107	93 105 106	3eqtr4d	$$⊢\phi \to \mathrm{ordTop}\left({\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)}^{-1}\right)=\mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
108		cnvin	$$⊢{\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)}^{-1}={\underset{\dot{}}{\le }}^{-1}\cap {\left(A\times A\right)}^{-1}$$
109		cnvxp	$$⊢{\left(A\times A\right)}^{-1}=A\times A$$
110	109	ineq2i	$$⊢{\underset{\dot{}}{\le }}^{-1}\cap {\left(A\times A\right)}^{-1}={\underset{\dot{}}{\le }}^{-1}\cap \left(A\times A\right)$$
111	108 110	eqtri	$$⊢{\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)}^{-1}={\underset{\dot{}}{\le }}^{-1}\cap \left(A\times A\right)$$
112	111	fveq2i	$$⊢\mathrm{ordTop}\left({\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)}^{-1}\right)=\mathrm{ordTop}\left({\underset{\dot{}}{\le }}^{-1}\cap \left(A\times A\right)\right)$$
113	107 112	eqtr3di	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)=\mathrm{ordTop}\left({\underset{\dot{}}{\le }}^{-1}\cap \left(A\times A\right)\right)$$
114	113	eleq2d	$$⊢\phi \to \left(v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\leftrightarrow v\cap A\in \mathrm{ordTop}\left({\underset{\dot{}}{\le }}^{-1}\cap \left(A\times A\right)\right)\right)$$
115	87 114	raleqbidv	$$⊢\phi \to \left(\forall v\in \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\leftrightarrow \forall v\in \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w{\underset{\dot{}}{\le }}^{-1}z\right\}\right)v\cap A\in \mathrm{ordTop}\left({\underset{\dot{}}{\le }}^{-1}\cap \left(A\times A\right)\right)\right)$$
116	79 115	mpbird	$$⊢\phi \to \forall v\in \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
117		ralunb	$$⊢\forall v\in \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\leftrightarrow \left(\forall v\in \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\wedge \forall v\in \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
118	56 116 117	sylanbrc	$$⊢\phi \to \forall v\in \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
119		ralunb	$$⊢\forall v\in \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\leftrightarrow \left(\forall v\in \left\{B\right\}v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\wedge \forall v\in \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
120	55 118 119	sylanbrc	$$⊢\phi \to \forall v\in \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
121		eqid	$$⊢\left(v\in \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)⟼v\cap A\right)=\left(v\in \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)⟼v\cap A\right)$$
122	121	fmpt	$$⊢\forall v\in \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\leftrightarrow \left(v\in \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)⟼v\cap A\right):\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)⟶\mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
123	120 122	sylib	$$⊢\phi \to \left(v\in \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)⟼v\cap A\right):\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)⟶\mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
124	123	frnd	$$⊢\phi \to \mathrm{ran}\left(v\in \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right)⟼v\cap A\right)\subseteq \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
125	38 124	eqsstrd	$$⊢\phi \to \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right){\upharpoonright }_{𝑡}A\subseteq \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
126		tgfiss	$$⊢\left(\mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\in \mathrm{Top}\wedge \left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right){\upharpoonright }_{𝑡}A\subseteq \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)\to \mathrm{topGen}\left(\mathrm{fi}\left(\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right){\upharpoonright }_{𝑡}A\right)\right)\subseteq \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
127	31 125 126	syl2anc	$$⊢\phi \to \mathrm{topGen}\left(\mathrm{fi}\left(\left(\left\{B\right\}\cup \left(\mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)\cup \mathrm{ran}\left(z\in B⟼\left\{w\in B|\neg z\underset{\dot{}}{\le }w\right\}\right)\right)\right){\upharpoonright }_{𝑡}A\right)\right)\subseteq \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
128	25 127	eqsstrd	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right){\upharpoonright }_{𝑡}A\subseteq \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
129	10 128	eqssd	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)=\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right){\upharpoonright }_{𝑡}A$$