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 43765

Description: Lemma for rencldnfi 43766. (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 2764	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑎 = (abs‘(𝑏 − 𝐵)) ↔ 𝑐 = (abs‘(𝑏 − 𝐵))))
2	1	rexbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵)) ↔ ∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵))))
3	2	elrab 3644	. . . . . . . . . . 11 ⊢ (𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ↔ (𝑐 ∈ ℝ ∧ ∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵))))
4		simp-4l 795	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝐴 ⊆ ℝ)
5		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐴)
6	4, 5	sseldd 3931	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ℝ)
7	6	recnd 11308	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ℂ)
8		simp-4r 796	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝐵 ∈ ℝ)
9	8	recnd 11308	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝐵 ∈ ℂ)
10	7, 9	subcld 11640	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (𝑏 − 𝐵) ∈ ℂ)
11		simprr 785	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → ¬ 𝐵 ∈ 𝐴)
12	11	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → ¬ 𝐵 ∈ 𝐴)
13		nelneq 2884	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ 𝐴 ∧ ¬ 𝐵 ∈ 𝐴) → ¬ 𝑏 = 𝐵)
14	5, 12, 13	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → ¬ 𝑏 = 𝐵)
15		subeq0 11555	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑏 − 𝐵) = 0 ↔ 𝑏 = 𝐵))
16	15	necon3abid 2991	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑏 − 𝐵) ≠ 0 ↔ ¬ 𝑏 = 𝐵))
17	7, 9, 16	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → ((𝑏 − 𝐵) ≠ 0 ↔ ¬ 𝑏 = 𝐵))
18	14, 17	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (𝑏 − 𝐵) ≠ 0)
19	10, 18	absrpcld 15585	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (abs‘(𝑏 − 𝐵)) ∈ ℝ⁺)
20		eleq1 2848	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (abs‘(𝑏 − 𝐵)) → (𝑐 ∈ ℝ⁺ ↔ (abs‘(𝑏 − 𝐵)) ∈ ℝ⁺))
21	19, 20	syl5ibrcom 250	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (𝑐 = (abs‘(𝑏 − 𝐵)) → 𝑐 ∈ ℝ⁺))
22	21	rexlimdva 3163	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) → (∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵)) → 𝑐 ∈ ℝ⁺))
23	22	expimpd 459	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → ((𝑐 ∈ ℝ ∧ ∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵))) → 𝑐 ∈ ℝ⁺))
24	3, 23	biimtrid 245	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → (𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} → 𝑐 ∈ ℝ⁺))
25	24	ssrdv 3936	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ⁺)
26	25	adantr 486	. . . . . . . 8 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ⁺)
27		abrexfi 9319	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Fin → {𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
28		rabssab 4032	. . . . . . . . . . 11 ⊢ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ {𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}
29		ssfi 9166	. . . . . . . . . . 11 ⊢ (({𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ {𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
30	27, 28, 29	sylancl 598	. . . . . . . . . 10 ⊢ (𝐴 ∈ Fin → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
31	30	adantl 487	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
32		simplrl 789	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → 𝐴 ≠ ∅)
33		n0 4299	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐴)
34	32, 33	sylib 221	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑦 𝑦 ∈ 𝐴)
35		simp-4l 795	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝐴 ⊆ ℝ)
36		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
37	35, 36	sseldd 3931	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ)
38	37	recnd 11308	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ)
39		simp-4r 796	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ ℝ)
40	39	recnd 11308	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ ℂ)
41	38, 40	subcld 11640	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (𝑦 − 𝐵) ∈ ℂ)
42	41	abscld 15573	. . . . . . . . . . . 12 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (abs‘(𝑦 − 𝐵)) ∈ ℝ)
43		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (abs‘(𝑦 − 𝐵)) = (abs‘(𝑦 − 𝐵))
44		fvoveq1 7431	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑦 → (abs‘(𝑏 − 𝐵)) = (abs‘(𝑦 − 𝐵)))
45	44	rspceeqv 3598	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ (abs‘(𝑦 − 𝐵)) = (abs‘(𝑦 − 𝐵))) → ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
46	43, 45	mpan2 704	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 → ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
47	46	adantl 487	. . . . . . . . . . . 12 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
48		eqeq1 2764	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (abs‘(𝑦 − 𝐵)) → (𝑎 = (abs‘(𝑏 − 𝐵)) ↔ (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵))))
49	48	rexbidv 3186	. . . . . . . . . . . . 13 ⊢ (𝑎 = (abs‘(𝑦 − 𝐵)) → (∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵)) ↔ ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵))))
50	49	elrab 3644	. . . . . . . . . . . 12 ⊢ ((abs‘(𝑦 − 𝐵)) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ↔ ((abs‘(𝑦 − 𝐵)) ∈ ℝ ∧ ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵))))
51	42, 47, 50	sylanbrc 595	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (abs‘(𝑦 − 𝐵)) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
52	51	ne0d 4287	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅)
53	34, 52	exlimddv 1968	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅)
54		ssrab2 4027	. . . . . . . . . 10 ⊢ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ
55	54	a1i 11	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ)
56		gtso 11362	. . . . . . . . . 10 ⊢ ^◡ < Or ℝ
57		fisupcl 9440	. . . . . . . . . 10 ⊢ ((^◡ < Or ℝ ∧ ({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅ ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ)) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
58	56, 57	mpan 703	. . . . . . . . 9 ⊢ (({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅ ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
59	31, 53, 55, 58	syl3anc 1398	. . . . . . . 8 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
60	26, 59	sseldd 3931	. . . . . . 7 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ⁺)
61	54	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ)
62		soss 5575	. . . . . . . . . . . . . . . 16 ⊢ ({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ → (^◡ < Or ℝ → ^◡ < Or {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}))
63	54, 56, 62	mp2 9	. . . . . . . . . . . . . . 15 ⊢ ^◡ < Or {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}
64	63	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ^◡ < Or {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
65		fisupg 9257	. . . . . . . . . . . . . 14 ⊢ ((^◡ < Or {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)))
66	64, 31, 53, 65	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)))
67		elrabi 3640	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} → 𝑐 ∈ ℝ)
68		elrabi 3640	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} → 𝑑 ∈ ℝ)
69		vex 3454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑐 ∈ V
70		vex 3454	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑑 ∈ V
71	69, 70	brcnv 5856	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐^◡ < 𝑑 ↔ 𝑑 < 𝑐)
72	71	notbii 323	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑐^◡ < 𝑑 ↔ ¬ 𝑑 < 𝑐)
73		lenlt 11359	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑐 ≤ 𝑑 ↔ ¬ 𝑑 < 𝑐))
74	73	biimprd 251	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (¬ 𝑑 < 𝑐 → 𝑐 ≤ 𝑑))
75	72, 74	biimtrid 245	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (¬ 𝑐^◡ < 𝑑 → 𝑐 ≤ 𝑑))
76	75	adantll 727	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) ∧ 𝑑 ∈ ℝ) → (¬ 𝑐^◡ < 𝑑 → 𝑐 ≤ 𝑑))
77	68, 76	sylan2 605	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) ∧ 𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → (¬ 𝑐^◡ < 𝑑 → 𝑐 ≤ 𝑑))
78	77	ralimdva 3174	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) → (∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 → ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
79	78	adantrd 497	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) → ((∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)) → ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
80	67, 79	sylan2 605	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → ((∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)) → ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
81	80	reximdva 3175	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → (∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
82	66, 81	mpd 16	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑)
83	82	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑)
84		lbinfle 12241	. . . . . . . . . . 11 ⊢ (({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ ∧ ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑 ∧ (abs‘(𝑦 − 𝐵)) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) ≤ (abs‘(𝑦 − 𝐵)))
85	61, 83, 51, 84	syl3anc 1398	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) ≤ (abs‘(𝑦 − 𝐵)))
86		df-inf 9413	. . . . . . . . . . . 12 ⊢ inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )
87	86	eqcomi 2769	. . . . . . . . . . 11 ⊢ sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) = inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < )
88	87	breq1i 5109	. . . . . . . . . 10 ⊢ (sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ≤ (abs‘(𝑦 − 𝐵)) ↔ inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) ≤ (abs‘(𝑦 − 𝐵)))
89	85, 88	sylibr 237	. . . . . . . . 9 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ≤ (abs‘(𝑦 − 𝐵)))
90	54, 59	sselid 3928	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ)
91	90	adantr 486	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ)
92	91, 42	lenltd 11427	. . . . . . . . 9 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ≤ (abs‘(𝑦 − 𝐵)) ↔ ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
93	89, 92	mpbid 235	. . . . . . . 8 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ))
94	93	ralrimiva 3154	. . . . . . 7 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ))
95		breq2 5106	. . . . . . . . . 10 ⊢ (𝑥 = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) → ((abs‘(𝑦 − 𝐵)) < 𝑥 ↔ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
96	95	notbid 321	. . . . . . . . 9 ⊢ (𝑥 = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) → (¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
97	96	ralbidv 3185	. . . . . . . 8 ⊢ (𝑥 = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) → (∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
98	97	rspcev 3576	. . . . . . 7 ⊢ ((sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ⁺ ∧ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )) → ∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥)
99	60, 94, 98	syl2anc 596	. . . . . 6 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥)
100		ralnex 3088	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ¬ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
101	100	rexbii 3109	. . . . . . 7 ⊢ (∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ∃𝑥 ∈ ℝ⁺ ¬ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
102		rexnal 3114	. . . . . . 7 ⊢ (∃𝑥 ∈ ℝ⁺ ¬ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
103	101, 102	bitri 278	. . . . . 6 ⊢ (∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
104	99, 103	sylib 221	. . . . 5 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
105	104	ex 418	. . . 4 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → (𝐴 ∈ Fin → ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥))
106	105	3impa 1127	. . 3 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → (𝐴 ∈ Fin → ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥))
107	106	con2d 135	. 2 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → (∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥 → ¬ 𝐴 ∈ Fin))
108	107	imp 412	1 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥) → ¬ 𝐴 ∈ Fin)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2145 {cab 2738 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 {crab 3412 ⊆ wss 3898 ∅c0 4278 class class class wbr 5102 Or wor 5554 ^◡ccnv 5646 ‘cfv 6527 (class class class)co 7408 Fincfn 8951 supcsup 9410 infcinf 9411 ℂcc 11169 ℝcr 11170 0cc0 11171 < clt 11314 ≤ cle 11315 − cmin 11512 ℝ⁺crp 13089 abscabs 15368

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 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734 ax-cnex 11227 ax-resscn 11228 ax-1cn 11229 ax-icn 11230 ax-addcl 11231 ax-addrcl 11232 ax-mulcl 11233 ax-mulrcl 11234 ax-mulcom 11235 ax-addass 11236 ax-mulass 11237 ax-distr 11238 ax-i2m1 11239 ax-1ne0 11240 ax-1rid 11241 ax-rnegex 11242 ax-rrecex 11243 ax-cnre 11244 ax-pre-lttri 11245 ax-pre-lttrn 11246 ax-pre-ltadd 11247 ax-pre-mulgt0 11248 ax-pre-sup 11249

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 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6293 df-ord 6354 df-on 6355 df-lim 6356 df-suc 6357 df-iota 6483 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7861 df-1st 7984 df-2nd 7985 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8454 df-er 8695 df-en 8952 df-dom 8953 df-sdom 8954 df-fin 8955 df-sup 9412 df-inf 9413 df-pnf 11316 df-mnf 11317 df-xr 11318 df-ltxr 11319 df-le 11320 df-sub 11514 df-neg 11515 df-div 11943 df-nn 12305 df-2 12374 df-3 12375 df-n0 12576 df-z 12663 df-uz 12935 df-rp 13090 df-seq 14113 df-exp 14173 df-cj 15233 df-re 15234 df-im 15235 df-sqrt 15369 df-abs 15370

This theorem is used by: rencldnfi 43766

W3C validator