Theorem ordtconnlem1 34556

Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 34557. See also reconnlem1 25146. (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 1947	. . . . 5 ⊢ Ⅎ𝑟(𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵)
2		nfcv 2923	. . . . . . 7 ⊢ Ⅎ𝑟𝐴
3		nfra2w 3299	. . . . . . 7 ⊢ Ⅎ𝑟∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
4	2, 3	nfralw 3310	. . . . . 6 ⊢ Ⅎ𝑟∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
5	4	nfn 1890	. . . . 5 ⊢ Ⅎ𝑟 ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
6	1, 5	nfan 1932	. . . 4 ⊢ Ⅎ𝑟((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
7		tospos 18592	. . . . . . . . . 10 ⊢ (𝐾 ∈ Toset → 𝐾 ∈ Poset)
8		posprs 18490	. . . . . . . . . 10 ⊢ (𝐾 ∈ Poset → 𝐾 ∈ Proset )
9		ordtconn.j	. . . . . . . . . . 11 ⊢ 𝐽 = (ordTop‘ ≤ )
10		ordtconn.l	. . . . . . . . . . . . . 14 ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))
11		fvex 6898	. . . . . . . . . . . . . . 15 ⊢ (le‘𝐾) ∈ V
12	11	inex1 5277	. . . . . . . . . . . . . 14 ⊢ ((le‘𝐾) ∩ (𝐵 × 𝐵)) ∈ V
13	10, 12	eqeltri 2857	. . . . . . . . . . . . 13 ⊢ ≤ ∈ V
14		eqid 2761	. . . . . . . . . . . . . 14 ⊢ dom ≤ = dom ≤
15	14	ordttopon 23511	. . . . . . . . . . . . 13 ⊢ ( ≤ ∈ V → (ordTop‘ ≤ ) ∈ (TopOn‘dom ≤ ))
16	13, 15	ax-mp 5	. . . . . . . . . . . 12 ⊢ (ordTop‘ ≤ ) ∈ (TopOn‘dom ≤ )
17		ordtconn.x	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝐾)
18	17, 10	prsdm 34546	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵)
19	18	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Proset → (TopOn‘dom ≤ ) = (TopOn‘𝐵))
20	16, 19	eleqtrid 2867	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Proset → (ordTop‘ ≤ ) ∈ (TopOn‘𝐵))
21	9, 20	eqeltrid 2865	. . . . . . . . . 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 5397	. . . . . . . . . . . . . . . 16 ⊢ {𝐵} ∈ V
29	17	fvexi 6899	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 ∈ V
30	29	mptex 7229	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∈ V
31	30	rnex 7922	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∈ V
32	29	mptex 7229	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ∈ V
33	32	rnex 7922	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ∈ V
34	31, 33	unex 7761	. . . . . . . . . . . . . . . 16 ⊢ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ∈ V
35	28, 34	unex 7761	. . . . . . . . . . . . . . 15 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ∈ V
36		ssfii 9411	. . . . . . . . . . . . . . 15 ⊢ (({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ∈ V → ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))))
37	35, 36	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))
38		fvex 6898	. . . . . . . . . . . . . . 15 ⊢ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))) ∈ V
39		bastg 23284	. . . . . . . . . . . . . . 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 3940	. . . . . . . . . . . . 13 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))))
42		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
43		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
44	17, 10, 42, 43	ordtprsval 34550	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ Proset → (ordTop‘ ≤ ) = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))))
45	9, 44	eqtrid 2808	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Proset → 𝐽 = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))))
46	41, 45	sseqtrrid 3974	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Proset → ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ 𝐽)
47	46	unssbd 4140	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Proset → (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ⊆ 𝐽)
48	27, 7, 8, 47	4syl 20	. . . . . . . . . 10 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ⊆ 𝐽)
49	48	unssbd 4140	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⊆ 𝐽)
50		breq2 5107	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (𝑟 ≤ 𝑧 ↔ 𝑟 ≤ 𝑦))
51	50	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (¬ 𝑟 ≤ 𝑧 ↔ ¬ 𝑟 ≤ 𝑦))
52	51	cbvrabv 3423	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦}
53		breq1 5106	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → (𝑥 ≤ 𝑦 ↔ 𝑟 ≤ 𝑦))
54	53	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → (¬ 𝑥 ≤ 𝑦 ↔ ¬ 𝑟 ≤ 𝑦))
55	54	rabbidv 3420	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑟 → {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦})
56	55	rspceeqv 3599	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝐵 ∧ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦}) → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
57	52, 56	mpan2 704	. . . . . . . . . . 11 ⊢ (𝑟 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
58	29	rabex 5300	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ V
59		eqid 2761	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
60	59	elrnmpt 5940	. . . . . . . . . . . 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 3932	. . . . . . . 8 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ 𝐽)
65	64	ad2antrr 739	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ 𝐽)
66	48	unssad 4139	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ⊆ 𝐽)
67		breq1 5106	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (𝑧 ≤ 𝑟 ↔ 𝑦 ≤ 𝑟))
68	67	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (¬ 𝑧 ≤ 𝑟 ↔ ¬ 𝑦 ≤ 𝑟))
69	68	cbvrabv 3423	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟}
70		breq2 5107	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 𝑟))
71	70	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → (¬ 𝑦 ≤ 𝑥 ↔ ¬ 𝑦 ≤ 𝑟))
72	71	rabbidv 3420	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑟 → {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟})
73	72	rspceeqv 3599	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝐵 ∧ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟}) → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
74	69, 73	mpan2 704	. . . . . . . . . . 11 ⊢ (𝑟 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
75	29	rabex 5300	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ V
76		eqid 2761	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
77	76	elrnmpt 5940	. . . . . . . . . . . 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 3932	. . . . . . . 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 3925	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
88	87	ancrd 561	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)))
89	88	anim1d 623	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥)))
90	89	impl 461	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥))
91		elin 3915	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ↔ (𝑥 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑥 ∈ 𝐴))
92		breq2 5107	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑥 → (𝑟 ≤ 𝑧 ↔ 𝑟 ≤ 𝑥))
93	92	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑥 → (¬ 𝑟 ≤ 𝑧 ↔ ¬ 𝑟 ≤ 𝑥))
94	93	elrab 3645	. . . . . . . . . . . . . 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 4288	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
100	25, 99	sylanl1 693	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
101	100	r19.29an 3167	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ ∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
102	85, 86, 101	syl2anc 596	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
103		simplrr 790	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)
104		ssel 3925	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
105	104	ancrd 561	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)))
106	105	anim1d 623	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 → ((𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑟) → ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟)))
107	106	impl 461	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟))
108		elin 3915	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ↔ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∧ 𝑦 ∈ 𝐴))
109	68	elrab 3645	. . . . . . . . . . . . . 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 4288	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
115	25, 114	sylanl1 693	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
116	115	r19.29an 3167	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
117	85, 103, 116	syl2anc 596	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
118	17, 10	trleile 33532	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑟 ≤ 𝑧 ∨ 𝑧 ≤ 𝑟))
119		oran 1005	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ≤ 𝑧 ∨ 𝑧 ≤ 𝑟) ↔ ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
120	118, 119	sylib 221	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
121	120	3expa 1136	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
122	121	nrexdv 3158	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) → ¬ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
123		rabid 3433	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧))
124		rabid 3433	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟))
125	123, 124	anbi12i 640	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
126		elin 3915	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
127		anandi 689	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
128	125, 126, 127	3bitr4i 306	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ (𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
129	128	exbii 1881	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ ∃𝑧(𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
130		nfrab1 3432	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧{𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧}
131		nfrab1 3432	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧{𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}
132	130, 131	nfin 4170	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟})
133	132	n0f 4296	. . . . . . . . . . . . . . 15 ⊢ (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
134		df-rex 3088	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟) ↔ ∃𝑧(𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
135	129, 133, 134	3bitr4i 306	. . . . . . . . . . . . . 14 ⊢ (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ≠ ∅ ↔ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
136	135	necon1bbii 3005	. . . . . . . . . . . . 13 ⊢ (¬ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟) ↔ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
137	122, 136	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
138	137	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
139	138	adantr 486	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
140	139	ineq1d 4165	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = (∅ ∩ 𝐴))
141		0in 4347	. . . . . . . . 9 ⊢ (∅ ∩ 𝐴) = ∅
142	140, 141	eqtrdi 2812	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = ∅)
143	142	adantlr 728	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = ∅)
144		simplr 781	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐵)
145		simpr 490	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
146		vex 3455	. . . . . . . . . . . . . . 15 ⊢ 𝑟 ∈ V
147	146	snss 4745	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ 𝐵 ↔ {𝑟} ⊆ 𝐵)
148		eldif 3909	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ (𝐵 ∖ 𝐴) ↔ (𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴))
149	146	snss 4745	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ (𝐵 ∖ 𝐴) ↔ {𝑟} ⊆ (𝐵 ∖ 𝐴))
150	148, 149	bitr3i 280	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ {𝑟} ⊆ (𝐵 ∖ 𝐴))
151		ssconb 4089	. . . . . . . . . . . . . . 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 1947	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵)
160	130, 131	nfun 4117	. . . . . . . . . . 11 ⊢ Ⅎ𝑧({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟})
161		nfcv 2923	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝐵 ∖ {𝑟})
162		ianor 997	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟))
163	17, 10	posrasymb 33528	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ 𝑟 = 𝑧))
164		equcom 2051	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑧 ↔ 𝑧 = 𝑟)
165	163, 164	bitrdi 290	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ 𝑧 = 𝑟))
166	165	necon3bbid 2993	. . . . . . . . . . . . . . 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 4100	. . . . . . . . . . . . 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 3950	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = (𝐵 ∖ {𝑟}))
178	158, 144, 177	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = (𝐵 ∖ {𝑟}))
179	157, 178	sseqtrrd 3968	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
180	179	adantlr 728	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
181	24, 26, 65, 82, 102, 117, 143, 180	nconnsubb 23741	. . . . . 6 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
182	181	anasss 472	. . . . 5 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
183	182	adantllr 732	. . . 4 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐵) ∧ ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)) → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
184		rexanali 3117	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
185	184	rexbii 3110	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑦 ∈ 𝐴 ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
186		rexcom 3292	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
187		rexnal 3115	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
188	185, 186, 187	3bitr3i 304	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
189	188	rexbii 3110	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑥 ∈ 𝐴 ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
190		rexcom 3292	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
191		rexnal 3115	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
192	189, 190, 191	3bitr3i 304	. . . . . . 7 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
193		r19.41v 3193	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
194	193	rexbii 3110	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
195		r19.41v 3193	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
196		reeanv 3235	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ↔ (∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦))
197	196	anbi1i 636	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
198	194, 195, 197	3bitri 300	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
199	198	rexbii 3110	. . . . . . 7 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
200	192, 199	bitr3i 280	. . . . . 6 ⊢ (¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
201	27	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐾 ∈ Toset)
202	25	sselda 3931	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)
203		simpllr 788	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑟 ∈ 𝐵)
204	17, 10	trleile 33532	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥))
205	201, 202, 203, 204	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥))
206		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
207		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
208		nelne2 3054	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑟 ∈ 𝐴) → 𝑥 ≠ 𝑟)
209	206, 207, 208	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ 𝑟)
210	158	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐾 ∈ Poset)
211	17, 10	posrasymb 33528	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥) ↔ 𝑥 = 𝑟))
212	211	necon3bbid 2993	. . . . . . . . . . . . . . 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 3185	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ↔ ∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥))
219	27	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ Toset)
220		simpllr 788	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑟 ∈ 𝐵)
221	25	sselda 3931	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐵)
222	17, 10	trleile 33532	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟))
223	219, 220, 221, 222	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟))
224		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
225		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
226		nelne2 3054	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐴 ∧ ¬ 𝑟 ∈ 𝐴) → 𝑦 ≠ 𝑟)
227	224, 225, 226	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ≠ 𝑟)
228	227	necomd 3011	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑟 ≠ 𝑦)
229	158	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ Poset)
230	17, 10	posrasymb 33528	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟) ↔ 𝑟 = 𝑦))
231	230	necon3bbid 2993	. . . . . . . . . . . . . . 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 3185	. . . . . . . . . 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 3185	. . . . . 6 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → (∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)))
242	200, 241	bitrid 286	. . . . 5 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → (¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)))
243	242	biimpa 482	. . . 4 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)) → ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴))
244	6, 183, 243	r19.29af 3272	. . 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 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  {crab 3413  Vcvv 3451   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  {csn 4584   class class class wbr 5103   ↦ cmpt 5186   × cxp 5649  dom cdm 5651  ran crn 5652  ‘cfv 6538  (class class class)co 7420  ficfi 9402  Basecbs 17387  lecple 17435   ↾_t crest 17591  topGenctg 17608  ordTopcordt 17671   Proset cproset 18466  Posetcpo 18481  Tosetctos 18588  TopOnctopon 23228  Conncconn 23729

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-1o 8476  df-2o 8477  df-en 8974  df-fin 8977  df-fi 9403  df-rest 17593  df-topgen 17614  df-ordt 17673  df-proset 18468  df-poset 18487  df-toset 18589  df-top 23212  df-topon 23229  df-bases 23264  df-cld 23337  df-conn 23730

This theorem is used by: (None)