Theorem ordtconnlem1 33695

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

Hypotheses

Ref	Expression
ordtconn.x	⊢ 𝐵 = (Base‘𝐾)
ordtconn.l	⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))
ordtconn.j	⊢ 𝐽 = (ordTop‘ ≤ )

Assertion

Ref	Expression
ordtconnlem1	⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Conn → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)))

Distinct variable groups:   𝑥,𝑟,𝑦,𝐴   𝐵,𝑟,𝑥,𝑦   𝐽,𝑟   𝐾,𝑟,𝑥,𝑦   𝑥, ≤ ,𝑦

Allowed substitution hints:   𝐽(𝑥,𝑦)   ≤ (𝑟)

Proof of Theorem ordtconnlem1

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1909	. . . . 5 ⊢ Ⅎ𝑟(𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵)
2		nfcv 2891	. . . . . . 7 ⊢ Ⅎ𝑟𝐴
3		nfra2w 3286	. . . . . . 7 ⊢ Ⅎ𝑟∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
4	2, 3	nfralw 3298	. . . . . 6 ⊢ Ⅎ𝑟∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
5	4	nfn 1852	. . . . 5 ⊢ Ⅎ𝑟 ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
6	1, 5	nfan 1894	. . . 4 ⊢ Ⅎ𝑟((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
7		tospos 18440	. . . . . . . . . 10 ⊢ (𝐾 ∈ Toset → 𝐾 ∈ Poset)
8		posprs 18336	. . . . . . . . . 10 ⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset )
9		ordtconn.j	. . . . . . . . . . 11 ⊢ 𝐽 = (ordTop‘ ≤ )
10		ordtconn.l	. . . . . . . . . . . . . 14 ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))
11		fvex 6913	. . . . . . . . . . . . . . 15 ⊢ (le‘𝐾) ∈ V
12	11	inex1 5321	. . . . . . . . . . . . . 14 ⊢ ((le‘𝐾) ∩ (𝐵 × 𝐵)) ∈ V
13	10, 12	eqeltri 2821	. . . . . . . . . . . . 13 ⊢ ≤ ∈ V
14		eqid 2725	. . . . . . . . . . . . . 14 ⊢ dom ≤ = dom ≤
15	14	ordttopon 23180	. . . . . . . . . . . . 13 ⊢ ( ≤ ∈ V → (ordTop‘ ≤ ) ∈ (TopOn‘dom ≤ ))
16	13, 15	ax-mp 5	. . . . . . . . . . . 12 ⊢ (ordTop‘ ≤ ) ∈ (TopOn‘dom ≤ )
17		ordtconn.x	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝐾)
18	17, 10	prsdm 33685	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵)
19	18	fveq2d 6904	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Proset → (TopOn‘dom ≤ ) = (TopOn‘𝐵))
20	16, 19	eleqtrid 2831	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Proset → (ordTop‘ ≤ ) ∈ (TopOn‘𝐵))
21	9, 20	eqeltrid 2829	. . . . . . . . . 10 ⊢ (𝐾 ∈ Proset → 𝐽 ∈ (TopOn‘𝐵))
22	7, 8, 21	3syl 18	. . . . . . . . 9 ⊢ (𝐾 ∈ Toset → 𝐽 ∈ (TopOn‘𝐵))
23	22	ad3antrrr 728	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐽 ∈ (TopOn‘𝐵))
24	23	adantlr 713	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐽 ∈ (TopOn‘𝐵))
25		simpllr 774	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ 𝐵)
26	25	adantlr 713	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ 𝐵)
27		simpll 765	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → 𝐾 ∈ Toset)
28		snex 5436	. . . . . . . . . . . . . . . 16 ⊢ {𝐵} ∈ V
29	17	fvexi 6914	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 ∈ V
30	29	mptex 7239	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∈ V
31	30	rnex 7922	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∈ V
32	29	mptex 7239	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ∈ V
33	32	rnex 7922	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ∈ V
34	31, 33	unex 7753	. . . . . . . . . . . . . . . 16 ⊢ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ∈ V
35	28, 34	unex 7753	. . . . . . . . . . . . . . 15 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ∈ V
36		ssfii 9458	. . . . . . . . . . . . . . 15 ⊢ (({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ∈ V → ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))))
37	35, 36	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))
38		fvex 6913	. . . . . . . . . . . . . . 15 ⊢ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))) ∈ V
39		bastg 22952	. . . . . . . . . . . . . . 15 ⊢ ((fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))) ∈ V → (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))))
40	38, 39	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))))
41	37, 40	sstri 3988	. . . . . . . . . . . . 13 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))))
42		eqid 2725	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
43		eqid 2725	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
44	17, 10, 42, 43	ordtprsval 33689	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ Proset → (ordTop‘ ≤ ) = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))))
45	9, 44	eqtrid 2777	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Proset → 𝐽 = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))))
46	41, 45	sseqtrrid 4032	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Proset → ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ 𝐽)
47	46	unssbd 4188	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Proset → (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ⊆ 𝐽)
48	27, 7, 8, 47	4syl 19	. . . . . . . . . 10 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ⊆ 𝐽)
49	48	unssbd 4188	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⊆ 𝐽)
50		breq2 5156	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (𝑟 ≤ 𝑧 ↔ 𝑟 ≤ 𝑦))
51	50	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (¬ 𝑟 ≤ 𝑧 ↔ ¬ 𝑟 ≤ 𝑦))
52	51	cbvrabv 3429	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦}
53		breq1 5155	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → (𝑥 ≤ 𝑦 ↔ 𝑟 ≤ 𝑦))
54	53	notbid 317	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → (¬ 𝑥 ≤ 𝑦 ↔ ¬ 𝑟 ≤ 𝑦))
55	54	rabbidv 3426	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑟 → {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦})
56	55	rspceeqv 3629	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝐵 ∧ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦}) → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
57	52, 56	mpan2 689	. . . . . . . . . . 11 ⊢ (𝑟 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
58	29	rabex 5338	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ V
59		eqid 2725	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
60	59	elrnmpt 5961	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ V → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
61	58, 60	ax-mp 5	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
62	57, 61	sylibr 233	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝐵 → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
63	62	adantl 480	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
64	49, 63	sseldd 3979	. . . . . . . 8 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ 𝐽)
65	64	ad2antrr 724	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ 𝐽)
66	48	unssad 4187	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ⊆ 𝐽)
67		breq1 5155	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (𝑧 ≤ 𝑟 ↔ 𝑦 ≤ 𝑟))
68	67	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (¬ 𝑧 ≤ 𝑟 ↔ ¬ 𝑦 ≤ 𝑟))
69	68	cbvrabv 3429	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟}
70		breq2 5156	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 𝑟))
71	70	notbid 317	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → (¬ 𝑦 ≤ 𝑥 ↔ ¬ 𝑦 ≤ 𝑟))
72	71	rabbidv 3426	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑟 → {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟})
73	72	rspceeqv 3629	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝐵 ∧ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟}) → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
74	69, 73	mpan2 689	. . . . . . . . . . 11 ⊢ (𝑟 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
75	29	rabex 5338	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ V
76		eqid 2725	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
77	76	elrnmpt 5961	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ V → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}))
78	75, 77	ax-mp 5	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
79	74, 78	sylibr 233	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝐵 → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}))
80	79	adantl 480	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}))
81	66, 80	sseldd 3979	. . . . . . . 8 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ 𝐽)
82	81	ad2antrr 724	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ 𝐽)
83		simpll 765	. . . . . . . . 9 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵))
84		simpr 483	. . . . . . . . 9 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
85	83, 84	jca 510	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴))
86		simplrl 775	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥)
87		ssel 3972	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
88	87	ancrd 550	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)))
89	88	anim1d 609	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥)))
90	89	impl 454	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥))
91		elin 3962	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ↔ (𝑥 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑥 ∈ 𝐴))
92		breq2 5156	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑥 → (𝑟 ≤ 𝑧 ↔ 𝑟 ≤ 𝑥))
93	92	notbid 317	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑥 → (¬ 𝑟 ≤ 𝑧 ↔ ¬ 𝑟 ≤ 𝑥))
94	93	elrab 3680	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥))
95	94	anbi1i 622	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑥 ∈ 𝐴) ↔ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥) ∧ 𝑥 ∈ 𝐴))
96		an32 644	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥) ∧ 𝑥 ∈ 𝐴) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥))
97	91, 95, 96	3bitri 296	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥))
98	90, 97	sylibr 233	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → 𝑥 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴))
99	98	ne0d 4337	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
100	25, 99	sylanl1 678	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
101	100	r19.29an 3147	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ ∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
102	85, 86, 101	syl2anc 582	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
103		simplrr 776	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)
104		ssel 3972	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
105	104	ancrd 550	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)))
106	105	anim1d 609	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 → ((𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑟) → ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟)))
107	106	impl 454	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟))
108		elin 3962	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ↔ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∧ 𝑦 ∈ 𝐴))
109	68	elrab 3680	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ↔ (𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟))
110	109	anbi1i 622	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∧ 𝑦 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟) ∧ 𝑦 ∈ 𝐴))
111		an32 644	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟) ∧ 𝑦 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟))
112	108, 110, 111	3bitri 296	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟))
113	107, 112	sylibr 233	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → 𝑦 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴))
114	113	ne0d 4337	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
115	25, 114	sylanl1 678	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
116	115	r19.29an 3147	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
117	85, 103, 116	syl2anc 582	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
118	17, 10	trleile 32829	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑟 ≤ 𝑧 ∨ 𝑧 ≤ 𝑟))
119		oran 987	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ≤ 𝑧 ∨ 𝑧 ≤ 𝑟) ↔ ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
120	118, 119	sylib 217	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
121	120	3expa 1115	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
122	121	nrexdv 3138	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) → ¬ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
123		rabid 3439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧))
124		rabid 3439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟))
125	123, 124	anbi12i 626	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
126		elin 3962	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
127		anandi 674	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
128	125, 126, 127	3bitr4i 302	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ (𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
129	128	exbii 1842	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ ∃𝑧(𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
130		nfrab1 3438	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧{𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧}
131		nfrab1 3438	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧{𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}
132	130, 131	nfin 4216	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟})
133	132	n0f 4344	. . . . . . . . . . . . . . 15 ⊢ (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
134		df-rex 3060	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟) ↔ ∃𝑧(𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
135	129, 133, 134	3bitr4i 302	. . . . . . . . . . . . . 14 ⊢ (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ≠ ∅ ↔ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
136	135	necon1bbii 2979	. . . . . . . . . . . . 13 ⊢ (¬ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟) ↔ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
137	122, 136	sylib 217	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
138	137	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
139	138	adantr 479	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
140	139	ineq1d 4211	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = (∅ ∩ 𝐴))
141		0in 4397	. . . . . . . . 9 ⊢ (∅ ∩ 𝐴) = ∅
142	140, 141	eqtrdi 2781	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = ∅)
143	142	adantlr 713	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = ∅)
144		simplr 767	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐵)
145		simpr 483	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
146		vex 3465	. . . . . . . . . . . . . . 15 ⊢ 𝑟 ∈ V
147	146	snss 4793	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ 𝐵 ↔ {𝑟} ⊆ 𝐵)
148		eldif 3956	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ (𝐵 ∖ 𝐴) ↔ (𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴))
149	146	snss 4793	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ (𝐵 ∖ 𝐴) ↔ {𝑟} ⊆ (𝐵 ∖ 𝐴))
150	148, 149	bitr3i 276	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ {𝑟} ⊆ (𝐵 ∖ 𝐴))
151		ssconb 4136	. . . . . . . . . . . . . . 15 ⊢ (({𝑟} ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐵) → ({𝑟} ⊆ (𝐵 ∖ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
152	150, 151	bitrid 282	. . . . . . . . . . . . . 14 ⊢ (({𝑟} ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐵) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
153	147, 152	sylanb 579	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐵) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
154	153	adantl 480	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Toset ∧ (𝑟 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐵)) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
155	154	anass1rs 653	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
156	155	adantr 479	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
157	144, 145, 156	mpbi2and 710	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ (𝐵 ∖ {𝑟}))
158	7	ad3antrrr 728	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐾 ∈ Poset)
159		nfv 1909	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵)
160	130, 131	nfun 4164	. . . . . . . . . . 11 ⊢ Ⅎ𝑧({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟})
161		nfcv 2891	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝐵 ∖ {𝑟})
162		ianor 979	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟))
163	17, 10	posrasymb 32823	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ 𝑟 = 𝑧))
164		equcom 2013	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑧 ↔ 𝑧 = 𝑟)
165	163, 164	bitrdi 286	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ 𝑧 = 𝑟))
166	165	necon3bbid 2967	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (¬ (𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ 𝑧 ≠ 𝑟))
167	162, 166	bitr3id 284	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟) ↔ 𝑧 ≠ 𝑟))
168	167	3expia 1118	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → (𝑧 ∈ 𝐵 → ((¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟) ↔ 𝑧 ≠ 𝑟)))
169	168	pm5.32d 575	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟)) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟)))
170	123, 124	orbi12i 912	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∨ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∨ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
171		elun 4147	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∨ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
172		andi 1005	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟)) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∨ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
173	170, 171, 172	3bitr4ri 303	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟)) ↔ 𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
174		eldifsn 4794	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐵 ∖ {𝑟}) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟))
175	174	bicomi 223	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟}))
176	169, 173, 175	3bitr3g 312	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟})))
177	159, 160, 161, 176	eqrd 3998	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = (𝐵 ∖ {𝑟}))
178	158, 144, 177	syl2anc 582	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = (𝐵 ∖ {𝑟}))
179	157, 178	sseqtrrd 4020	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
180	179	adantlr 713	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
181	24, 26, 65, 82, 102, 117, 143, 180	nconnsubb 23410	. . . . . 6 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
182	181	anasss 465	. . . . 5 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
183	182	adantllr 717	. . . 4 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐵) ∧ ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
184		rexanali 3091	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
185	184	rexbii 3083	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑦 ∈ 𝐴 ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
186		rexcom 3277	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
187		rexnal 3089	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
188	185, 186, 187	3bitr3i 300	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
189	188	rexbii 3083	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑥 ∈ 𝐴 ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
190		rexcom 3277	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
191		rexnal 3089	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
192	189, 190, 191	3bitr3i 300	. . . . . . 7 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
193		r19.41v 3178	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
194	193	rexbii 3083	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
195		r19.41v 3178	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
196		reeanv 3216	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ↔ (∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦))
197	196	anbi1i 622	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
198	194, 195, 197	3bitri 296	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
199	198	rexbii 3083	. . . . . . 7 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
200	192, 199	bitr3i 276	. . . . . 6 ⊢ (¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
201	27	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐾 ∈ Toset)
202	25	sselda 3978	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)
203		simpllr 774	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑟 ∈ 𝐵)
204	17, 10	trleile 32829	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥))
205	201, 202, 203, 204	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥))
206		simpr 483	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
207		simplr 767	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
208		nelne2 3029	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑟 ∈ 𝐴) → 𝑥 ≠ 𝑟)
209	206, 207, 208	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ 𝑟)
210	158	adantr 479	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐾 ∈ Poset)
211	17, 10	posrasymb 32823	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥) ↔ 𝑥 = 𝑟))
212	211	necon3bbid 2967	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥) ↔ 𝑥 ≠ 𝑟))
213	210, 202, 203, 212	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥) ↔ 𝑥 ≠ 𝑟))
214	209, 213	mpbird 256	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → ¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥))
215	205, 214	jca 510	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥) ∧ ¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥)))
216		pm5.17 1009	. . . . . . . . . . . 12 ⊢ (((𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥) ∧ ¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥)) ↔ (𝑥 ≤ 𝑟 ↔ ¬ 𝑟 ≤ 𝑥))
217	215, 216	sylib 217	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≤ 𝑟 ↔ ¬ 𝑟 ≤ 𝑥))
218	217	rexbidva 3166	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ↔ ∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥))
219	27	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ Toset)
220		simpllr 774	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑟 ∈ 𝐵)
221	25	sselda 3978	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐵)
222	17, 10	trleile 32829	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟))
223	219, 220, 221, 222	syl3anc 1368	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟))
224		simpr 483	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
225		simplr 767	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
226		nelne2 3029	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐴 ∧ ¬ 𝑟 ∈ 𝐴) → 𝑦 ≠ 𝑟)
227	224, 225, 226	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ≠ 𝑟)
228	227	necomd 2985	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑟 ≠ 𝑦)
229	158	adantr 479	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ Poset)
230	17, 10	posrasymb 32823	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟) ↔ 𝑟 = 𝑦))
231	230	necon3bbid 2967	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟) ↔ 𝑟 ≠ 𝑦))
232	229, 220, 221, 231	syl3anc 1368	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟) ↔ 𝑟 ≠ 𝑦))
233	228, 232	mpbird 256	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟))
234	223, 233	jca 510	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ((𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟) ∧ ¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟)))
235		pm5.17 1009	. . . . . . . . . . . 12 ⊢ (((𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟) ∧ ¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟)) ↔ (𝑟 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑟))
236	234, 235	sylib 217	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑟 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑟))
237	236	rexbidva 3166	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟))
238	218, 237	anbi12d 630	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ↔ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)))
239	238	ex 411	. . . . . . . 8 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → (¬ 𝑟 ∈ 𝐴 → ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ↔ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟))))
240	239	pm5.32rd 576	. . . . . . 7 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → (((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)))
241	240	rexbidva 3166	. . . . . 6 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → (∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)))
242	200, 241	bitrid 282	. . . . 5 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → (¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)))
243	242	biimpa 475	. . . 4 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)) → ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴))
244	6, 183, 243	r19.29af 3255	. . 3 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
245	244	ex 411	. 2 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → (¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) → ¬ (𝐽 ↾t 𝐴) ∈ Conn))
246	245	con4d 115	1 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Conn → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   ∧ w3a 1084   = wceq 1533  ∃wex 1773   ∈ wcel 2098   ≠ wne 2929  ∀wral 3050  ∃wrex 3059  {crab 3418  Vcvv 3461   ∖ cdif 3943   ∪ cun 3944   ∩ cin 3945   ⊆ wss 3946  ∅c0 4324  {csn 4632   class class class wbr 5152   ↦ cmpt 5235   × cxp 5679  dom cdm 5681  ran crn 5682  ‘cfv 6553  (class class class)co 7423  ficfi 9449  Basecbs 17208  lecple 17268   ↾_t crest 17430  topGenctg 17447  ordTopcordt 17509   Proset cproset 18313  Posetcpo 18327  Tosetctos 18436  TopOnctopon 22895  Conncconn 23398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7876  df-1st 8002  df-2nd 8003  df-1o 8495  df-2o 8496  df-en 8974  df-fin 8977  df-fi 9450  df-rest 17432  df-topgen 17453  df-ordt 17511  df-proset 18315  df-poset 18333  df-toset 18437  df-top 22879  df-topon 22896  df-bases 22932  df-cld 23006  df-conn 23399

This theorem is referenced by: (None)