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		snex	$$⊢\left\{B\right\}\in \mathrm{V}$$
29	1	fvexi	$$⊢B\in \mathrm{V}$$
30	29	mptex	$$⊢\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)\in \mathrm{V}$$
31	30	rnex	$$⊢\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg y\underset{\dot{}}{\le }x\right\}\right)\in \mathrm{V}$$
32	29	mptex	$$⊢\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)\in \mathrm{V}$$
33	32	rnex	$$⊢\mathrm{ran}\left(x\in B⟼\left\{y\in B|\neg x\underset{\dot{}}{\le }y\right\}\right)\in \mathrm{V}$$
34	31 33	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}$$
35	28 34	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}$$
36		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)$$
37	35 36	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)$$
38		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}$$
39		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)$$
40	38 39	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)$$
41	37 40	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)$$
42		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)$$
43		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)$$
44	1 2 42 43	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)$$
45	3 44	eqtrid	$$⊢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)$$
46	41 45	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$$
47	46	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$$
48	27 10 11 47	4syl	$$⊢\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$$
49	48	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$$
50		breq2	$$⊢z=y\to \left(r\underset{\dot{}}{\le }z\leftrightarrow r\underset{\dot{}}{\le }y\right)$$
51	50	notbid	$$⊢z=y\to \left(\neg r\underset{\dot{}}{\le }z\leftrightarrow \neg r\underset{\dot{}}{\le }y\right)$$
52	51	cbvrabv	$$⊢\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}=\left\{y\in B|\neg r\underset{\dot{}}{\le }y\right\}$$
53		breq1	$$⊢x=r\to \left(x\underset{\dot{}}{\le }y\leftrightarrow r\underset{\dot{}}{\le }y\right)$$
54	53	notbid	$$⊢x=r\to \left(\neg x\underset{\dot{}}{\le }y\leftrightarrow \neg r\underset{\dot{}}{\le }y\right)$$
55	54	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\}$$
56	55	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\}$$
57	52 56	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\}$$
58	29	rabex	$$⊢\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}\in \mathrm{V}$$
59		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)$$
60	59	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)$$
61	58 60	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\}$$
62	57 61	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)$$
63	62	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)$$
64	49 63	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$$
65	64	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$$
66	48	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$$
67		breq1	$$⊢z=y\to \left(z\underset{\dot{}}{\le }r\leftrightarrow y\underset{\dot{}}{\le }r\right)$$
68	67	notbid	$$⊢z=y\to \left(\neg z\underset{\dot{}}{\le }r\leftrightarrow \neg y\underset{\dot{}}{\le }r\right)$$
69	68	cbvrabv	$$⊢\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}=\left\{y\in B|\neg y\underset{\dot{}}{\le }r\right\}$$
70		breq2	$$⊢x=r\to \left(y\underset{\dot{}}{\le }x\leftrightarrow y\underset{\dot{}}{\le }r\right)$$
71	70	notbid	$$⊢x=r\to \left(\neg y\underset{\dot{}}{\le }x\leftrightarrow \neg y\underset{\dot{}}{\le }r\right)$$
72	71	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\}$$
73	72	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\}$$
74	69 73	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\}$$
75	29	rabex	$$⊢\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}\in \mathrm{V}$$
76		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)$$
77	76	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)$$
78	75 77	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\}$$
79	74 78	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)$$
80	79	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)$$
81	66 80	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$$
82	81	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$$
83		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)$$
84		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$$
85	83 84	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)$$
86		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$$
87		ssel	$$⊢A\subseteq B\to \left(x\in A\to x\in B\right)$$
88	87	ancrd	$$⊢A\subseteq B\to \left(x\in A\to \left(x\in B\wedge x\in A\right)\right)$$
89	88	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)$$
90	89	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)$$
91		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)$$
92		breq2	$$⊢z=x\to \left(r\underset{\dot{}}{\le }z\leftrightarrow r\underset{\dot{}}{\le }x\right)$$
93	92	notbid	$$⊢z=x\to \left(\neg r\underset{\dot{}}{\le }z\leftrightarrow \neg r\underset{\dot{}}{\le }x\right)$$
94	93	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)$$
95	94	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)$$
96		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)$$
97	91 95 96	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)$$
98	90 97	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)$$
99	98	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$$
100	25 99	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$$
101	100	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$$
102	85 86 101	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$$
103		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$$
104		ssel	$$⊢A\subseteq B\to \left(y\in A\to y\in B\right)$$
105	104	ancrd	$$⊢A\subseteq B\to \left(y\in A\to \left(y\in B\wedge y\in A\right)\right)$$
106	105	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)$$
107	106	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)$$
108		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)$$
109	68	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)$$
110	109	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)$$
111		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)$$
112	108 110 111	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)$$
113	107 112	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)$$
114	113	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$$
115	25 114	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$$
116	115	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$$
117	85 103 116	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$$
118	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)$$
119		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)$$
120	118 119	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)$$
121	120	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)$$
122	121	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)$$
123		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)$$
124		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)$$
125	123 124	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)$$
126		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)$$
127		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)$$
128	125 126 127	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)$$
129	128	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)$$
130		nfrab1	$$⊢\underset{\_}{Ⅎ}z\left\{z\in B|\neg r\underset{\dot{}}{\le }z\right\}$$
131		nfrab1	$$⊢\underset{\_}{Ⅎ}z\left\{z\in B|\neg z\underset{\dot{}}{\le }r\right\}$$
132	130 131	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)$$
133	132	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)$$
134		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)$$
135	129 133 134	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)$$
136	135	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$$
137	122 136	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$$
138	137	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$$
139	138	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$$
140	139	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$$
141		0in	$$⊢\varnothing \cap A=\varnothing$$
142	140 141	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$$
143	142	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$$
144		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$$
145		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$$
146		vex	$$⊢r\in \mathrm{V}$$
147	146	snss	$$⊢r\in B\leftrightarrow \left\{r\right\}\subseteq B$$
148		eldif	$$⊢r\in \left(B\setminus A\right)\leftrightarrow \left(r\in B\wedge \neg r\in A\right)$$
149	146	snss	$$⊢r\in \left(B\setminus A\right)\leftrightarrow \left\{r\right\}\subseteq B\setminus A$$
150	148 149	bitr3i	$$⊢\left(r\in B\wedge \neg r\in A\right)\leftrightarrow \left\{r\right\}\subseteq B\setminus A$$
151		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)$$
152	150 151	bitrid	$$⊢\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)$$
153	147 152	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)$$
154	153	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)$$
155	154	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)$$
156	155	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)$$
157	144 145 156	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\}$$
158	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}$$
159		nfv	$$⊢Ⅎz\left(K\in \mathrm{Poset}\wedge r\in B\right)$$
160	130 131	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)$$
161		nfcv	$$⊢\underset{\_}{Ⅎ}z\left(B\setminus \left\{r\right\}\right)$$
162		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)$$
163	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)$$
164		equcom	$$⊢r=z\leftrightarrow z=r$$
165	163 164	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)$$
166	165	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)$$
167	162 166	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)$$
168	167	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)$$
169	168	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)$$
170	123 124	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)$$
171		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)$$
172		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)$$
173	170 171 172	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)$$
174		eldifsn	$$⊢z\in \left(B\setminus \left\{r\right\}\right)\leftrightarrow \left(z\in B\wedge z\ne r\right)$$
175	174	bicomi	$$⊢\left(z\in B\wedge z\ne r\right)\leftrightarrow z\in \left(B\setminus \left\{r\right\}\right)$$
176	169 173 175	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)$$
177	159 160 161 176	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\}$$
178	158 144 177	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\}$$
179	157 178	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\}$$
180	179	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\}$$
181	24 26 65 82 102 117 143 180	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}$$
182	181	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}$$
183	182	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}$$
184		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)$$
185	184	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)$$
186		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)$$
187		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)$$
188	185 186 187	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)$$
189	188	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)$$
190		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)$$
191		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)$$
192	189 190 191	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)$$
193		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)$$
194	193	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)$$
195		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)$$
196		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)$$
197	196	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)$$
198	194 195 197	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)$$
199	198	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)$$
200	192 199	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)$$
201	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}$$
202	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$$
203		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$$
204	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)$$
205	201 202 203 204	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)$$
206		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$$
207		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$$
208		nelne2	$$⊢\left(x\in A\wedge \neg r\in A\right)\to x\ne r$$
209	206 207 208	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$$
210	158	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}$$
211	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)$$
212	211	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)$$
213	210 202 203 212	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)$$
214	209 213	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)$$
215	205 214	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)$$
216		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)$$
217	215 216	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)$$
218	217	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)$$
219	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}$$
220		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$$
221	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$$
222	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)$$
223	219 220 221 222	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)$$
224		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$$
225		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$$
226		nelne2	$$⊢\left(y\in A\wedge \neg r\in A\right)\to y\ne r$$
227	224 225 226	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$$
228	227	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$$
229	158	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}$$
230	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)$$
231	230	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)$$
232	229 220 221 231	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)$$
233	228 232	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)$$
234	223 233	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)$$
235		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)$$
236	234 235	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)$$
237	236	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)$$
238	218 237	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)$$
239	238	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)$$
240	239	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)$$
241	240	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)$$
242	200 241	bitrid	$$⊢\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)$$
243	242	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)$$
244	9 183 243	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}$$
245	244	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)$$
246	245	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)$$