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 41234

Description: Lemma for rencldnfi 41235. (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 2735	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑎 = (abs‘(𝑏 − 𝐵)) ↔ 𝑐 = (abs‘(𝑏 − 𝐵))))
2	1	rexbidv 3177	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵)) ↔ ∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵))))
3	2	elrab 3663	. . . . . . . . . . 11 ⊢ (𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ↔ (𝑐 ∈ ℝ ∧ ∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵))))
4		simp-4l 781	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝐴 ⊆ ℝ)
5		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐴)
6	4, 5	sseldd 3963	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ℝ)
7	6	recnd 11207	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ℂ)
8		simp-4r 782	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝐵 ∈ ℝ)
9	8	recnd 11207	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝐵 ∈ ℂ)
10	7, 9	subcld 11536	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (𝑏 − 𝐵) ∈ ℂ)
11		simprr 771	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → ¬ 𝐵 ∈ 𝐴)
12	11	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → ¬ 𝐵 ∈ 𝐴)
13		nelneq 2856	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ 𝐴 ∧ ¬ 𝐵 ∈ 𝐴) → ¬ 𝑏 = 𝐵)
14	5, 12, 13	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → ¬ 𝑏 = 𝐵)
15		subeq0 11451	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑏 − 𝐵) = 0 ↔ 𝑏 = 𝐵))
16	15	necon3abid 2976	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑏 − 𝐵) ≠ 0 ↔ ¬ 𝑏 = 𝐵))
17	7, 9, 16	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → ((𝑏 − 𝐵) ≠ 0 ↔ ¬ 𝑏 = 𝐵))
18	14, 17	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (𝑏 − 𝐵) ≠ 0)
19	10, 18	absrpcld 15360	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (abs‘(𝑏 − 𝐵)) ∈ ℝ⁺)
20		eleq1 2820	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (abs‘(𝑏 − 𝐵)) → (𝑐 ∈ ℝ⁺ ↔ (abs‘(𝑏 − 𝐵)) ∈ ℝ⁺))
21	19, 20	syl5ibrcom 246	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (𝑐 = (abs‘(𝑏 − 𝐵)) → 𝑐 ∈ ℝ⁺))
22	21	rexlimdva 3154	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) → (∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵)) → 𝑐 ∈ ℝ⁺))
23	22	expimpd 454	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → ((𝑐 ∈ ℝ ∧ ∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵))) → 𝑐 ∈ ℝ⁺))
24	3, 23	biimtrid 241	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → (𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} → 𝑐 ∈ ℝ⁺))
25	24	ssrdv 3968	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ⁺)
26	25	adantr 481	. . . . . . . 8 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ⁺)
27		abrexfi 9318	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Fin → {𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
28		rabssab 4063	. . . . . . . . . . 11 ⊢ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ {𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}
29		ssfi 9139	. . . . . . . . . . 11 ⊢ (({𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ {𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
30	27, 28, 29	sylancl 586	. . . . . . . . . 10 ⊢ (𝐴 ∈ Fin → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
31	30	adantl 482	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
32		simplrl 775	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → 𝐴 ≠ ∅)
33		n0 4326	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐴)
34	32, 33	sylib 217	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑦 𝑦 ∈ 𝐴)
35		simp-4l 781	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝐴 ⊆ ℝ)
36		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
37	35, 36	sseldd 3963	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ)
38	37	recnd 11207	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ)
39		simp-4r 782	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ ℝ)
40	39	recnd 11207	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ ℂ)
41	38, 40	subcld 11536	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (𝑦 − 𝐵) ∈ ℂ)
42	41	abscld 15348	. . . . . . . . . . . 12 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (abs‘(𝑦 − 𝐵)) ∈ ℝ)
43		eqid 2731	. . . . . . . . . . . . . 14 ⊢ (abs‘(𝑦 − 𝐵)) = (abs‘(𝑦 − 𝐵))
44		fvoveq1 7400	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑦 → (abs‘(𝑏 − 𝐵)) = (abs‘(𝑦 − 𝐵)))
45	44	rspceeqv 3613	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ (abs‘(𝑦 − 𝐵)) = (abs‘(𝑦 − 𝐵))) → ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
46	43, 45	mpan2 689	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 → ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
47	46	adantl 482	. . . . . . . . . . . 12 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
48		eqeq1 2735	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (abs‘(𝑦 − 𝐵)) → (𝑎 = (abs‘(𝑏 − 𝐵)) ↔ (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵))))
49	48	rexbidv 3177	. . . . . . . . . . . . 13 ⊢ (𝑎 = (abs‘(𝑦 − 𝐵)) → (∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵)) ↔ ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵))))
50	49	elrab 3663	. . . . . . . . . . . 12 ⊢ ((abs‘(𝑦 − 𝐵)) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ↔ ((abs‘(𝑦 − 𝐵)) ∈ ℝ ∧ ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵))))
51	42, 47, 50	sylanbrc 583	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (abs‘(𝑦 − 𝐵)) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
52	51	ne0d 4315	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅)
53	34, 52	exlimddv 1938	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅)
54		ssrab2 4057	. . . . . . . . . 10 ⊢ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ
55	54	a1i 11	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ)
56		gtso 11260	. . . . . . . . . 10 ⊢ ^◡ < Or ℝ
57		fisupcl 9429	. . . . . . . . . 10 ⊢ ((^◡ < Or ℝ ∧ ({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅ ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ)) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
58	56, 57	mpan 688	. . . . . . . . 9 ⊢ (({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅ ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
59	31, 53, 55, 58	syl3anc 1371	. . . . . . . 8 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
60	26, 59	sseldd 3963	. . . . . . 7 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ⁺)
61	54	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ)
62		soss 5585	. . . . . . . . . . . . . . . 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 1371	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)))
67		elrabi 3657	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} → 𝑐 ∈ ℝ)
68		elrabi 3657	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} → 𝑑 ∈ ℝ)
69		vex 3463	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑐 ∈ V
70		vex 3463	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑑 ∈ V
71	69, 70	brcnv 5858	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐^◡ < 𝑑 ↔ 𝑑 < 𝑐)
72	71	notbii 319	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑐^◡ < 𝑑 ↔ ¬ 𝑑 < 𝑐)
73		lenlt 11257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑐 ≤ 𝑑 ↔ ¬ 𝑑 < 𝑐))
74	73	biimprd 247	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (¬ 𝑑 < 𝑐 → 𝑐 ≤ 𝑑))
75	72, 74	biimtrid 241	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (¬ 𝑐^◡ < 𝑑 → 𝑐 ≤ 𝑑))
76	75	adantll 712	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) ∧ 𝑑 ∈ ℝ) → (¬ 𝑐^◡ < 𝑑 → 𝑐 ≤ 𝑑))
77	68, 76	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) ∧ 𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → (¬ 𝑐^◡ < 𝑑 → 𝑐 ≤ 𝑑))
78	77	ralimdva 3166	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) → (∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 → ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
79	78	adantrd 492	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) → ((∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)) → ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
80	67, 79	sylan2 593	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → ((∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)) → ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
81	80	reximdva 3167	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → (∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
82	66, 81	mpd 15	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑)
83	82	adantr 481	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑)
84		lbinfle 12134	. . . . . . . . . . 11 ⊢ (({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ ∧ ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑 ∧ (abs‘(𝑦 − 𝐵)) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) ≤ (abs‘(𝑦 − 𝐵)))
85	61, 83, 51, 84	syl3anc 1371	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) ≤ (abs‘(𝑦 − 𝐵)))
86		df-inf 9403	. . . . . . . . . . . 12 ⊢ inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )
87	86	eqcomi 2740	. . . . . . . . . . 11 ⊢ sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) = inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < )
88	87	breq1i 5132	. . . . . . . . . 10 ⊢ (sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ≤ (abs‘(𝑦 − 𝐵)) ↔ inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) ≤ (abs‘(𝑦 − 𝐵)))
89	85, 88	sylibr 233	. . . . . . . . 9 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ≤ (abs‘(𝑦 − 𝐵)))
90	54, 59	sselid 3960	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ)
91	90	adantr 481	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ)
92	91, 42	lenltd 11325	. . . . . . . . 9 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ≤ (abs‘(𝑦 − 𝐵)) ↔ ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
93	89, 92	mpbid 231	. . . . . . . 8 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ))
94	93	ralrimiva 3145	. . . . . . 7 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ))
95		breq2 5129	. . . . . . . . . 10 ⊢ (𝑥 = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) → ((abs‘(𝑦 − 𝐵)) < 𝑥 ↔ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
96	95	notbid 317	. . . . . . . . 9 ⊢ (𝑥 = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) → (¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
97	96	ralbidv 3176	. . . . . . . 8 ⊢ (𝑥 = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) → (∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
98	97	rspcev 3595	. . . . . . 7 ⊢ ((sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ⁺ ∧ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )) → ∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥)
99	60, 94, 98	syl2anc 584	. . . . . 6 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥)
100		ralnex 3071	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ¬ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
101	100	rexbii 3093	. . . . . . 7 ⊢ (∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ∃𝑥 ∈ ℝ⁺ ¬ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
102		rexnal 3099	. . . . . . 7 ⊢ (∃𝑥 ∈ ℝ⁺ ¬ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
103	101, 102	bitri 274	. . . . . 6 ⊢ (∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
104	99, 103	sylib 217	. . . . 5 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
105	104	ex 413	. . . 4 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → (𝐴 ∈ Fin → ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥))
106	105	3impa 1110	. . 3 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → (𝐴 ∈ Fin → ¬ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥))
107	106	con2d 134	. 2 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → (∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥 → ¬ 𝐴 ∈ Fin))
108	107	imp 407	1 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ ∀𝑥 ∈ ℝ⁺ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥) → ¬ 𝐴 ∈ Fin)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∃wex 1781 ∈ wcel 2106 {cab 2708 ≠ wne 2939 ∀wral 3060 ∃wrex 3069 {crab 3418 ⊆ wss 3928 ∅c0 4302 class class class wbr 5125 Or wor 5564 ^◡ccnv 5652 ‘cfv 6516 (class class class)co 7377 Fincfn 8905 supcsup 9400 infcinf 9401 ℂcc 11073 ℝcr 11074 0cc0 11075 < clt 11213 ≤ cle 11214 − cmin 11409 ℝ⁺crp 12939 abscabs 15146

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5276 ax-nul 5283 ax-pow 5340 ax-pr 5404 ax-un 7692 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3364 df-reu 3365 df-rab 3419 df-v 3461 df-sbc 3758 df-csb 3874 df-dif 3931 df-un 3933 df-in 3935 df-ss 3945 df-pss 3947 df-nul 4303 df-if 4507 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4886 df-iun 4976 df-br 5126 df-opab 5188 df-mpt 5209 df-tr 5243 df-id 5551 df-eprel 5557 df-po 5565 df-so 5566 df-fr 5608 df-we 5610 df-xp 5659 df-rel 5660 df-cnv 5661 df-co 5662 df-dm 5663 df-rn 5664 df-res 5665 df-ima 5666 df-pred 6273 df-ord 6340 df-on 6341 df-lim 6342 df-suc 6343 df-iota 6468 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-riota 7333 df-ov 7380 df-oprab 7381 df-mpo 7382 df-om 7823 df-1st 7941 df-2nd 7942 df-frecs 8232 df-wrecs 8263 df-recs 8337 df-rdg 8376 df-1o 8432 df-er 8670 df-en 8906 df-dom 8907 df-sdom 8908 df-fin 8909 df-sup 9402 df-inf 9403 df-pnf 11215 df-mnf 11216 df-xr 11217 df-ltxr 11218 df-le 11219 df-sub 11411 df-neg 11412 df-div 11837 df-nn 12178 df-2 12240 df-3 12241 df-n0 12438 df-z 12524 df-uz 12788 df-rp 12940 df-seq 13932 df-exp 13993 df-cj 15011 df-re 15012 df-im 15013 df-sqrt 15147 df-abs 15148

This theorem is referenced by: rencldnfi 41235

W3C validator