Theorem ordtconnlem1

Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn . See also reconnlem1 . (Contributed by Thierry Arnoux, 14-Sep-2018)

	Ref	Expression
Hypotheses	ordtconn.x	$$⊢B={\mathrm{Base}}_K$$
	ordtconn.l	$$⊢\underset{\dot{}}{\le }={\le }_K\cap \left(B\times B\right)$$
	ordtconn.j	$$⊢J=\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)$$
Assertion	ordtconnlem1	$$⊢\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\to \left(J{\upharpoonright }_{𝑡}A\in \mathrm{Conn}\to \forall x\in A\forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ordtconn.x	$$⊢B={\mathrm{Base}}_K$$
2		ordtconn.l	$$⊢\underset{\dot{}}{\le }={\le }_K\cap \left(B\times B\right)$$
3		ordtconn.j	$$⊢J=\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)$$
4		nfv	$$⊢Ⅎr\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}rA$$
6		nfra2w	$$⊢Ⅎr\forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)$$
7	5 6	nfralw	$$⊢Ⅎr\forall x\in A\forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)$$
8	7	nfn	$$⊢Ⅎr\neg \forall x\in A\forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)$$
9	4 8	nfan	$$⊢Ⅎr\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge \neg \forall x\in A\forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)\right)$$
10		tospos	$$⊢K\in \mathrm{Toset}\to K\in \mathrm{Poset}$$
11		posprs	$$⊢K\in \mathrm{Poset}\to K\in \mathrm{Proset}$$
12		fvex	$$⊢{\le }_K\in \mathrm{V}$$
13	12	inex1	$$⊢{\le }_K\cap \left(B\times B\right)\in \mathrm{V}$$
14	2 13	eqeltri	$$⊢\underset{\dot{}}{\le }\in \mathrm{V}$$
15		eqid	$$⊢\mathrm{dom}\underset{\dot{}}{\le }=\mathrm{dom}\underset{\dot{}}{\le }$$
16	15	ordttopon	$$⊢\underset{\dot{}}{\le }\in \mathrm{V}\to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)\in \mathrm{TopOn}\left(\mathrm{dom}\underset{\dot{}}{\le }\right)$$
17	14 16	ax-mp	$$⊢\mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)\in \mathrm{TopOn}\left(\mathrm{dom}\underset{\dot{}}{\le }\right)$$
18	1 2	prsdm	$$⊢K\in \mathrm{Proset}\to \mathrm{dom}\underset{\dot{}}{\le }=B$$
19	18	fveq2d	$$⊢K\in \mathrm{Proset}\to \mathrm{TopOn}\left(\mathrm{dom}\underset{\dot{}}{\le }\right)=\mathrm{TopOn}\left(B\right)$$
20	17 19	eleqtrid	$$⊢K\in \mathrm{Proset}\to \mathrm{ordTop}\left(\underset{\dot{}}{\le }\right)\in \mathrm{TopOn}\left(B\right)$$
21	3 20	eqeltrid	$$⊢K\in \mathrm{Proset}\to J\in \mathrm{TopOn}\left(B\right)$$
22	10 11 21	3syl	$$⊢K\in \mathrm{Toset}\to J\in \mathrm{TopOn}\left(B\right)$$
23	22	ad3antrrr	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to J\in \mathrm{TopOn}\left(B\right)$$
24	23	adantlr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\wedge \neg r\in A\right)\to J\in \mathrm{TopOn}\left(B\right)$$
25		simpllr	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to A\subseteq B$$
26	25	adantlr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\wedge \neg r\in A\right)\to A\subseteq B$$
27		simpll	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\to K\in \mathrm{Toset}$$
28	27 10 11	3syl	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\to K\in \mathrm{Proset}$$
29		snex	$$⊢\left\{B\right\}\in \mathrm{V}$$
30	1	fvexi	$$⊢B\in \mathrm{V}$$
31	30	mptex	$$⊢\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)\in \mathrm{V}$$
32	31	rnex	$$⊢\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)\in \mathrm{V}$$
33	30	mptex	$$⊢\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)\in \mathrm{V}$$
34	33	rnex	$$⊢\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)\in \mathrm{V}$$
35	32 34	unex	$$⊢\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)\in \mathrm{V}$$
36	29 35	unex	$$⊢\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)\in \mathrm{V}$$
37		ssfii	$$⊢\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)\in \mathrm{V}\to \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)\subseteq \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)$$
38	36 37	ax-mp	$$⊢\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)\subseteq \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)$$
39		fvex	$$⊢\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)\in \mathrm{V}$$
40		bastg	$$⊢\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)\in \mathrm{V}\to \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)\subseteq \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)$$
41	39 40	ax-mp	$$⊢\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)\subseteq \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)$$
42	38 41	sstri	$$⊢\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)\subseteq \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)$$
43		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)$$
44		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)$$
45	1 2 43 44	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)$$
46	3 45	syl5eq	$$⊢K\in \mathrm{Proset}\to J=\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)$$
47	42 46	sseqtrrid	$$⊢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 }x\right\}\right)\cup \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)\right)\subseteq J$$
48	47	unssbd	$$⊢K\in \mathrm{Proset}\to \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)\subseteq J$$
49	28 48	syl	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\to \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)\subseteq J$$
50	49	unssbd	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\to \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)\subseteq J$$
51		breq2	$$⊢z=y\to \left(r\underset{\dot{}}{\le }z\leftrightarrow r\underset{\dot{}}{\le }y\right)$$
52	51	notbid	$$⊢z=y\to \left(\neg r\underset{\dot{}}{\le }z\leftrightarrow \neg r\underset{\dot{}}{\le }y\right)$$
53	52	cbvrabv	$$⊢\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}=\left\{y\in B|\neg r\underset{\dot{}}{\le }y\right\}$$
54		breq1	$$⊢x=r\to \left(x\underset{\dot{}}{\le }y\leftrightarrow r\underset{\dot{}}{\le }y\right)$$
55	54	notbid	$$⊢x=r\to \left(\neg x\underset{\dot{}}{\le }y\leftrightarrow \neg r\underset{\dot{}}{\le }y\right)$$
56	55	rabbidv	$$⊢x=r\to \left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}=\left\{y\in B|\neg r\underset{\dot{}}{\le }y\right\}$$
57	56	rspceeqv	$$⊢\left(r\in B\wedge \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}=\left\{y\in B|\neg r\underset{\dot{}}{\le }y\right\}\right)\to \exists x\in B\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}=\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}$$
58	53 57	mpan2	$$⊢r\in B\to \exists x\in B\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}=\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}$$
59	30	rabex	$$⊢\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\in \mathrm{V}$$
60		eqid	$$⊢\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)=\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)$$
61	60	elrnmpt	$$⊢\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\in \mathrm{V}\to \left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\in \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)\leftrightarrow \exists x\in B\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}=\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)$$
62	59 61	ax-mp	$$⊢\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\in \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)\leftrightarrow \exists x\in B\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}=\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}$$
63	58 62	sylibr	$$⊢r\in B\to \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\in \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)$$
64	63	adantl	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\to \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\in \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)$$
65	50 64	sseldd	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\to \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\in J$$
66	65	ad2antrr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\wedge \neg r\in A\right)\to \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\in J$$
67	49	unssad	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\to \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)\subseteq J$$
68		breq1	$$⊢z=y\to \left(z\underset{\dot{}}{\le }r\leftrightarrow y\underset{\dot{}}{\le }r\right)$$
69	68	notbid	$$⊢z=y\to \left(\neg z\underset{\dot{}}{\le }r\leftrightarrow \neg y\underset{\dot{}}{\le }r\right)$$
70	69	cbvrabv	$$⊢\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}=\left\{y\in B|\neg y\underset{\dot{}}{\le }r\right\}$$
71		breq2	$$⊢x=r\to \left(y\underset{\dot{}}{\le }x\leftrightarrow y\underset{\dot{}}{\le }r\right)$$
72	71	notbid	$$⊢x=r\to \left(\neg y\underset{\dot{}}{\le }x\leftrightarrow \neg y\underset{\dot{}}{\le }r\right)$$
73	72	rabbidv	$$⊢x=r\to \left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}=\left\{y\in B|\neg y\underset{\dot{}}{\le }r\right\}$$
74	73	rspceeqv	$$⊢\left(r\in B\wedge \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}=\left\{y\in B|\neg y\underset{\dot{}}{\le }r\right\}\right)\to \exists x\in B\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}=\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}$$
75	70 74	mpan2	$$⊢r\in B\to \exists x\in B\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}=\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}$$
76	30	rabex	$$⊢\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\in \mathrm{V}$$
77		eqid	$$⊢\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)=\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)$$
78	77	elrnmpt	$$⊢\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\in \mathrm{V}\to \left(\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\in \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)\leftrightarrow \exists x\in B\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}=\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)$$
79	76 78	ax-mp	$$⊢\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\in \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)\leftrightarrow \exists x\in B\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}=\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}$$
80	75 79	sylibr	$$⊢r\in B\to \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\in \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)$$
81	80	adantl	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\to \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\in \mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)$$
82	67 81	sseldd	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\to \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\in J$$
83	82	ad2antrr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\wedge \neg r\in A\right)\to \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\in J$$
84		simpll	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\wedge \neg r\in A\right)\to \left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)$$
85		simpr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\wedge \neg r\in A\right)\to \neg r\in A$$
86	84 85	jca	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\wedge \neg r\in A\right)\to \left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)$$
87		simplrl	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\wedge \neg r\in A\right)\to \exists x\in A\neg r\underset{\dot{}}{\le }x$$
88		ssel	$$⊢A\subseteq B\to \left(x\in A\to x\in B\right)$$
89	88	ancrd	$$⊢A\subseteq B\to \left(x\in A\to \left(x\in B\wedge x\in A\right)\right)$$
90	89	anim1d	$$⊢A\subseteq B\to \left(\left(x\in A\wedge \neg r\underset{\dot{}}{\le }x\right)\to \left(\left(x\in B\wedge x\in A\right)\wedge \neg r\underset{\dot{}}{\le }x\right)\right)$$
91	90	impl	$$⊢\left(\left(A\subseteq B\wedge x\in A\right)\wedge \neg r\underset{\dot{}}{\le }x\right)\to \left(\left(x\in B\wedge x\in A\right)\wedge \neg r\underset{\dot{}}{\le }x\right)$$
92		elin	$$⊢x\in \left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap A\right)\leftrightarrow \left(x\in \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\wedge x\in A\right)$$
93		breq2	$$⊢z=x\to \left(r\underset{\dot{}}{\le }z\leftrightarrow r\underset{\dot{}}{\le }x\right)$$
94	93	notbid	$$⊢z=x\to \left(\neg r\underset{\dot{}}{\le }z\leftrightarrow \neg r\underset{\dot{}}{\le }x\right)$$
95	94	elrab	$$⊢x\in \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\leftrightarrow \left(x\in B\wedge \neg r\underset{\dot{}}{\le }x\right)$$
96	95	anbi1i	$$⊢\left(x\in \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\wedge x\in A\right)\leftrightarrow \left(\left(x\in B\wedge \neg r\underset{\dot{}}{\le }x\right)\wedge x\in A\right)$$
97		an32	$$⊢\left(\left(x\in B\wedge \neg r\underset{\dot{}}{\le }x\right)\wedge x\in A\right)\leftrightarrow \left(\left(x\in B\wedge x\in A\right)\wedge \neg r\underset{\dot{}}{\le }x\right)$$
98	92 96 97	3bitri	$$⊢x\in \left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap A\right)\leftrightarrow \left(\left(x\in B\wedge x\in A\right)\wedge \neg r\underset{\dot{}}{\le }x\right)$$
99	91 98	sylibr	$$⊢\left(\left(A\subseteq B\wedge x\in A\right)\wedge \neg r\underset{\dot{}}{\le }x\right)\to x\in \left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap A\right)$$
100	99	ne0d	$$⊢\left(\left(A\subseteq B\wedge x\in A\right)\wedge \neg r\underset{\dot{}}{\le }x\right)\to \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap A\ne \varnothing$$
101	25 100	sylanl1	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge x\in A\right)\wedge \neg r\underset{\dot{}}{\le }x\right)\to \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap A\ne \varnothing$$
102	101	r19.29an	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge \exists x\in A\neg r\underset{\dot{}}{\le }x\right)\to \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap A\ne \varnothing$$
103	86 87 102	syl2anc	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\wedge \neg r\in A\right)\to \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap A\ne \varnothing$$
104		simplrr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\wedge \neg r\in A\right)\to \exists y\in A\neg y\underset{\dot{}}{\le }r$$
105		ssel	$$⊢A\subseteq B\to \left(y\in A\to y\in B\right)$$
106	105	ancrd	$$⊢A\subseteq B\to \left(y\in A\to \left(y\in B\wedge y\in A\right)\right)$$
107	106	anim1d	$$⊢A\subseteq B\to \left(\left(y\in A\wedge \neg y\underset{\dot{}}{\le }r\right)\to \left(\left(y\in B\wedge y\in A\right)\wedge \neg y\underset{\dot{}}{\le }r\right)\right)$$
108	107	impl	$$⊢\left(\left(A\subseteq B\wedge y\in A\right)\wedge \neg y\underset{\dot{}}{\le }r\right)\to \left(\left(y\in B\wedge y\in A\right)\wedge \neg y\underset{\dot{}}{\le }r\right)$$
109		elin	$$⊢y\in \left(\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\cap A\right)\leftrightarrow \left(y\in \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\wedge y\in A\right)$$
110	69	elrab	$$⊢y\in \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\leftrightarrow \left(y\in B\wedge \neg y\underset{\dot{}}{\le }r\right)$$
111	110	anbi1i	$$⊢\left(y\in \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\wedge y\in A\right)\leftrightarrow \left(\left(y\in B\wedge \neg y\underset{\dot{}}{\le }r\right)\wedge y\in A\right)$$
112		an32	$$⊢\left(\left(y\in B\wedge \neg y\underset{\dot{}}{\le }r\right)\wedge y\in A\right)\leftrightarrow \left(\left(y\in B\wedge y\in A\right)\wedge \neg y\underset{\dot{}}{\le }r\right)$$
113	109 111 112	3bitri	$$⊢y\in \left(\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\cap A\right)\leftrightarrow \left(\left(y\in B\wedge y\in A\right)\wedge \neg y\underset{\dot{}}{\le }r\right)$$
114	108 113	sylibr	$$⊢\left(\left(A\subseteq B\wedge y\in A\right)\wedge \neg y\underset{\dot{}}{\le }r\right)\to y\in \left(\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\cap A\right)$$
115	114	ne0d	$$⊢\left(\left(A\subseteq B\wedge y\in A\right)\wedge \neg y\underset{\dot{}}{\le }r\right)\to \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\cap A\ne \varnothing$$
116	25 115	sylanl1	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge y\in A\right)\wedge \neg y\underset{\dot{}}{\le }r\right)\to \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\cap A\ne \varnothing$$
117	116	r19.29an	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\to \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\cap A\ne \varnothing$$
118	86 104 117	syl2anc	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\wedge \neg r\in A\right)\to \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\cap A\ne \varnothing$$
119	1 2	trleile	$$⊢\left(K\in \mathrm{Toset}\wedge r\in B\wedge z\in B\right)\to \left(r\underset{\dot{}}{\le }z\vee z\underset{\dot{}}{\le }r\right)$$
120		oran	$$⊢\left(r\underset{\dot{}}{\le }z\vee z\underset{\dot{}}{\le }r\right)\leftrightarrow \neg \left(\neg r\underset{\dot{}}{\le }z\wedge \neg z\underset{\dot{}}{\le }r\right)$$
121	119 120	sylib	$$⊢\left(K\in \mathrm{Toset}\wedge r\in B\wedge z\in B\right)\to \neg \left(\neg r\underset{\dot{}}{\le }z\wedge \neg z\underset{\dot{}}{\le }r\right)$$
122	121	3expa	$$⊢\left(\left(K\in \mathrm{Toset}\wedge r\in B\right)\wedge z\in B\right)\to \neg \left(\neg r\underset{\dot{}}{\le }z\wedge \neg z\underset{\dot{}}{\le }r\right)$$
123	122	nrexdv	$$⊢\left(K\in \mathrm{Toset}\wedge r\in B\right)\to \neg \exists z\in B\left(\neg r\underset{\dot{}}{\le }z\wedge \neg z\underset{\dot{}}{\le }r\right)$$
124		rabid	$$⊢z\in \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\leftrightarrow \left(z\in B\wedge \neg r\underset{\dot{}}{\le }z\right)$$
125		rabid	$$⊢z\in \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\leftrightarrow \left(z\in B\wedge \neg z\underset{\dot{}}{\le }r\right)$$
126	124 125	anbi12i	$$⊢\left(z\in \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\wedge z\in \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)\leftrightarrow \left(\left(z\in B\wedge \neg r\underset{\dot{}}{\le }z\right)\wedge \left(z\in B\wedge \neg z\underset{\dot{}}{\le }r\right)\right)$$
127		elin	$$⊢z\in \left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)\leftrightarrow \left(z\in \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\wedge z\in \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)$$
128		anandi	$$⊢\left(z\in B\wedge \left(\neg r\underset{\dot{}}{\le }z\wedge \neg z\underset{\dot{}}{\le }r\right)\right)\leftrightarrow \left(\left(z\in B\wedge \neg r\underset{\dot{}}{\le }z\right)\wedge \left(z\in B\wedge \neg z\underset{\dot{}}{\le }r\right)\right)$$
129	126 127 128	3bitr4i	$$⊢z\in \left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)\leftrightarrow \left(z\in B\wedge \left(\neg r\underset{\dot{}}{\le }z\wedge \neg z\underset{\dot{}}{\le }r\right)\right)$$
130	129	exbii	$$⊢\exists zz\in \left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)\leftrightarrow \exists z\left(z\in B\wedge \left(\neg r\underset{\dot{}}{\le }z\wedge \neg z\underset{\dot{}}{\le }r\right)\right)$$
131		nfrab1	$$⊢\underset{\_}{Ⅎ}z\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}$$
132		nfrab1	$$⊢\underset{\_}{Ⅎ}z\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}$$
133	131 132	nfin	$$⊢\underset{\_}{Ⅎ}z\left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)$$
134	133	n0f	$$⊢\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\ne \varnothing \leftrightarrow \exists zz\in \left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)$$
135		df-rex	$$⊢\exists z\in B\left(\neg r\underset{\dot{}}{\le }z\wedge \neg z\underset{\dot{}}{\le }r\right)\leftrightarrow \exists z\left(z\in B\wedge \left(\neg r\underset{\dot{}}{\le }z\wedge \neg z\underset{\dot{}}{\le }r\right)\right)$$
136	130 134 135	3bitr4i	$$⊢\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\ne \varnothing \leftrightarrow \exists z\in B\left(\neg r\underset{\dot{}}{\le }z\wedge \neg z\underset{\dot{}}{\le }r\right)$$
137	136	necon1bbii	$$⊢\neg \exists z\in B\left(\neg r\underset{\dot{}}{\le }z\wedge \neg z\underset{\dot{}}{\le }r\right)\leftrightarrow \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}=\varnothing$$
138	123 137	sylib	$$⊢\left(K\in \mathrm{Toset}\wedge r\in B\right)\to \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}=\varnothing$$
139	138	adantlr	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\to \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}=\varnothing$$
140	139	adantr	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}=\varnothing$$
141	140	ineq1d	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to \left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)\cap A=\varnothing \cap A$$
142		0in	$$⊢\varnothing \cap A=\varnothing$$
143	141 142	eqtrdi	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to \left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)\cap A=\varnothing$$
144	143	adantlr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\wedge \neg r\in A\right)\to \left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cap \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)\cap A=\varnothing$$
145		simplr	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to r\in B$$
146		simpr	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to \neg r\in A$$
147		vex	$$⊢r\in \mathrm{V}$$
148	147	snss	$$⊢r\in B\leftrightarrow \left\{r\right\}\subseteq B$$
149		eldif	$$⊢r\in \left(B\setminus A\right)\leftrightarrow \left(r\in B\wedge \neg r\in A\right)$$
150	147	snss	$$⊢r\in \left(B\setminus A\right)\leftrightarrow \left\{r\right\}\subseteq B\setminus A$$
151	149 150	bitr3i	$$⊢\left(r\in B\wedge \neg r\in A\right)\leftrightarrow \left\{r\right\}\subseteq B\setminus A$$
152		ssconb	$$⊢\left(\left\{r\right\}\subseteq B\wedge A\subseteq B\right)\to \left(\left\{r\right\}\subseteq B\setminus A\leftrightarrow A\subseteq B\setminus \left\{r\right\}\right)$$
153	151 152	syl5bb	$$⊢\left(\left\{r\right\}\subseteq B\wedge A\subseteq B\right)\to \left(\left(r\in B\wedge \neg r\in A\right)\leftrightarrow A\subseteq B\setminus \left\{r\right\}\right)$$
154	148 153	sylanb	$$⊢\left(r\in B\wedge A\subseteq B\right)\to \left(\left(r\in B\wedge \neg r\in A\right)\leftrightarrow A\subseteq B\setminus \left\{r\right\}\right)$$
155	154	adantl	$$⊢\left(K\in \mathrm{Toset}\wedge \left(r\in B\wedge A\subseteq B\right)\right)\to \left(\left(r\in B\wedge \neg r\in A\right)\leftrightarrow A\subseteq B\setminus \left\{r\right\}\right)$$
156	155	anass1rs	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\to \left(\left(r\in B\wedge \neg r\in A\right)\leftrightarrow A\subseteq B\setminus \left\{r\right\}\right)$$
157	156	adantr	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to \left(\left(r\in B\wedge \neg r\in A\right)\leftrightarrow A\subseteq B\setminus \left\{r\right\}\right)$$
158	145 146 157	mpbi2and	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to A\subseteq B\setminus \left\{r\right\}$$
159	10	ad3antrrr	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to K\in \mathrm{Poset}$$
160		nfv	$$⊢Ⅎz\left(K\in \mathrm{Poset}\wedge r\in B\right)$$
161	131 132	nfun	$$⊢\underset{\_}{Ⅎ}z\left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cup \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)$$
162		nfcv	$$⊢\underset{\_}{Ⅎ}z\left(B\setminus \left\{r\right\}\right)$$
163		ianor	$$⊢\neg \left(r\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }r\right)\leftrightarrow \left(\neg r\underset{\dot{}}{\le }z\vee \neg z\underset{\dot{}}{\le }r\right)$$
164	1 2	posrasymb	$$⊢\left(K\in \mathrm{Poset}\wedge r\in B\wedge z\in B\right)\to \left(\left(r\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }r\right)\leftrightarrow r=z\right)$$
165		equcom	$$⊢r=z\leftrightarrow z=r$$
166	164 165	bitrdi	$$⊢\left(K\in \mathrm{Poset}\wedge r\in B\wedge z\in B\right)\to \left(\left(r\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }r\right)\leftrightarrow z=r\right)$$
167	166	necon3bbid	$$⊢\left(K\in \mathrm{Poset}\wedge r\in B\wedge z\in B\right)\to \left(\neg \left(r\underset{\dot{}}{\le }z\wedge z\underset{\dot{}}{\le }r\right)\leftrightarrow z\ne r\right)$$
168	163 167	bitr3id	$$⊢\left(K\in \mathrm{Poset}\wedge r\in B\wedge z\in B\right)\to \left(\left(\neg r\underset{\dot{}}{\le }z\vee \neg z\underset{\dot{}}{\le }r\right)\leftrightarrow z\ne r\right)$$
169	168	3expia	$$⊢\left(K\in \mathrm{Poset}\wedge r\in B\right)\to \left(z\in B\to \left(\left(\neg r\underset{\dot{}}{\le }z\vee \neg z\underset{\dot{}}{\le }r\right)\leftrightarrow z\ne r\right)\right)$$
170	169	pm5.32d	$$⊢\left(K\in \mathrm{Poset}\wedge r\in B\right)\to \left(\left(z\in B\wedge \left(\neg r\underset{\dot{}}{\le }z\vee \neg z\underset{\dot{}}{\le }r\right)\right)\leftrightarrow \left(z\in B\wedge z\ne r\right)\right)$$
171	124 125	orbi12i	$$⊢\left(z\in \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\vee z\in \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)\leftrightarrow \left(\left(z\in B\wedge \neg r\underset{\dot{}}{\le }z\right)\vee \left(z\in B\wedge \neg z\underset{\dot{}}{\le }r\right)\right)$$
172		elun	$$⊢z\in \left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cup \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)\leftrightarrow \left(z\in \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\vee z\in \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)$$
173		andi	$$⊢\left(z\in B\wedge \left(\neg r\underset{\dot{}}{\le }z\vee \neg z\underset{\dot{}}{\le }r\right)\right)\leftrightarrow \left(\left(z\in B\wedge \neg r\underset{\dot{}}{\le }z\right)\vee \left(z\in B\wedge \neg z\underset{\dot{}}{\le }r\right)\right)$$
174	171 172 173	3bitr4ri	$$⊢\left(z\in B\wedge \left(\neg r\underset{\dot{}}{\le }z\vee \neg z\underset{\dot{}}{\le }r\right)\right)\leftrightarrow z\in \left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cup \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)$$
175		eldifsn	$$⊢z\in \left(B\setminus \left\{r\right\}\right)\leftrightarrow \left(z\in B\wedge z\ne r\right)$$
176	175	bicomi	$$⊢\left(z\in B\wedge z\ne r\right)\leftrightarrow z\in \left(B\setminus \left\{r\right\}\right)$$
177	170 174 176	3bitr3g	$$⊢\left(K\in \mathrm{Poset}\wedge r\in B\right)\to \left(z\in \left(\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cup \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\right)\leftrightarrow z\in \left(B\setminus \left\{r\right\}\right)\right)$$
178	160 161 162 177	eqrd	$$⊢\left(K\in \mathrm{Poset}\wedge r\in B\right)\to \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cup \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}=B\setminus \left\{r\right\}$$
179	159 145 178	syl2anc	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cup \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}=B\setminus \left\{r\right\}$$
180	158 179	sseqtrrd	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to A\subseteq \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cup \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}$$
181	180	adantlr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\wedge \neg r\in A\right)\to A\subseteq \left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\cup \left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}$$
182	24 26 66 83 103 118 144 181	nconnsubb	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\wedge \neg r\in A\right)\to \neg J{\upharpoonright }_{𝑡}A\in \mathrm{Conn}$$
183	182	anasss	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \left(\left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\wedge \neg r\in A\right)\right)\to \neg J{\upharpoonright }_{𝑡}A\in \mathrm{Conn}$$
184	183	adantllr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge \neg \forall x\in A\forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)\right)\wedge r\in B\right)\wedge \left(\left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\wedge \neg r\in A\right)\right)\to \neg J{\upharpoonright }_{𝑡}A\in \mathrm{Conn}$$
185		rexanali	$$⊢\exists r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \neg \forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)$$
186	185	rexbii	$$⊢\exists y\in A\exists r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \exists y\in A\neg \forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)$$
187		rexcom	$$⊢\exists y\in A\exists r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \exists r\in B\exists y\in A\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)$$
188		rexnal	$$⊢\exists y\in A\neg \forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)\leftrightarrow \neg \forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)$$
189	186 187 188	3bitr3i	$$⊢\exists r\in B\exists y\in A\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \neg \forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)$$
190	189	rexbii	$$⊢\exists x\in A\exists r\in B\exists y\in A\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \exists x\in A\neg \forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)$$
191		rexcom	$$⊢\exists x\in A\exists r\in B\exists y\in A\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \exists r\in B\exists x\in A\exists y\in A\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)$$
192		rexnal	$$⊢\exists x\in A\neg \forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)\leftrightarrow \neg \forall x\in A\forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)$$
193	190 191 192	3bitr3i	$$⊢\exists r\in B\exists x\in A\exists y\in A\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \neg \forall x\in A\forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)$$
194		r19.41v	$$⊢\exists y\in A\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \left(\exists y\in A\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)$$
195	194	rexbii	$$⊢\exists x\in A\exists y\in A\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \exists x\in A\left(\exists y\in A\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)$$
196		r19.41v	$$⊢\exists x\in A\left(\exists y\in A\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \left(\exists x\in A\exists y\in A\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)$$
197		reeanv	$$⊢\exists x\in A\exists y\in A\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\leftrightarrow \left(\exists x\in Ax\underset{\dot{}}{\le }r\wedge \exists y\in Ar\underset{\dot{}}{\le }y\right)$$
198	197	anbi1i	$$⊢\left(\exists x\in A\exists y\in A\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \left(\left(\exists x\in Ax\underset{\dot{}}{\le }r\wedge \exists y\in Ar\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)$$
199	195 196 198	3bitri	$$⊢\exists x\in A\exists y\in A\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \left(\left(\exists x\in Ax\underset{\dot{}}{\le }r\wedge \exists y\in Ar\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)$$
200	199	rexbii	$$⊢\exists r\in B\exists x\in A\exists y\in A\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \exists r\in B\left(\left(\exists x\in Ax\underset{\dot{}}{\le }r\wedge \exists y\in Ar\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)$$
201	193 200	bitr3i	$$⊢\neg \forall x\in A\forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)\leftrightarrow \exists r\in B\left(\left(\exists x\in Ax\underset{\dot{}}{\le }r\wedge \exists y\in Ar\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)$$
202	27	ad2antrr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge x\in A\right)\to K\in \mathrm{Toset}$$
203	25	sselda	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge x\in A\right)\to x\in B$$
204		simpllr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge x\in A\right)\to r\in B$$
205	1 2	trleile	$$⊢\left(K\in \mathrm{Toset}\wedge x\in B\wedge r\in B\right)\to \left(x\underset{\dot{}}{\le }r\vee r\underset{\dot{}}{\le }x\right)$$
206	202 203 204 205	syl3anc	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge x\in A\right)\to \left(x\underset{\dot{}}{\le }r\vee r\underset{\dot{}}{\le }x\right)$$
207		simpr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge x\in A\right)\to x\in A$$
208		simplr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge x\in A\right)\to \neg r\in A$$
209		nelne2	$$⊢\left(x\in A\wedge \neg r\in A\right)\to x\ne r$$
210	207 208 209	syl2anc	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge x\in A\right)\to x\ne r$$
211	159	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge x\in A\right)\to K\in \mathrm{Poset}$$
212	1 2	posrasymb	$$⊢\left(K\in \mathrm{Poset}\wedge x\in B\wedge r\in B\right)\to \left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }x\right)\leftrightarrow x=r\right)$$
213	212	necon3bbid	$$⊢\left(K\in \mathrm{Poset}\wedge x\in B\wedge r\in B\right)\to \left(\neg \left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }x\right)\leftrightarrow x\ne r\right)$$
214	211 203 204 213	syl3anc	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge x\in A\right)\to \left(\neg \left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }x\right)\leftrightarrow x\ne r\right)$$
215	210 214	mpbird	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge x\in A\right)\to \neg \left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }x\right)$$
216	206 215	jca	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge x\in A\right)\to \left(\left(x\underset{\dot{}}{\le }r\vee r\underset{\dot{}}{\le }x\right)\wedge \neg \left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }x\right)\right)$$
217		pm5.17	$$⊢\left(\left(x\underset{\dot{}}{\le }r\vee r\underset{\dot{}}{\le }x\right)\wedge \neg \left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }x\right)\right)\leftrightarrow \left(x\underset{\dot{}}{\le }r\leftrightarrow \neg r\underset{\dot{}}{\le }x\right)$$
218	216 217	sylib	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge x\in A\right)\to \left(x\underset{\dot{}}{\le }r\leftrightarrow \neg r\underset{\dot{}}{\le }x\right)$$
219	218	rexbidva	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to \left(\exists x\in Ax\underset{\dot{}}{\le }r\leftrightarrow \exists x\in A\neg r\underset{\dot{}}{\le }x\right)$$
220	27	ad2antrr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge y\in A\right)\to K\in \mathrm{Toset}$$
221		simpllr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge y\in A\right)\to r\in B$$
222	25	sselda	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge y\in A\right)\to y\in B$$
223	1 2	trleile	$$⊢\left(K\in \mathrm{Toset}\wedge r\in B\wedge y\in B\right)\to \left(r\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }r\right)$$
224	220 221 222 223	syl3anc	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge y\in A\right)\to \left(r\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }r\right)$$
225		simpr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge y\in A\right)\to y\in A$$
226		simplr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge y\in A\right)\to \neg r\in A$$
227		nelne2	$$⊢\left(y\in A\wedge \neg r\in A\right)\to y\ne r$$
228	225 226 227	syl2anc	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge y\in A\right)\to y\ne r$$
229	228	necomd	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge y\in A\right)\to r\ne y$$
230	159	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge y\in A\right)\to K\in \mathrm{Poset}$$
231	1 2	posrasymb	$$⊢\left(K\in \mathrm{Poset}\wedge r\in B\wedge y\in B\right)\to \left(\left(r\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }r\right)\leftrightarrow r=y\right)$$
232	231	necon3bbid	$$⊢\left(K\in \mathrm{Poset}\wedge r\in B\wedge y\in B\right)\to \left(\neg \left(r\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }r\right)\leftrightarrow r\ne y\right)$$
233	230 221 222 232	syl3anc	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge y\in A\right)\to \left(\neg \left(r\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }r\right)\leftrightarrow r\ne y\right)$$
234	229 233	mpbird	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge y\in A\right)\to \neg \left(r\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }r\right)$$
235	224 234	jca	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge y\in A\right)\to \left(\left(r\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }r\right)\wedge \neg \left(r\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }r\right)\right)$$
236		pm5.17	$$⊢\left(\left(r\underset{\dot{}}{\le }y\vee y\underset{\dot{}}{\le }r\right)\wedge \neg \left(r\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }r\right)\right)\leftrightarrow \left(r\underset{\dot{}}{\le }y\leftrightarrow \neg y\underset{\dot{}}{\le }r\right)$$
237	235 236	sylib	$$⊢\left(\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\wedge y\in A\right)\to \left(r\underset{\dot{}}{\le }y\leftrightarrow \neg y\underset{\dot{}}{\le }r\right)$$
238	237	rexbidva	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to \left(\exists y\in Ar\underset{\dot{}}{\le }y\leftrightarrow \exists y\in A\neg y\underset{\dot{}}{\le }r\right)$$
239	219 238	anbi12d	$$⊢\left(\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\wedge \neg r\in A\right)\to \left(\left(\exists x\in Ax\underset{\dot{}}{\le }r\wedge \exists y\in Ar\underset{\dot{}}{\le }y\right)\leftrightarrow \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)$$
240	239	ex	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\to \left(\neg r\in A\to \left(\left(\exists x\in Ax\underset{\dot{}}{\le }r\wedge \exists y\in Ar\underset{\dot{}}{\le }y\right)\leftrightarrow \left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\right)\right)$$
241	240	pm5.32rd	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge r\in B\right)\to \left(\left(\left(\exists x\in Ax\underset{\dot{}}{\le }r\wedge \exists y\in Ar\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \left(\left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\wedge \neg r\in A\right)\right)$$
242	241	rexbidva	$$⊢\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\to \left(\exists r\in B\left(\left(\exists x\in Ax\underset{\dot{}}{\le }r\wedge \exists y\in Ar\underset{\dot{}}{\le }y\right)\wedge \neg r\in A\right)\leftrightarrow \exists r\in B\left(\left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\wedge \neg r\in A\right)\right)$$
243	201 242	syl5bb	$$⊢\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\to \left(\neg \forall x\in A\forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)\leftrightarrow \exists r\in B\left(\left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\wedge \neg r\in A\right)\right)$$
244	243	biimpa	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge \neg \forall x\in A\forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)\right)\to \exists r\in B\left(\left(\exists x\in A\neg r\underset{\dot{}}{\le }x\wedge \exists y\in A\neg y\underset{\dot{}}{\le }r\right)\wedge \neg r\in A\right)$$
245	9 184 244	r19.29af	$$⊢\left(\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\wedge \neg \forall x\in A\forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)\right)\to \neg J{\upharpoonright }_{𝑡}A\in \mathrm{Conn}$$
246	245	ex	$$⊢\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\to \left(\neg \forall x\in A\forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)\to \neg J{\upharpoonright }_{𝑡}A\in \mathrm{Conn}\right)$$
247	246	con4d	$$⊢\left(K\in \mathrm{Toset}\wedge A\subseteq B\right)\to \left(J{\upharpoonright }_{𝑡}A\in \mathrm{Conn}\to \forall x\in A\forall y\in A\forall r\in B\left(\left(x\underset{\dot{}}{\le }r\wedge r\underset{\dot{}}{\le }y\right)\to r\in A\right)\right)$$