Theorem ordtconlem1 29298

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

Hypotheses

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

Assertion

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

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

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

Proof of Theorem ordtconlem1

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1830	. . . . 5 ⊢ Ⅎ𝑟(𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵)
2		nfcv 2751	. . . . . . 7 ⊢ Ⅎ𝑟𝐴
3		nfra2 2930	. . . . . . 7 ⊢ Ⅎ𝑟∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
4	2, 3	nfral 2929	. . . . . 6 ⊢ Ⅎ𝑟∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
5	4	nfn 1768	. . . . 5 ⊢ Ⅎ𝑟 ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)
6	1, 5	nfan 1816	. . . 4 ⊢ Ⅎ𝑟((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
7		tospos 28989	. . . . . . . . . 10 ⊢ (𝐾 ∈ Toset → 𝐾 ∈ Poset)
8		posprs 16772	. . . . . . . . . 10 ⊢ (𝐾 ∈ Poset → 𝐾 ∈ Preset )
9		ordtcon.j	. . . . . . . . . . 11 ⊢ 𝐽 = (ordTop‘ ≤ )
10		ordtcon.l	. . . . . . . . . . . . . 14 ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))
11		fvex 6113	. . . . . . . . . . . . . . 15 ⊢ (le‘𝐾) ∈ V
12	11	inex1 4727	. . . . . . . . . . . . . 14 ⊢ ((le‘𝐾) ∩ (𝐵 × 𝐵)) ∈ V
13	10, 12	eqeltri 2684	. . . . . . . . . . . . 13 ⊢ ≤ ∈ V
14		eqid 2610	. . . . . . . . . . . . . 14 ⊢ dom ≤ = dom ≤
15	14	ordttopon 20807	. . . . . . . . . . . . 13 ⊢ ( ≤ ∈ V → (ordTop‘ ≤ ) ∈ (TopOn‘dom ≤ ))
16	13, 15	ax-mp 5	. . . . . . . . . . . 12 ⊢ (ordTop‘ ≤ ) ∈ (TopOn‘dom ≤ )
17		ordtcon.x	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝐾)
18	17, 10	prsdm 29288	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Preset → dom ≤ = 𝐵)
19	18	fveq2d 6107	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Preset → (TopOn‘dom ≤ ) = (TopOn‘𝐵))
20	16, 19	syl5eleq 2694	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Preset → (ordTop‘ ≤ ) ∈ (TopOn‘𝐵))
21	9, 20	syl5eqel 2692	. . . . . . . . . 10 ⊢ (𝐾 ∈ Preset → 𝐽 ∈ (TopOn‘𝐵))
22	7, 8, 21	3syl 18	. . . . . . . . 9 ⊢ (𝐾 ∈ Toset → 𝐽 ∈ (TopOn‘𝐵))
23	22	ad3antrrr 762	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐽 ∈ (TopOn‘𝐵))
24	23	adantlr 747	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐽 ∈ (TopOn‘𝐵))
25		simpllr 795	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ 𝐵)
26	25	adantlr 747	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ 𝐵)
27		simpll 786	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → 𝐾 ∈ Toset)
28	27, 7, 8	3syl 18	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → 𝐾 ∈ Preset )
29		snex 4835	. . . . . . . . . . . . . . . 16 ⊢ {𝐵} ∈ V
30		fvex 6113	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Base‘𝐾) ∈ V
31	17, 30	eqeltri 2684	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐵 ∈ V
32	31	mptex 6390	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∈ V
33	32	rnex 6992	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∈ V
34	31	mptex 6390	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ∈ V
35	34	rnex 6992	. . . . . . . . . . . . . . . . 17 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ∈ V
36	33, 35	unex 6854	. . . . . . . . . . . . . . . 16 ⊢ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ∈ V
37	29, 36	unex 6854	. . . . . . . . . . . . . . 15 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ∈ V
38		ssfii 8208	. . . . . . . . . . . . . . 15 ⊢ (({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ∈ V → ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))))
39	37, 38	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))
40		fvex 6113	. . . . . . . . . . . . . . 15 ⊢ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))) ∈ V
41		bastg 20581	. . . . . . . . . . . . . . 15 ⊢ ((fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))) ∈ V → (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))))
42	40, 41	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))))
43	39, 42	sstri 3577	. . . . . . . . . . . . 13 ⊢ ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})))))
44		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
45		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
46	17, 10, 44, 45	ordtprsval 29292	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ Preset → (ordTop‘ ≤ ) = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))))
47	9, 46	syl5eq 2656	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ Preset → 𝐽 = (topGen‘(fi‘({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))))))
48	43, 47	syl5sseqr 3617	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ Preset → ({𝐵} ∪ (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))) ⊆ 𝐽)
49	48	unssbd 3753	. . . . . . . . . . 11 ⊢ (𝐾 ∈ Preset → (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ⊆ 𝐽)
50	28, 49	syl 17	. . . . . . . . . 10 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → (ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ∪ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})) ⊆ 𝐽)
51	50	unssbd 3753	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⊆ 𝐽)
52		breq2 4587	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (𝑟 ≤ 𝑧 ↔ 𝑟 ≤ 𝑦))
53	52	notbid 307	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (¬ 𝑟 ≤ 𝑧 ↔ ¬ 𝑟 ≤ 𝑦))
54	53	cbvrabv 3172	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦}
55		breq1 4586	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑟 → (𝑥 ≤ 𝑦 ↔ 𝑟 ≤ 𝑦))
56	55	notbid 307	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → (¬ 𝑥 ≤ 𝑦 ↔ ¬ 𝑟 ≤ 𝑦))
57	56	rabbidv 3164	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦})
58	57	eqeq2d 2620	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑟 → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦} ↔ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦}))
59	58	rspcev 3282	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝐵 ∧ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑦}) → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
60	54, 59	mpan2 703	. . . . . . . . . . 11 ⊢ (𝑟 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
61	31	rabex 4740	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ V
62		eqid 2610	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
63	62	elrnmpt 5293	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ V → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
64	61, 63	ax-mp 5	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})
65	60, 64	sylibr 223	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝐵 → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
66	65	adantl 481	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}))
67	51, 66	sseldd 3569	. . . . . . . 8 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ 𝐽)
68	67	ad2antrr 758	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∈ 𝐽)
69	50	unssad 3752	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ⊆ 𝐽)
70		breq1 4586	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑦 → (𝑧 ≤ 𝑟 ↔ 𝑦 ≤ 𝑟))
71	70	notbid 307	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (¬ 𝑧 ≤ 𝑟 ↔ ¬ 𝑦 ≤ 𝑟))
72	71	cbvrabv 3172	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟}
73		breq2 4587	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑟 → (𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 𝑟))
74	73	notbid 307	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑟 → (¬ 𝑦 ≤ 𝑥 ↔ ¬ 𝑦 ≤ 𝑟))
75	74	rabbidv 3164	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑟 → {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟})
76	75	eqeq2d 2620	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑟 → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥} ↔ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟}))
77	76	rspcev 3282	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ 𝐵 ∧ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑟}) → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
78	72, 77	mpan2 703	. . . . . . . . . . 11 ⊢ (𝑟 ∈ 𝐵 → ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
79	31	rabex 4740	. . . . . . . . . . . 12 ⊢ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ V
80		eqid 2610	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) = (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
81	80	elrnmpt 5293	. . . . . . . . . . . 12 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ V → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}))
82	79, 81	ax-mp 5	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) ↔ ∃𝑥 ∈ 𝐵 {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} = {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})
83	78, 82	sylibr 223	. . . . . . . . . 10 ⊢ (𝑟 ∈ 𝐵 → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}))
84	83	adantl 481	. . . . . . . . 9 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}))
85	69, 84	sseldd 3569	. . . . . . . 8 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ 𝐽)
86	85	ad2antrr 758	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∈ 𝐽)
87		simpll 786	. . . . . . . . 9 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵))
88		simpr 476	. . . . . . . . 9 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
89	87, 88	jca 553	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴))
90		simplrl 796	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥)
91		ssel 3562	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
92	91	ancrd 575	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)))
93	92	anim1d 586	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥)))
94	93	impl 648	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥))
95		elin 3758	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ↔ (𝑥 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑥 ∈ 𝐴))
96		breq2 4587	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑥 → (𝑟 ≤ 𝑧 ↔ 𝑟 ≤ 𝑥))
97	96	notbid 307	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑥 → (¬ 𝑟 ≤ 𝑧 ↔ ¬ 𝑟 ≤ 𝑥))
98	97	elrab 3331	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥))
99	98	anbi1i 727	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑥 ∈ 𝐴) ↔ ((𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥) ∧ 𝑥 ∈ 𝐴))
100		an32 835	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑥) ∧ 𝑥 ∈ 𝐴) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥))
101	95, 99, 100	3bitri 285	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥))
102	94, 101	sylibr 223	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → 𝑥 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴))
103		ne0i 3880	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
104	102, 103	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
105	25, 104	sylanl1 680	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
106	105	r19.29an 3059	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ ∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
107	89, 90, 106	syl2anc 691	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ 𝐴) ≠ ∅)
108		simplrr 797	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)
109		ssel 3562	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
110	109	ancrd 575	. . . . . . . . . . . . . 14 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → (𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)))
111	110	anim1d 586	. . . . . . . . . . . . 13 ⊢ (𝐴 ⊆ 𝐵 → ((𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ≤ 𝑟) → ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟)))
112	111	impl 648	. . . . . . . . . . . 12 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟))
113		elin 3758	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ↔ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∧ 𝑦 ∈ 𝐴))
114	71	elrab 3331	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ↔ (𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟))
115	114	anbi1i 727	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∧ 𝑦 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟) ∧ 𝑦 ∈ 𝐴))
116		an32 835	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ≤ 𝑟) ∧ 𝑦 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟))
117	113, 115, 116	3bitri 285	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟))
118	112, 117	sylibr 223	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → 𝑦 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴))
119		ne0i 3880	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
120	118, 119	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ 𝐵 ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
121	25, 120	sylanl1 680	. . . . . . . . 9 ⊢ ((((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
122	121	r19.29an 3059	. . . . . . . 8 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
123	89, 108, 122	syl2anc 691	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ∩ 𝐴) ≠ ∅)
124	17, 10	trleile 28997	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑟 ≤ 𝑧 ∨ 𝑧 ≤ 𝑟))
125		oran 516	. . . . . . . . . . . . . . . 16 ⊢ ((𝑟 ≤ 𝑧 ∨ 𝑧 ≤ 𝑟) ↔ ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
126	124, 125	sylib 207	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
127	126	3expa 1257	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ¬ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
128	127	nrexdv 2984	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) → ¬ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
129		rabid 3095	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧))
130		rabid 3095	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟} ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟))
131	129, 130	anbi12i 729	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
132		elin 3758	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∧ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
133		anandi 867	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
134	131, 132, 133	3bitr4i 291	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ (𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
135	134	exbii 1764	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ ∃𝑧(𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
136		nfrab1 3099	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧{𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧}
137		nfrab1 3099	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑧{𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}
138	136, 137	nfin 3782	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟})
139	138	n0f 3886	. . . . . . . . . . . . . . 15 ⊢ (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
140		df-rex 2902	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟) ↔ ∃𝑧(𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟)))
141	135, 139, 140	3bitr4i 291	. . . . . . . . . . . . . 14 ⊢ (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ≠ ∅ ↔ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟))
142	141	necon1bbii 2831	. . . . . . . . . . . . 13 ⊢ (¬ ∃𝑧 ∈ 𝐵 (¬ 𝑟 ≤ 𝑧 ∧ ¬ 𝑧 ≤ 𝑟) ↔ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
143	128, 142	sylib 207	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
144	143	adantlr 747	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
145	144	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = ∅)
146	145	ineq1d 3775	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = (∅ ∩ 𝐴))
147		0in 3921	. . . . . . . . 9 ⊢ (∅ ∩ 𝐴) = ∅
148	146, 147	syl6eq 2660	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = ∅)
149	148	adantlr 747	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → (({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∩ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ∩ 𝐴) = ∅)
150		simplr 788	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐵)
151		simpr 476	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
152		vex 3176	. . . . . . . . . . . . . . 15 ⊢ 𝑟 ∈ V
153	152	snss 4259	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ 𝐵 ↔ {𝑟} ⊆ 𝐵)
154		eldif 3550	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ (𝐵 ∖ 𝐴) ↔ (𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴))
155	152	snss 4259	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ (𝐵 ∖ 𝐴) ↔ {𝑟} ⊆ (𝐵 ∖ 𝐴))
156	154, 155	bitr3i 265	. . . . . . . . . . . . . . 15 ⊢ ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ {𝑟} ⊆ (𝐵 ∖ 𝐴))
157		ssconb 3705	. . . . . . . . . . . . . . 15 ⊢ (({𝑟} ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐵) → ({𝑟} ⊆ (𝐵 ∖ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
158	156, 157	syl5bb 271	. . . . . . . . . . . . . 14 ⊢ (({𝑟} ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐵) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
159	153, 158	sylanb 488	. . . . . . . . . . . . 13 ⊢ ((𝑟 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐵) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
160	159	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Toset ∧ (𝑟 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐵)) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
161	160	anass1rs 845	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
162	161	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ((𝑟 ∈ 𝐵 ∧ ¬ 𝑟 ∈ 𝐴) ↔ 𝐴 ⊆ (𝐵 ∖ {𝑟})))
163	150, 151, 162	mpbi2and 958	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ (𝐵 ∖ {𝑟}))
164	7	ad3antrrr 762	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐾 ∈ Poset)
165		nfv 1830	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵)
166	136, 137	nfun 3731	. . . . . . . . . . 11 ⊢ Ⅎ𝑧({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟})
167		nfcv 2751	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝐵 ∖ {𝑟})
168		ianor 508	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟))
169	17, 10	posrasymb 28988	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ 𝑟 = 𝑧))
170		equcom 1932	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑧 ↔ 𝑧 = 𝑟)
171	169, 170	syl6bb 275	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ 𝑧 = 𝑟))
172	171	necon3bbid 2819	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (¬ (𝑟 ≤ 𝑧 ∧ 𝑧 ≤ 𝑟) ↔ 𝑧 ≠ 𝑟))
173	168, 172	syl5bbr 273	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟) ↔ 𝑧 ≠ 𝑟))
174	173	3expia 1259	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → (𝑧 ∈ 𝐵 → ((¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟) ↔ 𝑧 ≠ 𝑟)))
175	174	pm5.32d 669	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟)) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟)))
176	129, 130	orbi12i 542	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∨ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∨ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
177		elun 3715	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ (𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∨ 𝑧 ∈ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
178		andi 907	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟)) ↔ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑟 ≤ 𝑧) ∨ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ≤ 𝑟)))
179	176, 177, 178	3bitr4ri 292	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑟 ≤ 𝑧 ∨ ¬ 𝑧 ≤ 𝑟)) ↔ 𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
180		eldifsn 4260	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ (𝐵 ∖ {𝑟}) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟))
181	180	bicomi 213	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 𝑟) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟}))
182	175, 179, 181	3bitr3g 301	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → (𝑧 ∈ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) ↔ 𝑧 ∈ (𝐵 ∖ {𝑟})))
183	165, 166, 167, 182	eqrd 3586	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = (𝐵 ∖ {𝑟}))
184	164, 150, 183	syl2anc 691	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}) = (𝐵 ∖ {𝑟}))
185	163, 184	sseqtr4d 3605	. . . . . . . 8 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
186	185	adantlr 747	. . . . . . 7 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → 𝐴 ⊆ ({𝑧 ∈ 𝐵 ∣ ¬ 𝑟 ≤ 𝑧} ∪ {𝑧 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑟}))
187	24, 26, 68, 86, 107, 123, 149, 186	nconsubb 21036	. . . . . 6 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)) ∧ ¬ 𝑟 ∈ 𝐴) → ¬ (𝐽 ↾t 𝐴) ∈ Con)
188	187	anasss 677	. . . . 5 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)) → ¬ (𝐽 ↾t 𝐴) ∈ Con)
189	188	adantllr 751	. . . 4 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐵) ∧ ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)) → ¬ (𝐽 ↾t 𝐴) ∈ Con)
190		rexanali 2981	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
191	190	rexbii 3023	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑦 ∈ 𝐴 ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
192		rexcom 3080	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
193		rexnal 2978	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ¬ ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
194	191, 192, 193	3bitr3i 289	. . . . . . . . 9 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
195	194	rexbii 3023	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑥 ∈ 𝐴 ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
196		rexcom 3080	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑟 ∈ 𝐵 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
197		rexnal 2978	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ¬ ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
198	195, 196, 197	3bitr3i 289	. . . . . . 7 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))
199		r19.41v 3070	. . . . . . . . . 10 ⊢ (∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
200	199	rexbii 3023	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
201		r19.41v 3070	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
202		reeanv 3086	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ↔ (∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦))
203	202	anbi1i 727	. . . . . . . . 9 ⊢ ((∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
204	200, 201, 203	3bitri 285	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
205	204	rexbii 3023	. . . . . . 7 ⊢ (∃𝑟 ∈ 𝐵 ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
206	198, 205	bitr3i 265	. . . . . 6 ⊢ (¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴))
207	27	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐾 ∈ Toset)
208	25	sselda 3568	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐵)
209		simpllr 795	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑟 ∈ 𝐵)
210	17, 10	trleile 28997	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Toset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥))
211	207, 208, 209, 210	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥))
212		simpr 476	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
213		simplr 788	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
214		nelne2 2879	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑟 ∈ 𝐴) → 𝑥 ≠ 𝑟)
215	212, 213, 214	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≠ 𝑟)
216	164	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝐾 ∈ Poset)
217	17, 10	posrasymb 28988	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥) ↔ 𝑥 = 𝑟))
218	217	necon3bbid 2819	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥) ↔ 𝑥 ≠ 𝑟))
219	216, 208, 209, 218	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥) ↔ 𝑥 ≠ 𝑟))
220	215, 219	mpbird 246	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → ¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥))
221	211, 220	jca 553	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥) ∧ ¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥)))
222		pm5.17 928	. . . . . . . . . . . 12 ⊢ (((𝑥 ≤ 𝑟 ∨ 𝑟 ≤ 𝑥) ∧ ¬ (𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑥)) ↔ (𝑥 ≤ 𝑟 ↔ ¬ 𝑟 ≤ 𝑥))
223	221, 222	sylib 207	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≤ 𝑟 ↔ ¬ 𝑟 ≤ 𝑥))
224	223	rexbidva 3031	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ↔ ∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥))
225	27	ad2antrr 758	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ Toset)
226		simpllr 795	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑟 ∈ 𝐵)
227	25	sselda 3568	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐵)
228	17, 10	trleile 28997	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Toset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟))
229	225, 226, 227, 228	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟))
230		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
231		simplr 788	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ¬ 𝑟 ∈ 𝐴)
232		nelne2 2879	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ 𝐴 ∧ ¬ 𝑟 ∈ 𝐴) → 𝑦 ≠ 𝑟)
233	230, 231, 232	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ≠ 𝑟)
234	233	necomd 2837	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑟 ≠ 𝑦)
235	164	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝐾 ∈ Poset)
236	17, 10	posrasymb 28988	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟) ↔ 𝑟 = 𝑦))
237	236	necon3bbid 2819	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ 𝑟 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟) ↔ 𝑟 ≠ 𝑦))
238	235, 226, 227, 237	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟) ↔ 𝑟 ≠ 𝑦))
239	234, 238	mpbird 246	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟))
240	229, 239	jca 553	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ((𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟) ∧ ¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟)))
241		pm5.17 928	. . . . . . . . . . . 12 ⊢ (((𝑟 ≤ 𝑦 ∨ 𝑦 ≤ 𝑟) ∧ ¬ (𝑟 ≤ 𝑦 ∧ 𝑦 ≤ 𝑟)) ↔ (𝑟 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑟))
242	240, 241	sylib 207	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑟 ≤ 𝑦 ↔ ¬ 𝑦 ≤ 𝑟))
243	242	rexbidva 3031	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟))
244	224, 243	anbi12d 743	. . . . . . . . 9 ⊢ ((((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) ∧ ¬ 𝑟 ∈ 𝐴) → ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ↔ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟)))
245	244	ex 449	. . . . . . . 8 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → (¬ 𝑟 ∈ 𝐴 → ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ↔ (∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟))))
246	245	pm5.32rd 670	. . . . . . 7 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑟 ∈ 𝐵) → (((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)))
247	246	rexbidva 3031	. . . . . 6 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → (∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 𝑥 ≤ 𝑟 ∧ ∃𝑦 ∈ 𝐴 𝑟 ≤ 𝑦) ∧ ¬ 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)))
248	206, 247	syl5bb 271	. . . . 5 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → (¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) ↔ ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴)))
249	248	biimpa 500	. . . 4 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)) → ∃𝑟 ∈ 𝐵 ((∃𝑥 ∈ 𝐴 ¬ 𝑟 ≤ 𝑥 ∧ ∃𝑦 ∈ 𝐴 ¬ 𝑦 ≤ 𝑟) ∧ ¬ 𝑟 ∈ 𝐴))
250	6, 189, 249	r19.29af 3058	. . 3 ⊢ (((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) ∧ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)) → ¬ (𝐽 ↾t 𝐴) ∈ Con)
251	250	ex 449	. 2 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → (¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴) → ¬ (𝐽 ↾t 𝐴) ∈ Con))
252	251	con4d 113	1 ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Con → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  {csn 4125   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  dom cdm 5038  ran crn 5039  ‘cfv 5804  (class class class)co 6549  ficfi 8199  Basecbs 15695  lecple 15775   ↾_t crest 15904  topGenctg 15921  ordTopcordt 15982   Preset cpreset 16749  Posetcpo 16763  Tosetctos 16856  TopOnctopon 20518  Conccon 21024

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-fin 7845  df-fi 8200  df-rest 15906  df-topgen 15927  df-ordt 15984  df-preset 16751  df-poset 16769  df-toset 16857  df-top 20521  df-bases 20522  df-topon 20523  df-cld 20633  df-con 21025

This theorem is referenced by: (None)