rencldnfilem - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > rencldnfilem		Structured version Visualization version GIF version

Theorem rencldnfilem 42801

Description: Lemma for rencldnfi 42802. (Contributed by Stefan O'Rear, 18-Oct-2014.)

**Assertion**
Ref	Expression
rencldnfilem	⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥) → ¬ 𝐴 ∈ Fin)

Distinct variable groups: 𝑥,𝐴,𝑦 𝑥,𝐵,𝑦

Proof of Theorem rencldnfilem Dummy variables 𝑎 𝑏 𝑐 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq1 2734	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑎 = (abs‘(𝑏 − 𝐵)) ↔ 𝑐 = (abs‘(𝑏 − 𝐵))))
2	1	rexbidv 3158	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵)) ↔ ∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵))))
3	2	elrab 3661	. . . . . . . . . . 11 ⊢ (𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ↔ (𝑐 ∈ ℝ ∧ ∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵))))
4		simp-4l 782	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝐴 ⊆ ℝ)
5		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐴)
6	4, 5	sseldd 3949	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ℝ)
7	6	recnd 11208	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ℂ)
8		simp-4r 783	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝐵 ∈ ℝ)
9	8	recnd 11208	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝐵 ∈ ℂ)
10	7, 9	subcld 11539	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (𝑏 − 𝐵) ∈ ℂ)
11		simprr 772	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → ¬ 𝐵 ∈ 𝐴)
12	11	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → ¬ 𝐵 ∈ 𝐴)
13		nelneq 2853	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ 𝐴 ∧ ¬ 𝐵 ∈ 𝐴) → ¬ 𝑏 = 𝐵)
14	5, 12, 13	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → ¬ 𝑏 = 𝐵)
15		subeq0 11454	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑏 − 𝐵) = 0 ↔ 𝑏 = 𝐵))
16	15	necon3abid 2962	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑏 − 𝐵) ≠ 0 ↔ ¬ 𝑏 = 𝐵))
17	7, 9, 16	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → ((𝑏 − 𝐵) ≠ 0 ↔ ¬ 𝑏 = 𝐵))
18	14, 17	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (𝑏 − 𝐵) ≠ 0)
19	10, 18	absrpcld 15423	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (abs‘(𝑏 − 𝐵)) ∈ ℝ⁺)
20		eleq1 2817	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (abs‘(𝑏 − 𝐵)) → (𝑐 ∈ ℝ⁺ ↔ (abs‘(𝑏 − 𝐵)) ∈ ℝ⁺))
21	19, 20	syl5ibrcom 247	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (𝑐 = (abs‘(𝑏 − 𝐵)) → 𝑐 ∈ ℝ⁺))
22	21	rexlimdva 3135	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) → (∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵)) → 𝑐 ∈ ℝ⁺))
23	22	expimpd 453	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → ((𝑐 ∈ ℝ ∧ ∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵))) → 𝑐 ∈ ℝ⁺))
24	3, 23	biimtrid 242	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → (𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} → 𝑐 ∈ ℝ⁺))
25	24	ssrdv 3954	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ⁺)
26	25	adantr 480	. . . . . . . 8 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ⁺)
27		abrexfi 9309	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Fin → {𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
28		rabssab 4050	. . . . . . . . . . 11 ⊢ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ {𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}
29		ssfi 9142	. . . . . . . . . . 11 ⊢ (({𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ {𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
30	27, 28, 29	sylancl 586	. . . . . . . . . 10 ⊢ (𝐴 ∈ Fin → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
31	30	adantl 481	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
32		simplrl 776	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → 𝐴 ≠ ∅)
33		n0 4318	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐴)
34	32, 33	sylib 218	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑦 𝑦 ∈ 𝐴)
35		simp-4l 782	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝐴 ⊆ ℝ)
36		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
37	35, 36	sseldd 3949	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ)
38	37	recnd 11208	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ)
39		simp-4r 783	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ ℝ)
40	39	recnd 11208	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ ℂ)
41	38, 40	subcld 11539	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (𝑦 − 𝐵) ∈ ℂ)
42	41	abscld 15411	. . . . . . . . . . . 12 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (abs‘(𝑦 − 𝐵)) ∈ ℝ)
43		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (abs‘(𝑦 − 𝐵)) = (abs‘(𝑦 − 𝐵))
44		fvoveq1 7412	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑦 → (abs‘(𝑏 − 𝐵)) = (abs‘(𝑦 − 𝐵)))
45	44	rspceeqv 3614	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ (abs‘(𝑦 − 𝐵)) = (abs‘(𝑦 − 𝐵))) → ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
46	43, 45	mpan2 691	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 → ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
47	46	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
48		eqeq1 2734	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (abs‘(𝑦 − 𝐵)) → (𝑎 = (abs‘(𝑏 − 𝐵)) ↔ (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵))))
49	48	rexbidv 3158	. . . . . . . . . . . . 13 ⊢ (𝑎 = (abs‘(𝑦 − 𝐵)) → (∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵)) ↔ ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵))))
50	49	elrab 3661	. . . . . . . . . . . 12 ⊢ ((abs‘(𝑦 − 𝐵)) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ↔ ((abs‘(𝑦 − 𝐵)) ∈ ℝ ∧ ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵))))
51	42, 47, 50	sylanbrc 583	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (abs‘(𝑦 − 𝐵)) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
52	51	ne0d 4307	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅)
53	34, 52	exlimddv 1935	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅)
54		ssrab2 4045	. . . . . . . . . 10 ⊢ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ
55	54	a1i 11	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ)
56		gtso 11261	. . . . . . . . . 10 ⊢ ^◡ < Or ℝ
57		fisupcl 9427	. . . . . . . . . 10 ⊢ ((^◡ < Or ℝ ∧ ({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅ ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ)) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
58	56, 57	mpan 690	. . . . . . . . 9 ⊢ (({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅ ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
59	31, 53, 55, 58	syl3anc 1373	. . . . . . . 8 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
60	26, 59	sseldd 3949	. . . . . . 7 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ⁺)
61	54	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ)
62		soss 5568	. . . . . . . . . . . . . . . 16 ⊢ ({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ → (^◡ < Or ℝ → ^◡ < Or {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}))
63	54, 56, 62	mp2 9	. . . . . . . . . . . . . . 15 ⊢ ^◡ < Or {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}
64	63	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ^◡ < Or {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
65		fisupg 9241	. . . . . . . . . . . . . 14 ⊢ ((^◡ < Or {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)))
66	64, 31, 53, 65	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)))
67		elrabi 3656	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} → 𝑐 ∈ ℝ)
68		elrabi 3656	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} → 𝑑 ∈ ℝ)
69		vex 3454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑐 ∈ V
70		vex 3454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑑 ∈ V
71	69, 70	brcnv 5848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐^◡ < 𝑑 ↔ 𝑑 < 𝑐)
72	71	notbii 320	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑐^◡ < 𝑑 ↔ ¬ 𝑑 < 𝑐)
73		lenlt 11258	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑐 ≤ 𝑑 ↔ ¬ 𝑑 < 𝑐))
74	73	biimprd 248	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (¬ 𝑑 < 𝑐 → 𝑐 ≤ 𝑑))
75	72, 74	biimtrid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (¬ 𝑐^◡ < 𝑑 → 𝑐 ≤ 𝑑))
76	75	adantll 714	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) ∧ 𝑑 ∈ ℝ) → (¬ 𝑐^◡ < 𝑑 → 𝑐 ≤ 𝑑))
77	68, 76	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) ∧ 𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → (¬ 𝑐^◡ < 𝑑 → 𝑐 ≤ 𝑑))
78	77	ralimdva 3146	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) → (∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 → ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
79	78	adantrd 491	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) → ((∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)) → ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
80	67, 79	sylan2 593	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → ((∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)) → ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
81	80	reximdva 3147	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → (∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
82	66, 81	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑)
83	82	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑)
84		lbinfle 12144	. . . . . . . . . . 11 ⊢ (({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ ∧ ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑 ∧ (abs‘(𝑦 − 𝐵)) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) ≤ (abs‘(𝑦 − 𝐵)))
85	61, 83, 51, 84	syl3anc 1373	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) ≤ (abs‘(𝑦 − 𝐵)))
86		df-inf 9400	. . . . . . . . . . . 12 ⊢ inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )
87	86	eqcomi 2739	. . . . . . . . . . 11 ⊢ sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) = inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < )
88	87	breq1i 5116	. . . . . . . . . 10 ⊢ (sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ≤ (abs‘(𝑦 − 𝐵)) ↔ inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) ≤ (abs‘(𝑦 − 𝐵)))
89	85, 88	sylibr 234	. . . . . . . . 9 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ≤ (abs‘(𝑦 − 𝐵)))
90	54, 59	sselid 3946	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ)
91	90	adantr 480	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ)
92	91, 42	lenltd 11326	. . . . . . . . 9 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ≤ (abs‘(𝑦 − 𝐵)) ↔ ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
93	89, 92	mpbid 232	. . . . . . . 8 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ))
94	93	ralrimiva 3126	. . . . . . 7 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ))
95		breq2 5113	. . . . . . . . . 10 ⊢ (𝑥 = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) → ((abs‘(𝑦 − 𝐵)) < 𝑥 ↔ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
96	95	notbid 318	. . . . . . . . 9 ⊢ (𝑥 = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) → (¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
97	96	ralbidv 3157	. . . . . . . 8 ⊢ (𝑥 = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) → (∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
98	97	rspcev 3591	. . . . . . 7 ⊢ ((sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ⁺ ∧ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )) → ∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥)
99	60, 94, 98	syl2anc 584	. . . . . 6 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥)
100		ralnex 3056	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ¬ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
101	100	rexbii 3077	. . . . . . 7 ⊢ (∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ∃𝑥 ∈ ℝ⁺ ¬ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
102		rexnal 3083	. . . . . . 7 ⊢ (∃𝑥 ∈ ℝ⁺ ¬ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
103	101, 102	bitri 275	. . . . . 6 ⊢ (∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
104	99, 103	sylib 218	. . . . 5 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
105	104	ex 412	. . . 4 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → (𝐴 ∈ Fin → ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥))
106	105	3impa 1109	. . 3 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → (𝐴 ∈ Fin → ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥))
107	106	con2d 134	. 2 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → (∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥 → ¬ 𝐴 ∈ Fin))
108	107	imp 406	1 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥) → ¬ 𝐴 ∈ Fin)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∃wex 1779 ∈ wcel 2109 {cab 2708 ≠ wne 2926 ∀wral 3045 ∃wrex 3054 {crab 3408 ⊆ wss 3916 ∅c0 4298 class class class wbr 5109 Or wor 5547 ^◡ccnv 5639 ‘cfv 6513 (class class class)co 7389 Fincfn 8920 supcsup 9397 infcinf 9398 ℂcc 11072 ℝcr 11073 0cc0 11074 < clt 11214 ≤ cle 11215 − cmin 11411 ℝ⁺crp 12957 abscabs 15206

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5253 ax-nul 5263 ax-pow 5322 ax-pr 5389 ax-un 7713 ax-cnex 11130 ax-resscn 11131 ax-1cn 11132 ax-icn 11133 ax-addcl 11134 ax-addrcl 11135 ax-mulcl 11136 ax-mulrcl 11137 ax-mulcom 11138 ax-addass 11139 ax-mulass 11140 ax-distr 11141 ax-i2m1 11142 ax-1ne0 11143 ax-1rid 11144 ax-rnegex 11145 ax-rrecex 11146 ax-cnre 11147 ax-pre-lttri 11148 ax-pre-lttrn 11149 ax-pre-ltadd 11150 ax-pre-mulgt0 11151 ax-pre-sup 11152

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3756 df-csb 3865 df-dif 3919 df-un 3921 df-in 3923 df-ss 3933 df-pss 3936 df-nul 4299 df-if 4491 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-iun 4959 df-br 5110 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5535 df-eprel 5540 df-po 5548 df-so 5549 df-fr 5593 df-we 5595 df-xp 5646 df-rel 5647 df-cnv 5648 df-co 5649 df-dm 5650 df-rn 5651 df-res 5652 df-ima 5653 df-pred 6276 df-ord 6337 df-on 6338 df-lim 6339 df-suc 6340 df-iota 6466 df-fun 6515 df-fn 6516 df-f 6517 df-f1 6518 df-fo 6519 df-f1o 6520 df-fv 6521 df-riota 7346 df-ov 7392 df-oprab 7393 df-mpo 7394 df-om 7845 df-1st 7970 df-2nd 7971 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8380 df-1o 8436 df-er 8673 df-en 8921 df-dom 8922 df-sdom 8923 df-fin 8924 df-sup 9399 df-inf 9400 df-pnf 11216 df-mnf 11217 df-xr 11218 df-ltxr 11219 df-le 11220 df-sub 11413 df-neg 11414 df-div 11842 df-nn 12188 df-2 12250 df-3 12251 df-n0 12449 df-z 12536 df-uz 12800 df-rp 12958 df-seq 13973 df-exp 14033 df-cj 15071 df-re 15072 df-im 15073 df-sqrt 15207 df-abs 15208

This theorem is referenced by: rencldnfi 42802

W3C validator