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 43251

Description: Lemma for rencldnfi 43252. (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 2741	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑐 → (𝑎 = (abs‘(𝑏 − 𝐵)) ↔ 𝑐 = (abs‘(𝑏 − 𝐵))))
2	1	rexbidv 3162	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → (∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵)) ↔ ∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵))))
3	2	elrab 3635	. . . . . . . . . . 11 ⊢ (𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ↔ (𝑐 ∈ ℝ ∧ ∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵))))
4		simp-4l 783	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝐴 ⊆ ℝ)
5		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐴)
6	4, 5	sseldd 3923	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ℝ)
7	6	recnd 11161	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ ℂ)
8		simp-4r 784	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝐵 ∈ ℝ)
9	8	recnd 11161	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → 𝐵 ∈ ℂ)
10	7, 9	subcld 11493	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (𝑏 − 𝐵) ∈ ℂ)
11		simprr 773	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → ¬ 𝐵 ∈ 𝐴)
12	11	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → ¬ 𝐵 ∈ 𝐴)
13		nelneq 2861	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ 𝐴 ∧ ¬ 𝐵 ∈ 𝐴) → ¬ 𝑏 = 𝐵)
14	5, 12, 13	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → ¬ 𝑏 = 𝐵)
15		subeq0 11408	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑏 − 𝐵) = 0 ↔ 𝑏 = 𝐵))
16	15	necon3abid 2969	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝑏 − 𝐵) ≠ 0 ↔ ¬ 𝑏 = 𝐵))
17	7, 9, 16	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → ((𝑏 − 𝐵) ≠ 0 ↔ ¬ 𝑏 = 𝐵))
18	14, 17	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (𝑏 − 𝐵) ≠ 0)
19	10, 18	absrpcld 15375	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (abs‘(𝑏 − 𝐵)) ∈ ℝ⁺)
20		eleq1 2825	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (abs‘(𝑏 − 𝐵)) → (𝑐 ∈ ℝ⁺ ↔ (abs‘(𝑏 − 𝐵)) ∈ ℝ⁺))
21	19, 20	syl5ibrcom 247	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) ∧ 𝑏 ∈ 𝐴) → (𝑐 = (abs‘(𝑏 − 𝐵)) → 𝑐 ∈ ℝ⁺))
22	21	rexlimdva 3139	. . . . . . . . . . . 12 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝑐 ∈ ℝ) → (∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵)) → 𝑐 ∈ ℝ⁺))
23	22	expimpd 453	. . . . . . . . . . 11 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → ((𝑐 ∈ ℝ ∧ ∃𝑏 ∈ 𝐴 𝑐 = (abs‘(𝑏 − 𝐵))) → 𝑐 ∈ ℝ⁺))
24	3, 23	biimtrid 242	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → (𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} → 𝑐 ∈ ℝ⁺))
25	24	ssrdv 3928	. . . . . . . . 9 ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ⁺)
26	25	adantr 480	. . . . . . . 8 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ⁺)
27		abrexfi 9253	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Fin → {𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
28		rabssab 4026	. . . . . . . . . . 11 ⊢ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ {𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}
29		ssfi 9098	. . . . . . . . . . 11 ⊢ (({𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ {𝑎 ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
30	27, 28, 29	sylancl 587	. . . . . . . . . 10 ⊢ (𝐴 ∈ Fin → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
31	30	adantl 481	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin)
32		simplrl 777	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → 𝐴 ≠ ∅)
33		n0 4294	. . . . . . . . . . 11 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐴)
34	32, 33	sylib 218	. . . . . . . . . 10 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑦 𝑦 ∈ 𝐴)
35		simp-4l 783	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝐴 ⊆ ℝ)
36		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
37	35, 36	sseldd 3923	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ)
38	37	recnd 11161	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℂ)
39		simp-4r 784	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ ℝ)
40	39	recnd 11161	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ ℂ)
41	38, 40	subcld 11493	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (𝑦 − 𝐵) ∈ ℂ)
42	41	abscld 15363	. . . . . . . . . . . 12 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (abs‘(𝑦 − 𝐵)) ∈ ℝ)
43		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (abs‘(𝑦 − 𝐵)) = (abs‘(𝑦 − 𝐵))
44		fvoveq1 7381	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑦 → (abs‘(𝑏 − 𝐵)) = (abs‘(𝑦 − 𝐵)))
45	44	rspceeqv 3588	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ (abs‘(𝑦 − 𝐵)) = (abs‘(𝑦 − 𝐵))) → ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
46	43, 45	mpan2 692	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐴 → ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
47	46	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵)))
48		eqeq1 2741	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (abs‘(𝑦 − 𝐵)) → (𝑎 = (abs‘(𝑏 − 𝐵)) ↔ (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵))))
49	48	rexbidv 3162	. . . . . . . . . . . . 13 ⊢ (𝑎 = (abs‘(𝑦 − 𝐵)) → (∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵)) ↔ ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵))))
50	49	elrab 3635	. . . . . . . . . . . 12 ⊢ ((abs‘(𝑦 − 𝐵)) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ↔ ((abs‘(𝑦 − 𝐵)) ∈ ℝ ∧ ∃𝑏 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) = (abs‘(𝑏 − 𝐵))))
51	42, 47, 50	sylanbrc 584	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (abs‘(𝑦 − 𝐵)) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
52	51	ne0d 4283	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅)
53	34, 52	exlimddv 1937	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅)
54		ssrab2 4021	. . . . . . . . . 10 ⊢ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ
55	54	a1i 11	. . . . . . . . 9 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ)
56		gtso 11215	. . . . . . . . . 10 ⊢ ^◡ < Or ℝ
57		fisupcl 9374	. . . . . . . . . 10 ⊢ ((^◡ < Or ℝ ∧ ({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅ ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ)) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
58	56, 57	mpan 691	. . . . . . . . 9 ⊢ (({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅ ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
59	31, 53, 55, 58	syl3anc 1374	. . . . . . . 8 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
60	26, 59	sseldd 3923	. . . . . . 7 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ⁺)
61	54	a1i 11	. . . . . . . . . . 11 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ)
62		soss 5550	. . . . . . . . . . . . . . . 16 ⊢ ({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ → (^◡ < Or ℝ → ^◡ < Or {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}))
63	54, 56, 62	mp2 9	. . . . . . . . . . . . . . 15 ⊢ ^◡ < Or {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}
64	63	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ^◡ < Or {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))})
65		fisupg 9189	. . . . . . . . . . . . . 14 ⊢ ((^◡ < Or {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ∈ Fin ∧ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ≠ ∅) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)))
66	64, 31, 53, 65	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)))
67		elrabi 3631	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} → 𝑐 ∈ ℝ)
68		elrabi 3631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} → 𝑑 ∈ ℝ)
69		vex 3434	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑐 ∈ V
70		vex 3434	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑑 ∈ V
71	69, 70	brcnv 5829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐^◡ < 𝑑 ↔ 𝑑 < 𝑐)
72	71	notbii 320	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑐^◡ < 𝑑 ↔ ¬ 𝑑 < 𝑐)
73		lenlt 11212	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑐 ≤ 𝑑 ↔ ¬ 𝑑 < 𝑐))
74	73	biimprd 248	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (¬ 𝑑 < 𝑐 → 𝑐 ≤ 𝑑))
75	72, 74	biimtrid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (¬ 𝑐^◡ < 𝑑 → 𝑐 ≤ 𝑑))
76	75	adantll 715	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) ∧ 𝑑 ∈ ℝ) → (¬ 𝑐^◡ < 𝑑 → 𝑐 ≤ 𝑑))
77	68, 76	sylan2 594	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) ∧ 𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → (¬ 𝑐^◡ < 𝑑 → 𝑐 ≤ 𝑑))
78	77	ralimdva 3150	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) → (∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 → ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
79	78	adantrd 491	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ ℝ) → ((∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)) → ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
80	67, 79	sylan2 594	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → ((∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ¬ 𝑐^◡ < 𝑑 ∧ ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} (𝑑^◡ < 𝑐 → ∃𝑥 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑑^◡ < 𝑥)) → ∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑))
81	80	reximdva 3151	. . . . . . . . . . . . 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 12098	. . . . . . . . . . 11 ⊢ (({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))} ⊆ ℝ ∧ ∃𝑐 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}∀𝑑 ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}𝑐 ≤ 𝑑 ∧ (abs‘(𝑦 − 𝐵)) ∈ {𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}) → inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) ≤ (abs‘(𝑦 − 𝐵)))
85	61, 83, 51, 84	syl3anc 1374	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) ≤ (abs‘(𝑦 − 𝐵)))
86		df-inf 9347	. . . . . . . . . . . 12 ⊢ inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )
87	86	eqcomi 2746	. . . . . . . . . . 11 ⊢ sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) = inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < )
88	87	breq1i 5093	. . . . . . . . . 10 ⊢ (sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ≤ (abs‘(𝑦 − 𝐵)) ↔ inf({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, < ) ≤ (abs‘(𝑦 − 𝐵)))
89	85, 88	sylibr 234	. . . . . . . . 9 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ≤ (abs‘(𝑦 − 𝐵)))
90	54, 59	sselid 3920	. . . . . . . . . . 11 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ)
91	90	adantr 480	. . . . . . . . . 10 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ)
92	91, 42	lenltd 11280	. . . . . . . . 9 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → (sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ≤ (abs‘(𝑦 − 𝐵)) ↔ ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
93	89, 92	mpbid 232	. . . . . . . 8 ⊢ (((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) ∧ 𝑦 ∈ 𝐴) → ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ))
94	93	ralrimiva 3130	. . . . . . 7 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ))
95		breq2 5090	. . . . . . . . . 10 ⊢ (𝑥 = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) → ((abs‘(𝑦 − 𝐵)) < 𝑥 ↔ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
96	95	notbid 318	. . . . . . . . 9 ⊢ (𝑥 = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) → (¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
97	96	ralbidv 3161	. . . . . . . 8 ⊢ (𝑥 = sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) → (∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )))
98	97	rspcev 3565	. . . . . . 7 ⊢ ((sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < ) ∈ ℝ⁺ ∧ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < sup({𝑎 ∈ ℝ ∣ ∃𝑏 ∈ 𝐴 𝑎 = (abs‘(𝑏 − 𝐵))}, ℝ, ^◡ < )) → ∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥)
99	60, 94, 98	syl2anc 585	. . . . . 6 ⊢ ((((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥)
100		ralnex 3064	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ¬ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
101	100	rexbii 3085	. . . . . . 7 ⊢ (∃𝑥 ∈ ℝ⁺ ∀𝑦 ∈ 𝐴 ¬ (abs‘(𝑦 − 𝐵)) < 𝑥 ↔ ∃𝑥 ∈ ℝ⁺ ¬ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥)
102		rexnal 3090	. . . . . . 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 1110	. . 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 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 {cab 2715 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 {crab 3390 ⊆ wss 3890 ∅c0 4274 class class class wbr 5086 Or wor 5529 ^◡ccnv 5621 ‘cfv 6490 (class class class)co 7358 Fincfn 8884 supcsup 9344 infcinf 9345 ℂcc 11025 ℝcr 11026 0cc0 11027 < clt 11167 ≤ cle 11168 − cmin 11365 ℝ⁺crp 12906 abscabs 15158

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104 ax-pre-sup 11105

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-er 8634 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-sup 9346 df-inf 9347 df-pnf 11169 df-mnf 11170 df-xr 11171 df-ltxr 11172 df-le 11173 df-sub 11367 df-neg 11368 df-div 11796 df-nn 12147 df-2 12209 df-3 12210 df-n0 12403 df-z 12490 df-uz 12753 df-rp 12907 df-seq 13926 df-exp 13986 df-cj 15023 df-re 15024 df-im 15025 df-sqrt 15159 df-abs 15160

This theorem is referenced by: rencldnfi 43252

W3C validator