Theorem ordtconnlem1 34612

Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 34613. See also reconnlem1 25161. (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 1948	. . . . 5 ⊢ Ⅎ𝑟(𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵)
2		nfcv 2926	. . . . . . 7 ⊢ Ⅎ𝑟𝐴
3		nfra2w 3302	. . . . . . 7 ⊢ Ⅎ𝑟∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
4	2, 3	nfralw 3313	. . . . . 6 ⊢ Ⅎ𝑟∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
5	4	nfn 1889	. . . . 5 ⊢ Ⅎ𝑟 ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
6	1, 5	nfan 1933	. . . 4 ⊢ Ⅎ𝑟((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
7		tospos 18607	. . . . . . . . . 10 ⊢ (𝐾 ∈ Toset → 𝐾 ∈ Poset)
8		posprs 18505	. . . . . . . . . 10 ⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset )
9		ordtconn.j	. . . . . . . . . . 11 ⊢ 𝐽 = (ordTop‘ ≤ )
10		ordtconn.l	. . . . . . . . . . . . . 14 ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))
11		fvex 6909	. . . . . . . . . . . . . . 15 ⊢ (le‘𝐾) ∈ V
12	11	inex1 5281	. . . . . . . . . . . . . 14 ⊢ ((le‘𝐾) ∩ (𝐵 × 𝐵)) ∈ V
13	10, 12	eqeltri 2860	. . . . . . . . . . . . 13 ⊢ ≤ ∈ V
14		eqid 2763	. . . . . . . . . . . . . 14 ⊢ dom ≤ = dom ≤
15	14	ordttopon 23526	. . . . . . . . . . . . 13 ⊢ ( ≤ ∈ V → (ordTop‘ ≤ ) ∈ (TopOn‘dom ≤ ))
16	13, 15	ax-mp 5	. . . . . . . . . . . 12 ⊢ (ordTop‘ ≤ ) ∈ (TopOn‘dom ≤ )
17		ordtconn.x	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝐾)
18	17, 10	prsdm 34602	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵)
19	18	fveq2d 6900	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Proset → (TopOn‘dom ≤ ) = (TopOn‘𝐵))
20	16, 19	eleqtrid 2870	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Proset → (ordTop‘ ≤ ) ∈ (TopOn‘𝐵))
21	9, 20	eqeltrid 2868	. . . . . . . . . 10 ⊢ (𝐾 ∈ Proset → 𝐽 ∈ (TopOn‘𝐵))
22	7, 8, 21	3syl 19	. . . . . . . . 9 ⊢ (𝐾 ∈ Toset → 𝐽 ∈ (TopOn‘𝐵))
23	22	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐽 ∈ (TopOn‘𝐵))
24	23	adantlr 728	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐽 ∈ (TopOn‘𝐵))
25		simpllr 788	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ 𝐵)
26	25	adantlr 728	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ 𝐵)
27		simpll 779	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → 𝐾 ∈ Toset)
28		snex 5401	. . . . . . . . . . . . . . . 16 ⊢ {𝐵} ∈ V
29	17	fvexi 6910	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 ∈ V
30	29	mptex 7239	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∈ V
31	30	rnex 7932	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∈ V
32	29	mptex 7239	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ∈ V
33	32	rnex 7932	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ∈ V
34	31, 33	unex 7771	. . . . . . . . . . . . . . . 16 ⊢ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ∈ V
35	28, 34	unex 7771	. . . . . . . . . . . . . . 15 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ∈ V
36		ssfii 9424	. . . . . . . . . . . . . . 15 ⊢ (({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ∈ V → ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))))
37	35, 36	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))
38		fvex 6909	. . . . . . . . . . . . . . 15 ⊢ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))) ∈ V
39		bastg 23299	. . . . . . . . . . . . . . 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 3922	. . . . . . . . . . . . 13 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))))
42		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
43		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
44	17, 10, 42, 43	ordtprsval 34606	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ Proset → (ordTop‘ ≤ ) = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))))
45	9, 44	eqtrid 2810	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Proset → 𝐽 = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))))
46	41, 45	sseqtrrid 3956	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Proset → ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ 𝐽)
47	46	unssbd 4195	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Proset → (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ⊆ 𝐽)
48	27, 7, 8, 47	4syl 20	. . . . . . . . . 10 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ⊆ 𝐽)
49	48	unssbd 4195	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⊆ 𝐽)
50		breq2 5110	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (𝑟 ≤ 𝑧 ↔ 𝑟 ≤ 𝑦))
51	50	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (¬ 𝑟 ≤ 𝑧 ↔ ¬ 𝑟 ≤ 𝑦))
52	51	cbvrabv 3426	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦}
53		breq1 5109	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → (𝑥 ≤ 𝑦 ↔ 𝑟 ≤ 𝑦))
54	53	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → (¬ 𝑥 ≤ 𝑦 ↔ ¬ 𝑟 ≤ 𝑦))
55	54	rabbidv 3423	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑟 → {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦})
56	55	rspceeqv 3602	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝐵 ∧ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦}) → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
57	52, 56	mpan2 704	. . . . . . . . . . 11 ⊢ (𝑟 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
58	29	rabex 5304	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ V
59		eqid 2763	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
60	59	elrnmpt 5945	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ V → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
61	58, 60	ax-mp 5	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
62	57, 61	sylibr 237	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝐵 → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
63	62	adantl 487	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
64	49, 63	sseldd 3914	. . . . . . . 8 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ 𝐽)
65	64	ad2antrr 739	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ 𝐽)
66	48	unssad 4194	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ⊆ 𝐽)
67		breq1 5109	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (𝑧 ≤ 𝑟 ↔ 𝑦 ≤ 𝑟))
68	67	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (¬ 𝑧 ≤ 𝑟 ↔ ¬ 𝑦 ≤ 𝑟))
69	68	cbvrabv 3426	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟}
70		breq2 5110	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 𝑟))
71	70	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → (¬ 𝑦 ≤ 𝑥 ↔ ¬ 𝑦 ≤ 𝑟))
72	71	rabbidv 3423	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑟 → {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟})
73	72	rspceeqv 3602	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝐵 ∧ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟}) → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
74	69, 73	mpan2 704	. . . . . . . . . . 11 ⊢ (𝑟 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
75	29	rabex 5304	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ V
76		eqid 2763	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
77	76	elrnmpt 5945	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ V → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}))
78	75, 77	ax-mp 5	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
79	74, 78	sylibr 237	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝐵 → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}))
80	79	adantl 487	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}))
81	66, 80	sseldd 3914	. . . . . . . 8 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ 𝐽)
82	81	ad2antrr 739	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ 𝐽)
83		simpll 779	. . . . . . . . 9 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵))
84		simpr 490	. . . . . . . . 9 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
85	83, 84	jca 521	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴))
86		simplrl 789	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥)
87		ssel 3907	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
88	87	ancrd 561	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)))
89	88	anim1d 623	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥)))
90	89	impl 461	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥))
91		elin 4096	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ↔ (𝑥 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑥 ∈ 𝐴))
92		breq2 5110	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑥 → (𝑟 ≤ 𝑧 ↔ 𝑟 ≤ 𝑥))
93	92	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑥 → (¬ 𝑟 ≤ 𝑧 ↔ ¬ 𝑟 ≤ 𝑥))
94	93	elrab 3648	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥))
95	94	anbi1i 636	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑥 ∈ 𝐴) ↔ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥) ∧ 𝑥 ∈ 𝐴))
96		an32 659	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥) ∧ 𝑥 ∈ 𝐴) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥))
97	91, 95, 96	3bitri 300	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥))
98	90, 97	sylibr 237	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → 𝑥 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴))
99	98	ne0d 4291	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
100	25, 99	sylanl1 693	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
101	100	r19.29an 3170	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ ∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
102	85, 86, 101	syl2anc 596	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
103		simplrr 790	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)
104		ssel 3907	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
105	104	ancrd 561	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)))
106	105	anim1d 623	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 → ((𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑟) → ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟)))
107	106	impl 461	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟))
108		elin 4096	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ↔ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∧ 𝑦 ∈ 𝐴))
109	68	elrab 3648	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ↔ (𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟))
110	109	anbi1i 636	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∧ 𝑦 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟) ∧ 𝑦 ∈ 𝐴))
111		an32 659	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟) ∧ 𝑦 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟))
112	108, 110, 111	3bitri 300	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟))
113	107, 112	sylibr 237	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → 𝑦 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴))
114	113	ne0d 4291	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
115	25, 114	sylanl1 693	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
116	115	r19.29an 3170	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
117	85, 103, 116	syl2anc 596	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
118	17, 10	trleile 33588	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑟 ≤ 𝑧 ∨ 𝑧 ≤ 𝑟))
119		oran 1005	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ≤ 𝑧 ∨ 𝑧 ≤ 𝑟) ↔ ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
120	118, 119	sylib 221	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
121	120	3expa 1136	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
122	121	nrexdv 3161	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) → ¬ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
123		rabid 3436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧))
124		rabid 3436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟))
125	123, 124	anbi12i 640	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
126		elin 4096	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
127		anandi 689	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
128	125, 126, 127	3bitr4i 306	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ (𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
129	128	exbii 1880	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ ∃𝑧(𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
130		nfrab1 3435	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧{𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧}
131		nfrab1 3435	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧{𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}
132	130, 131	nfin 4124	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟})
133	132	n0f 4299	. . . . . . . . . . . . . . 15 ⊢ (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
134		df-rex 3091	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟) ↔ ∃𝑧(𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
135	129, 133, 134	3bitr4i 306	. . . . . . . . . . . . . 14 ⊢ (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ≠ ∅ ↔ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
136	135	necon1bbii 3008	. . . . . . . . . . . . 13 ⊢ (¬ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟) ↔ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
137	122, 136	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
138	137	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
139	138	adantr 486	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
140	139	ineq1d 4119	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = (∅ ∩ 𝐴))
141		0in 4350	. . . . . . . . 9 ⊢ (∅ ∩ 𝐴) = ∅
142	140, 141	eqtrdi 2814	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = ∅)
143	142	adantlr 728	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = ∅)
144		simplr 781	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐵)
145		simpr 490	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
146		vex 3458	. . . . . . . . . . . . . . 15 ⊢ 𝑟 ∈ V
147	146	snss 4745	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ 𝐵 ↔ {𝑟} ⊆ 𝐵)
148		eldif 4052	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ (𝐵 ∖ 𝐴) ↔ (𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴))
149	146	snss 4745	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ (𝐵 ∖ 𝐴) ↔ {𝑟} ⊆ (𝐵 ∖ 𝐴))
150	148, 149	bitr3i 280	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ {𝑟} ⊆ (𝐵 ∖ 𝐴))
151		ssconb 4081	. . . . . . . . . . . . . . 15 ⊢ (({𝑟} ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐵) → ({𝑟} ⊆ (𝐵 ∖ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
152	150, 151	bitrid 286	. . . . . . . . . . . . . 14 ⊢ (({𝑟} ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐵) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
153	147, 152	sylanb 593	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐵) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
154	153	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Toset ∧ (𝑟 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐵)) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
155	154	anass1rs 668	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
156	155	adantr 486	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
157	144, 145, 156	mpbi2and 725	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ (𝐵 ∖ {𝑟}))
158	7	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐾 ∈ Poset)
159		nfv 1948	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵)
160	130, 131	nfun 4172	. . . . . . . . . . 11 ⊢ Ⅎ𝑧({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟})
161		nfcv 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝐵 ∖ {𝑟})
162		ianor 997	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟))
163	17, 10	posrasymb 33584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ 𝑟 = 𝑧))
164		equcom 2052	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑧 ↔ 𝑧 = 𝑟)
165	163, 164	bitrdi 290	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ 𝑧 = 𝑟))
166	165	necon3bbid 2996	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (¬ (𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ 𝑧 ≠ 𝑟))
167	162, 166	bitr3id 288	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟) ↔ 𝑧 ≠ 𝑟))
168	167	3expia 1139	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → (𝑧 ∈ 𝐵 → ((¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟) ↔ 𝑧 ≠ 𝑟)))
169	168	pm5.32d 588	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟)) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟)))
170	123, 124	orbi12i 928	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∨ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∨ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
171		elun 4155	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∨ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
172		andi 1025	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟)) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∨ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
173	170, 171, 172	3bitr4ri 307	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟)) ↔ 𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
174		eldifsn 4748	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐵 ∖ {𝑟}) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟))
175	174	bicomi 227	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟}))
176	169, 173, 175	3bitr3g 316	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟})))
177	159, 160, 161, 176	eqrd 3932	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = (𝐵 ∖ {𝑟}))
178	158, 144, 177	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = (𝐵 ∖ {𝑟}))
179	157, 178	sseqtrrd 3950	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
180	179	adantlr 728	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
181	24, 26, 65, 82, 102, 117, 143, 180	nconnsubb 23756	. . . . . 6 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
182	181	anasss 472	. . . . 5 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
183	182	adantllr 732	. . . 4 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐵) ∧ ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
184		rexanali 3120	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
185	184	rexbii 3113	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑦 ∈ 𝐴 ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
186		rexcom 3295	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
187		rexnal 3118	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
188	185, 186, 187	3bitr3i 304	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
189	188	rexbii 3113	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑥 ∈ 𝐴 ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
190		rexcom 3295	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
191		rexnal 3118	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
192	189, 190, 191	3bitr3i 304	. . . . . . 7 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
193		r19.41v 3196	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
194	193	rexbii 3113	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
195		r19.41v 3196	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
196		reeanv 3238	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ↔ (∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦))
197	196	anbi1i 636	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
198	194, 195, 197	3bitri 300	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
199	198	rexbii 3113	. . . . . . 7 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
200	192, 199	bitr3i 280	. . . . . 6 ⊢ (¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
201	27	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐾 ∈ Toset)
202	25	sselda 3913	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)
203		simpllr 788	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑟 ∈ 𝐵)
204	17, 10	trleile 33588	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥))
205	201, 202, 203, 204	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥))
206		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
207		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
208		nelne2 3057	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑟 ∈ 𝐴) → 𝑥 ≠ 𝑟)
209	206, 207, 208	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ 𝑟)
210	158	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐾 ∈ Poset)
211	17, 10	posrasymb 33584	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥) ↔ 𝑥 = 𝑟))
212	211	necon3bbid 2996	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥) ↔ 𝑥 ≠ 𝑟))
213	210, 202, 203, 212	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥) ↔ 𝑥 ≠ 𝑟))
214	209, 213	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → ¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥))
215	205, 214	jca 521	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥) ∧ ¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥)))
216		pm5.17 1029	. . . . . . . . . . . 12 ⊢ (((𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥) ∧ ¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥)) ↔ (𝑥 ≤ 𝑟 ↔ ¬ 𝑟 ≤ 𝑥))
217	215, 216	sylib 221	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≤ 𝑟 ↔ ¬ 𝑟 ≤ 𝑥))
218	217	rexbidva 3188	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ↔ ∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥))
219	27	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ Toset)
220		simpllr 788	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑟 ∈ 𝐵)
221	25	sselda 3913	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐵)
222	17, 10	trleile 33588	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟))
223	219, 220, 221, 222	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟))
224		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
225		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
226		nelne2 3057	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐴 ∧ ¬ 𝑟 ∈ 𝐴) → 𝑦 ≠ 𝑟)
227	224, 225, 226	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ≠ 𝑟)
228	227	necomd 3014	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑟 ≠ 𝑦)
229	158	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ Poset)
230	17, 10	posrasymb 33584	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟) ↔ 𝑟 = 𝑦))
231	230	necon3bbid 2996	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟) ↔ 𝑟 ≠ 𝑦))
232	229, 220, 221, 231	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟) ↔ 𝑟 ≠ 𝑦))
233	228, 232	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟))
234	223, 233	jca 521	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ((𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟) ∧ ¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟)))
235		pm5.17 1029	. . . . . . . . . . . 12 ⊢ (((𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟) ∧ ¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟)) ↔ (𝑟 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑟))
236	234, 235	sylib 221	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑟 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑟))
237	236	rexbidva 3188	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟))
238	218, 237	anbi12d 644	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ↔ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)))
239	238	ex 418	. . . . . . . 8 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → (¬ 𝑟 ∈ 𝐴 → ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ↔ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟))))
240	239	pm5.32rd 589	. . . . . . 7 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → (((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)))
241	240	rexbidva 3188	. . . . . 6 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → (∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)))
242	200, 241	bitrid 286	. . . . 5 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → (¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)))
243	242	biimpa 482	. . . 4 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)) → ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴))
244	6, 183, 243	r19.29af 3275	. . 3 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
245	244	ex 418	. 2 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → (¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) → ¬ (𝐽 ↾t 𝐴) ∈ Conn))
246	245	con4d 116	1 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Conn → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1569  ∃wex 1811   ∈ wcel 2146   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  {crab 3416  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092   ∪ cun 4152  ∅c0 4281  {csn 4588   class class class wbr 5106   ↦ cmpt 5189   × cxp 5653  dom cdm 5655  ran crn 5656  ‘cfv 6547  (class class class)co 7430  ficfi 9415  Basecbs 17402  lecple 17450   ↾_t crest 17606  topGenctg 17623  ordTopcordt 17686   Proset cproset 18481  Posetcpo 18496  Tosetctos 18603  TopOnctopon 23243  Conncconn 23744

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7888  df-1st 8011  df-2nd 8012  df-1o 8490  df-2o 8491  df-en 8988  df-fin 8991  df-fi 9416  df-rest 17608  df-topgen 17629  df-ordt 17688  df-proset 18483  df-poset 18502  df-toset 18604  df-top 23227  df-topon 23244  df-bases 23279  df-cld 23352  df-conn 23745

This theorem is used by: (None)