Theorem ordtconnlem1 31853

Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 31854. See also reconnlem1 23970. (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 1920	. . . . 5 ⊢ Ⅎ𝑟(𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵)
2		nfcv 2908	. . . . . . 7 ⊢ Ⅎ𝑟𝐴
3		nfra2w 3153	. . . . . . 7 ⊢ Ⅎ𝑟∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
4	2, 3	nfralw 3151	. . . . . 6 ⊢ Ⅎ𝑟∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
5	4	nfn 1863	. . . . 5 ⊢ Ⅎ𝑟 ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
6	1, 5	nfan 1905	. . . 4 ⊢ Ⅎ𝑟((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
7		tospos 18119	. . . . . . . . . 10 ⊢ (𝐾 ∈ Toset → 𝐾 ∈ Poset)
8		posprs 18015	. . . . . . . . . 10 ⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset )
9		ordtconn.j	. . . . . . . . . . 11 ⊢ 𝐽 = (ordTop‘ ≤ )
10		ordtconn.l	. . . . . . . . . . . . . 14 ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))
11		fvex 6781	. . . . . . . . . . . . . . 15 ⊢ (le‘𝐾) ∈ V
12	11	inex1 5244	. . . . . . . . . . . . . 14 ⊢ ((le‘𝐾) ∩ (𝐵 × 𝐵)) ∈ V
13	10, 12	eqeltri 2836	. . . . . . . . . . . . 13 ⊢ ≤ ∈ V
14		eqid 2739	. . . . . . . . . . . . . 14 ⊢ dom ≤ = dom ≤
15	14	ordttopon 22325	. . . . . . . . . . . . 13 ⊢ ( ≤ ∈ V → (ordTop‘ ≤ ) ∈ (TopOn‘dom ≤ ))
16	13, 15	ax-mp 5	. . . . . . . . . . . 12 ⊢ (ordTop‘ ≤ ) ∈ (TopOn‘dom ≤ )
17		ordtconn.x	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝐾)
18	17, 10	prsdm 31843	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵)
19	18	fveq2d 6772	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Proset → (TopOn‘dom ≤ ) = (TopOn‘𝐵))
20	16, 19	eleqtrid 2846	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Proset → (ordTop‘ ≤ ) ∈ (TopOn‘𝐵))
21	9, 20	eqeltrid 2844	. . . . . . . . . 10 ⊢ (𝐾 ∈ Proset → 𝐽 ∈ (TopOn‘𝐵))
22	7, 8, 21	3syl 18	. . . . . . . . 9 ⊢ (𝐾 ∈ Toset → 𝐽 ∈ (TopOn‘𝐵))
23	22	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐽 ∈ (TopOn‘𝐵))
24	23	adantlr 711	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐽 ∈ (TopOn‘𝐵))
25		simpllr 772	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ 𝐵)
26	25	adantlr 711	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ 𝐵)
27		simpll 763	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → 𝐾 ∈ Toset)
28	27, 7, 8	3syl 18	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → 𝐾 ∈ Proset )
29		snex 5357	. . . . . . . . . . . . . . . 16 ⊢ {𝐵} ∈ V
30	17	fvexi 6782	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 ∈ V
31	30	mptex 7093	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∈ V
32	31	rnex 7746	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∈ V
33	30	mptex 7093	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ∈ V
34	33	rnex 7746	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ∈ V
35	32, 34	unex 7587	. . . . . . . . . . . . . . . 16 ⊢ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ∈ V
36	29, 35	unex 7587	. . . . . . . . . . . . . . 15 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ∈ V
37		ssfii 9139	. . . . . . . . . . . . . . 15 ⊢ (({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ∈ V → ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))))
38	36, 37	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))
39		fvex 6781	. . . . . . . . . . . . . . 15 ⊢ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))) ∈ V
40		bastg 22097	. . . . . . . . . . . . . . 15 ⊢ ((fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))) ∈ V → (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))))
41	39, 40	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))))
42	38, 41	sstri 3934	. . . . . . . . . . . . 13 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))))
43		eqid 2739	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
44		eqid 2739	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
45	17, 10, 43, 44	ordtprsval 31847	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ Proset → (ordTop‘ ≤ ) = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))))
46	9, 45	eqtrid 2791	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Proset → 𝐽 = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))))
47	42, 46	sseqtrrid 3978	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Proset → ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ 𝐽)
48	47	unssbd 4126	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Proset → (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ⊆ 𝐽)
49	28, 48	syl 17	. . . . . . . . . 10 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ⊆ 𝐽)
50	49	unssbd 4126	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⊆ 𝐽)
51		breq2 5082	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (𝑟 ≤ 𝑧 ↔ 𝑟 ≤ 𝑦))
52	51	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (¬ 𝑟 ≤ 𝑧 ↔ ¬ 𝑟 ≤ 𝑦))
53	52	cbvrabv 3424	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦}
54		breq1 5081	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → (𝑥 ≤ 𝑦 ↔ 𝑟 ≤ 𝑦))
55	54	notbid 317	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → (¬ 𝑥 ≤ 𝑦 ↔ ¬ 𝑟 ≤ 𝑦))
56	55	rabbidv 3412	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑟 → {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦})
57	56	rspceeqv 3575	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝐵 ∧ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦}) → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
58	53, 57	mpan2 687	. . . . . . . . . . 11 ⊢ (𝑟 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
59	30	rabex 5259	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ V
60		eqid 2739	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
61	60	elrnmpt 5862	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ V → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
62	59, 61	ax-mp 5	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
63	58, 62	sylibr 233	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝐵 → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
64	63	adantl 481	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
65	50, 64	sseldd 3926	. . . . . . . 8 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ 𝐽)
66	65	ad2antrr 722	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ 𝐽)
67	49	unssad 4125	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ⊆ 𝐽)
68		breq1 5081	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (𝑧 ≤ 𝑟 ↔ 𝑦 ≤ 𝑟))
69	68	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (¬ 𝑧 ≤ 𝑟 ↔ ¬ 𝑦 ≤ 𝑟))
70	69	cbvrabv 3424	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟}
71		breq2 5082	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 𝑟))
72	71	notbid 317	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → (¬ 𝑦 ≤ 𝑥 ↔ ¬ 𝑦 ≤ 𝑟))
73	72	rabbidv 3412	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑟 → {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟})
74	73	rspceeqv 3575	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝐵 ∧ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟}) → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
75	70, 74	mpan2 687	. . . . . . . . . . 11 ⊢ (𝑟 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
76	30	rabex 5259	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ V
77		eqid 2739	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
78	77	elrnmpt 5862	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ V → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}))
79	76, 78	ax-mp 5	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
80	75, 79	sylibr 233	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝐵 → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}))
81	80	adantl 481	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}))
82	67, 81	sseldd 3926	. . . . . . . 8 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ 𝐽)
83	82	ad2antrr 722	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ 𝐽)
84		simpll 763	. . . . . . . . 9 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵))
85		simpr 484	. . . . . . . . 9 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
86	84, 85	jca 511	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴))
87		simplrl 773	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥)
88		ssel 3918	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
89	88	ancrd 551	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)))
90	89	anim1d 610	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥)))
91	90	impl 455	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥))
92		elin 3907	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ↔ (𝑥 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑥 ∈ 𝐴))
93		breq2 5082	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑥 → (𝑟 ≤ 𝑧 ↔ 𝑟 ≤ 𝑥))
94	93	notbid 317	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑥 → (¬ 𝑟 ≤ 𝑧 ↔ ¬ 𝑟 ≤ 𝑥))
95	94	elrab 3625	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥))
96	95	anbi1i 623	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑥 ∈ 𝐴) ↔ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥) ∧ 𝑥 ∈ 𝐴))
97		an32 642	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥) ∧ 𝑥 ∈ 𝐴) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥))
98	92, 96, 97	3bitri 296	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥))
99	91, 98	sylibr 233	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → 𝑥 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴))
100	99	ne0d 4274	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
101	25, 100	sylanl1 676	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
102	101	r19.29an 3218	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ ∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
103	86, 87, 102	syl2anc 583	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
104		simplrr 774	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)
105		ssel 3918	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
106	105	ancrd 551	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)))
107	106	anim1d 610	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 → ((𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑟) → ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟)))
108	107	impl 455	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟))
109		elin 3907	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ↔ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∧ 𝑦 ∈ 𝐴))
110	69	elrab 3625	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ↔ (𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟))
111	110	anbi1i 623	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∧ 𝑦 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟) ∧ 𝑦 ∈ 𝐴))
112		an32 642	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟) ∧ 𝑦 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟))
113	109, 111, 112	3bitri 296	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟))
114	108, 113	sylibr 233	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → 𝑦 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴))
115	114	ne0d 4274	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
116	25, 115	sylanl1 676	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
117	116	r19.29an 3218	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
118	86, 104, 117	syl2anc 583	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
119	17, 10	trleile 31228	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑟 ≤ 𝑧 ∨ 𝑧 ≤ 𝑟))
120		oran 986	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ≤ 𝑧 ∨ 𝑧 ≤ 𝑟) ↔ ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
121	119, 120	sylib 217	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
122	121	3expa 1116	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
123	122	nrexdv 3199	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) → ¬ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
124		rabid 3308	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧))
125		rabid 3308	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟))
126	124, 125	anbi12i 626	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
127		elin 3907	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
128		anandi 672	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
129	126, 127, 128	3bitr4i 302	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ (𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
130	129	exbii 1853	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ ∃𝑧(𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
131		nfrab1 3315	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧{𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧}
132		nfrab1 3315	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧{𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}
133	131, 132	nfin 4155	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟})
134	133	n0f 4281	. . . . . . . . . . . . . . 15 ⊢ (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
135		df-rex 3071	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟) ↔ ∃𝑧(𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
136	130, 134, 135	3bitr4i 302	. . . . . . . . . . . . . 14 ⊢ (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ≠ ∅ ↔ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
137	136	necon1bbii 2994	. . . . . . . . . . . . 13 ⊢ (¬ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟) ↔ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
138	123, 137	sylib 217	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
139	138	adantlr 711	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
140	139	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
141	140	ineq1d 4150	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = (∅ ∩ 𝐴))
142		0in 4332	. . . . . . . . 9 ⊢ (∅ ∩ 𝐴) = ∅
143	141, 142	eqtrdi 2795	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = ∅)
144	143	adantlr 711	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = ∅)
145		simplr 765	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐵)
146		simpr 484	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
147		vex 3434	. . . . . . . . . . . . . . 15 ⊢ 𝑟 ∈ V
148	147	snss 4724	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ 𝐵 ↔ {𝑟} ⊆ 𝐵)
149		eldif 3901	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ (𝐵 ∖ 𝐴) ↔ (𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴))
150	147	snss 4724	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ (𝐵 ∖ 𝐴) ↔ {𝑟} ⊆ (𝐵 ∖ 𝐴))
151	149, 150	bitr3i 276	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ {𝑟} ⊆ (𝐵 ∖ 𝐴))
152		ssconb 4076	. . . . . . . . . . . . . . 15 ⊢ (({𝑟} ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐵) → ({𝑟} ⊆ (𝐵 ∖ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
153	151, 152	syl5bb 282	. . . . . . . . . . . . . 14 ⊢ (({𝑟} ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐵) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
154	148, 153	sylanb 580	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐵) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
155	154	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Toset ∧ (𝑟 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐵)) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
156	155	anass1rs 651	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
157	156	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
158	145, 146, 157	mpbi2and 708	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ (𝐵 ∖ {𝑟}))
159	7	ad3antrrr 726	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐾 ∈ Poset)
160		nfv 1920	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵)
161	131, 132	nfun 4103	. . . . . . . . . . 11 ⊢ Ⅎ𝑧({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟})
162		nfcv 2908	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝐵 ∖ {𝑟})
163		ianor 978	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟))
164	17, 10	posrasymb 31222	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ 𝑟 = 𝑧))
165		equcom 2024	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑧 ↔ 𝑧 = 𝑟)
166	164, 165	bitrdi 286	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ 𝑧 = 𝑟))
167	166	necon3bbid 2982	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (¬ (𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ 𝑧 ≠ 𝑟))
168	163, 167	bitr3id 284	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟) ↔ 𝑧 ≠ 𝑟))
169	168	3expia 1119	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → (𝑧 ∈ 𝐵 → ((¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟) ↔ 𝑧 ≠ 𝑟)))
170	169	pm5.32d 576	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟)) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟)))
171	124, 125	orbi12i 911	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∨ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∨ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
172		elun 4087	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∨ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
173		andi 1004	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟)) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∨ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
174	171, 172, 173	3bitr4ri 303	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟)) ↔ 𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
175		eldifsn 4725	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐵 ∖ {𝑟}) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟))
176	175	bicomi 223	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟}))
177	170, 174, 176	3bitr3g 312	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟})))
178	160, 161, 162, 177	eqrd 3944	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = (𝐵 ∖ {𝑟}))
179	159, 145, 178	syl2anc 583	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = (𝐵 ∖ {𝑟}))
180	158, 179	sseqtrrd 3966	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
181	180	adantlr 711	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
182	24, 26, 66, 83, 103, 118, 144, 181	nconnsubb 22555	. . . . . 6 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
183	182	anasss 466	. . . . 5 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
184	183	adantllr 715	. . . 4 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐵) ∧ ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
185		rexanali 3193	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
186	185	rexbii 3179	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑦 ∈ 𝐴 ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
187		rexcom 3283	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
188		rexnal 3167	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
189	186, 187, 188	3bitr3i 300	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
190	189	rexbii 3179	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑥 ∈ 𝐴 ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
191		rexcom 3283	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
192		rexnal 3167	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
193	190, 191, 192	3bitr3i 300	. . . . . . 7 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
194		r19.41v 3275	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
195	194	rexbii 3179	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
196		r19.41v 3275	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
197		reeanv 3294	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ↔ (∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦))
198	197	anbi1i 623	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
199	195, 196, 198	3bitri 296	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
200	199	rexbii 3179	. . . . . . 7 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
201	193, 200	bitr3i 276	. . . . . 6 ⊢ (¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
202	27	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐾 ∈ Toset)
203	25	sselda 3925	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)
204		simpllr 772	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑟 ∈ 𝐵)
205	17, 10	trleile 31228	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥))
206	202, 203, 204, 205	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥))
207		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
208		simplr 765	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
209		nelne2 3043	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑟 ∈ 𝐴) → 𝑥 ≠ 𝑟)
210	207, 208, 209	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ 𝑟)
211	159	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐾 ∈ Poset)
212	17, 10	posrasymb 31222	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥) ↔ 𝑥 = 𝑟))
213	212	necon3bbid 2982	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥) ↔ 𝑥 ≠ 𝑟))
214	211, 203, 204, 213	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥) ↔ 𝑥 ≠ 𝑟))
215	210, 214	mpbird 256	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → ¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥))
216	206, 215	jca 511	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥) ∧ ¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥)))
217		pm5.17 1008	. . . . . . . . . . . 12 ⊢ (((𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥) ∧ ¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥)) ↔ (𝑥 ≤ 𝑟 ↔ ¬ 𝑟 ≤ 𝑥))
218	216, 217	sylib 217	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≤ 𝑟 ↔ ¬ 𝑟 ≤ 𝑥))
219	218	rexbidva 3226	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ↔ ∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥))
220	27	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ Toset)
221		simpllr 772	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑟 ∈ 𝐵)
222	25	sselda 3925	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐵)
223	17, 10	trleile 31228	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟))
224	220, 221, 222, 223	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟))
225		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
226		simplr 765	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
227		nelne2 3043	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐴 ∧ ¬ 𝑟 ∈ 𝐴) → 𝑦 ≠ 𝑟)
228	225, 226, 227	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ≠ 𝑟)
229	228	necomd 3000	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑟 ≠ 𝑦)
230	159	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ Poset)
231	17, 10	posrasymb 31222	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟) ↔ 𝑟 = 𝑦))
232	231	necon3bbid 2982	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟) ↔ 𝑟 ≠ 𝑦))
233	230, 221, 222, 232	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟) ↔ 𝑟 ≠ 𝑦))
234	229, 233	mpbird 256	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟))
235	224, 234	jca 511	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ((𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟) ∧ ¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟)))
236		pm5.17 1008	. . . . . . . . . . . 12 ⊢ (((𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟) ∧ ¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟)) ↔ (𝑟 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑟))
237	235, 236	sylib 217	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑟 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑟))
238	237	rexbidva 3226	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟))
239	219, 238	anbi12d 630	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ↔ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)))
240	239	ex 412	. . . . . . . 8 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → (¬ 𝑟 ∈ 𝐴 → ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ↔ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟))))
241	240	pm5.32rd 577	. . . . . . 7 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → (((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)))
242	241	rexbidva 3226	. . . . . 6 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → (∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)))
243	201, 242	syl5bb 282	. . . . 5 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → (¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)))
244	243	biimpa 476	. . . 4 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)) → ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴))
245	6, 184, 244	r19.29af 3261	. . 3 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
246	245	ex 412	. 2 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → (¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) → ¬ (𝐽 ↾t 𝐴) ∈ Conn))
247	246	con4d 115	1 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Conn → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   ∧ w3a 1085   = wceq 1541  ∃wex 1785   ∈ wcel 2109   ≠ wne 2944  ∀wral 3065  ∃wrex 3066  {crab 3069  Vcvv 3430   ∖ cdif 3888   ∪ cun 3889   ∩ cin 3890   ⊆ wss 3891  ∅c0 4261  {csn 4566   class class class wbr 5078   ↦ cmpt 5161   × cxp 5586  dom cdm 5588  ran crn 5589  ‘cfv 6430  (class class class)co 7268  ficfi 9130  Basecbs 16893  lecple 16950   ↾_t crest 17112  topGenctg 17129  ordTopcordt 17191   Proset cproset 17992  Posetcpo 18006  Tosetctos 18115  TopOnctopon 22040  Conncconn 22543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-rep 5213  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-int 4885  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-ov 7271  df-oprab 7272  df-mpo 7273  df-om 7701  df-1st 7817  df-2nd 7818  df-1o 8281  df-er 8472  df-en 8708  df-fin 8711  df-fi 9131  df-rest 17114  df-topgen 17135  df-ordt 17193  df-proset 17994  df-poset 18012  df-toset 18116  df-top 22024  df-topon 22041  df-bases 22077  df-cld 22151  df-conn 22544

This theorem is referenced by: (None)