Theorem ordtrest2NEWlem

Description: Lemma for ordtrest2NEW . (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	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)$$

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		inrab2	$$⊢\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\cap A=\left\{w\in \left(B\cap A\right)|\neg w\underset{\dot{}}{\le }z\right\}$$
7		sseqin2	$$⊢A\subseteq B\leftrightarrow B\cap A=A$$
8	4 7	sylib	$$⊢\phi \to B\cap A=A$$
9	8	adantr	$$⊢\left(\phi \wedge z\in B\right)\to B\cap A=A$$
10		rabeq	$$⊢B\cap A=A\to \left\{w\in \left(B\cap A\right)|\neg w\underset{\dot{}}{\le }z\right\}=\left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}$$
11	9 10	syl	$$⊢\left(\phi \wedge z\in B\right)\to \left\{w\in \left(B\cap A\right)|\neg w\underset{\dot{}}{\le }z\right\}=\left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}$$
12	6 11	syl5eq	$$⊢\left(\phi \wedge z\in B\right)\to \left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\cap A=\left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}$$
13		fvex	$$⊢{\le }_K\in \mathrm{V}$$
14	13	inex1	$$⊢{\le }_K\cap \left(B\times B\right)\in \mathrm{V}$$
15	2 14	eqeltri	$$⊢\underset{\dot{}}{\le }\in \mathrm{V}$$
16	15	inex1	$$⊢\underset{\dot{}}{\le }\cap \left(A\times A\right)\in \mathrm{V}$$
17	16	a1i	$$⊢\phi \to \underset{\dot{}}{\le }\cap \left(A\times A\right)\in \mathrm{V}$$
18		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)$$
19	18	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)$$
20	17 19	syl	$$⊢\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)$$
21		tospos	$$⊢K\in \mathrm{Toset}\to K\in \mathrm{Poset}$$
22		posprs	$$⊢K\in \mathrm{Poset}\to K\in \mathrm{Proset}$$
23	3 21 22	3syl	$$⊢\phi \to K\in \mathrm{Proset}$$
24	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$$
25	23 4 24	syl2anc	$$⊢\phi \to \mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)=A$$
26	25	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)$$
27	20 26	eleqtrd	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\in \mathrm{TopOn}\left(A\right)$$
28		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)$$
29	27 28	syl	$$⊢\phi \to A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
30	29	adantr	$$⊢\left(\phi \wedge z\in B\right)\to A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
31		rabid2	$$⊢A=\left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\leftrightarrow \forall w\in A\neg w\underset{\dot{}}{\le }z$$
32		eleq1	$$⊢A=\left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\to \left(A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\leftrightarrow \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
33	31 32	sylbir	$$⊢\forall w\in A\neg w\underset{\dot{}}{\le }z\to \left(A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\leftrightarrow \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
34	30 33	syl5ibcom	$$⊢\left(\phi \wedge z\in B\right)\to \left(\forall w\in A\neg w\underset{\dot{}}{\le }z\to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
35		dfrex2	$$⊢\exists w\in Aw\underset{\dot{}}{\le }z\leftrightarrow \neg \forall w\in A\neg w\underset{\dot{}}{\le }z$$
36		breq1	$$⊢w=x\to \left(w\underset{\dot{}}{\le }z\leftrightarrow x\underset{\dot{}}{\le }z\right)$$
37	36	cbvrexvw	$$⊢\exists w\in Aw\underset{\dot{}}{\le }z\leftrightarrow \exists x\in Ax\underset{\dot{}}{\le }z$$
38	35 37	bitr3i	$$⊢\neg \forall w\in A\neg w\underset{\dot{}}{\le }z\leftrightarrow \exists x\in Ax\underset{\dot{}}{\le }z$$
39		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}$$
40	17 39	syl	$$⊢\phi \to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\in \mathrm{Top}$$
41	40	adantr	$$⊢\left(\phi \wedge z\in B\right)\to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\in \mathrm{Top}$$
42		0opn	$$⊢\mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\in \mathrm{Top}\to \varnothing \in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
43	41 42	syl	$$⊢\left(\phi \wedge z\in B\right)\to \varnothing \in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
44	43	adantr	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\right)\to \varnothing \in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
45		eleq1	$$⊢\left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}=\varnothing \to \left(\left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\leftrightarrow \varnothing \in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
46	44 45	syl5ibrcom	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\right)\to \left(\left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}=\varnothing \to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
47		rabn0	$$⊢\left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\ne \varnothing \leftrightarrow \exists w\in A\neg w\underset{\dot{}}{\le }z$$
48		breq1	$$⊢w=y\to \left(w\underset{\dot{}}{\le }z\leftrightarrow y\underset{\dot{}}{\le }z\right)$$
49	48	notbid	$$⊢w=y\to \left(\neg w\underset{\dot{}}{\le }z\leftrightarrow \neg y\underset{\dot{}}{\le }z\right)$$
50	49	cbvrexvw	$$⊢\exists w\in A\neg w\underset{\dot{}}{\le }z\leftrightarrow \exists y\in A\neg y\underset{\dot{}}{\le }z$$
51	47 50	bitri	$$⊢\left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\ne \varnothing \leftrightarrow \exists y\in A\neg y\underset{\dot{}}{\le }z$$
52	3	ad3antrrr	$$⊢\left(\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\right)\wedge y\in A\right)\to K\in \mathrm{Toset}$$
53	4	ad2antrr	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\right)\to A\subseteq B$$
54	53	sselda	$$⊢\left(\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\right)\wedge y\in A\right)\to y\in B$$
55		simpllr	$$⊢\left(\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\right)\wedge y\in A\right)\to z\in B$$
56	1 2	trleile	$$⊢\left(K\in \mathrm{Toset}\wedge y\in B\wedge z\in B\right)\to \left(y\underset{\dot{}}{\le }z\vee z\underset{\dot{}}{\le }y\right)$$
57	52 54 55 56	syl3anc	$$⊢\left(\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\right)\wedge y\in A\right)\to \left(y\underset{\dot{}}{\le }z\vee z\underset{\dot{}}{\le }y\right)$$
58	57	ord	$$⊢\left(\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\right)\wedge y\in A\right)\to \left(\neg y\underset{\dot{}}{\le }z\to z\underset{\dot{}}{\le }y\right)$$
59		an4	$$⊢\left(\left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\wedge \left(y\in A\wedge z\underset{\dot{}}{\le }y\right)\right)\leftrightarrow \left(\left(x\in A\wedge y\in A\right)\wedge \left(x\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }y\right)\right)$$
60		rabss	$$⊢\left\{z\in B|\left(x\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }y\right)\right\}\subseteq A\leftrightarrow \forall z\in B\left(\left(x\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }y\right)\to z\in A\right)$$
61	5 60	sylib	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in A\right)\right)\to \forall z\in B\left(\left(x\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }y\right)\to z\in A\right)$$
62	61	r19.21bi	$$⊢\left(\left(\phi \wedge \left(x\in A\wedge y\in A\right)\right)\wedge z\in B\right)\to \left(\left(x\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }y\right)\to z\in A\right)$$
63	62	an32s	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge y\in A\right)\right)\to \left(\left(x\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }y\right)\to z\in A\right)$$
64	63	impr	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(\left(x\in A\wedge y\in A\right)\wedge \left(x\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }y\right)\right)\right)\to z\in A$$
65	59 64	sylan2b	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(\left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\wedge \left(y\in A\wedge z\underset{\dot{}}{\le }y\right)\right)\right)\to z\in A$$
66		brinxp	$$⊢\left(w\in A\wedge z\in A\right)\to \left(w\underset{\dot{}}{\le }z\leftrightarrow w\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)z\right)$$
67	66	ancoms	$$⊢\left(z\in A\wedge w\in A\right)\to \left(w\underset{\dot{}}{\le }z\leftrightarrow w\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)z\right)$$
68	67	notbid	$$⊢\left(z\in A\wedge w\in A\right)\to \left(\neg w\underset{\dot{}}{\le }z\leftrightarrow \neg w\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)z\right)$$
69	68	rabbidva	$$⊢z\in A\to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}=\left\{w\in A|\neg w\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)z\right\}$$
70	65 69	syl	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(\left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\wedge \left(y\in A\wedge z\underset{\dot{}}{\le }y\right)\right)\right)\to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}=\left\{w\in A|\neg w\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)z\right\}$$
71	25	ad2antrr	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(\left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\wedge \left(y\in A\wedge z\underset{\dot{}}{\le }y\right)\right)\right)\to \mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)=A$$
72		rabeq	$$⊢\mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)=A\to \left\{w\in \mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)|\neg w\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)z\right\}=\left\{w\in A|\neg w\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)z\right\}$$
73	71 72	syl	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(\left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\wedge \left(y\in A\wedge z\underset{\dot{}}{\le }y\right)\right)\right)\to \left\{w\in \mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)|\neg w\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)z\right\}=\left\{w\in A|\neg w\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)z\right\}$$
74	70 73	eqtr4d	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(\left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\wedge \left(y\in A\wedge z\underset{\dot{}}{\le }y\right)\right)\right)\to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}=\left\{w\in \mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)|\neg w\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)z\right\}$$
75	16	a1i	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(\left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\wedge \left(y\in A\wedge z\underset{\dot{}}{\le }y\right)\right)\right)\to \underset{\dot{}}{\le }\cap \left(A\times A\right)\in \mathrm{V}$$
76	65 71	eleqtrrd	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(\left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\wedge \left(y\in A\wedge z\underset{\dot{}}{\le }y\right)\right)\right)\to z\in \mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
77	18	ordtopn1	$$⊢\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\in \mathrm{V}\wedge z\in \mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)\to \left\{w\in \mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)|\neg w\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
78	75 76 77	syl2anc	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(\left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\wedge \left(y\in A\wedge z\underset{\dot{}}{\le }y\right)\right)\right)\to \left\{w\in \mathrm{dom}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)|\neg w\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
79	74 78	eqeltrd	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(\left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\wedge \left(y\in A\wedge z\underset{\dot{}}{\le }y\right)\right)\right)\to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
80	79	anassrs	$$⊢\left(\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\right)\wedge \left(y\in A\wedge z\underset{\dot{}}{\le }y\right)\right)\to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
81	80	expr	$$⊢\left(\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\right)\wedge y\in A\right)\to \left(z\underset{\dot{}}{\le }y\to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
82	58 81	syld	$$⊢\left(\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\right)\wedge y\in A\right)\to \left(\neg y\underset{\dot{}}{\le }z\to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
83	82	rexlimdva	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\right)\to \left(\exists y\in A\neg y\underset{\dot{}}{\le }z\to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
84	51 83	syl5bi	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\right)\to \left(\left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\ne \varnothing \to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
85	46 84	pm2.61dne	$$⊢\left(\left(\phi \wedge z\in B\right)\wedge \left(x\in A\wedge x\underset{\dot{}}{\le }z\right)\right)\to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
86	85	rexlimdvaa	$$⊢\left(\phi \wedge z\in B\right)\to \left(\exists x\in Ax\underset{\dot{}}{\le }z\to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
87	38 86	syl5bi	$$⊢\left(\phi \wedge z\in B\right)\to \left(\neg \forall w\in A\neg w\underset{\dot{}}{\le }z\to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
88	34 87	pm2.61d	$$⊢\left(\phi \wedge z\in B\right)\to \left\{w\in A|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
89	12 88	eqeltrd	$$⊢\left(\phi \wedge z\in B\right)\to \left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
90	89	ralrimiva	$$⊢\phi \to \forall z\in B\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)$$
91		fvex	$$⊢{\mathrm{Base}}_K\in \mathrm{V}$$
92	1 91	eqeltri	$$⊢B\in \mathrm{V}$$
93	92	a1i	$$⊢\phi \to B\in \mathrm{V}$$
94		rabexg	$$⊢B\in \mathrm{V}\to \left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{V}$$
95	93 94	syl	$$⊢\phi \to \left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{V}$$
96	95	ralrimivw	$$⊢\phi \to \forall z\in B\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{V}$$
97		eqid	$$⊢\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)=\left(z\in B⟼\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\right)$$
98		ineq1	$$⊢v=\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\to v\cap A=\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\cap A$$
99	98	eleq1d	$$⊢v=\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\to \left(v\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\leftrightarrow \left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
100	97 99	ralrnmptw	$$⊢\forall z\in B\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\in \mathrm{V}\to \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)\leftrightarrow \forall z\in B\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
101	96 100	syl	$$⊢\phi \to \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)\leftrightarrow \forall z\in B\left\{w\in B|\neg w\underset{\dot{}}{\le }z\right\}\cap A\in \mathrm{ordTop}\left(\underset{\dot{}}{\le }\cap \left(A\times A\right)\right)\right)$$
102	90 101	mpbird	$$⊢\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)$$