rencldnfilem

		Ref	Expression
	Assertion	rencldnfilem	$⊢ ((A \subseteq ℝ \land B \in ℝ \land (A \neq \emptyset \land \neg B \in A)) \land \forall x \in ℝ^{+} \exists y \in A \|y - B\| < x) \to \neg A \in Fin$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ a = c \to (a = \|b - B\| \leftrightarrow c = \|b - B\|)$
2	1	rexbidv	$⊢ a = c \to (\exists b \in A a = \|b - B\| \leftrightarrow \exists b \in A c = \|b - B\|)$
3	2	elrab	$⊢ c \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \leftrightarrow (c \in ℝ \land \exists b \in A c = \|b - B\|)$
4		simp-4l	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land c \in ℝ) \land b \in A) \to A \subseteq ℝ$
5		simpr	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land c \in ℝ) \land b \in A) \to b \in A$
6	4 5	sseldd	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land c \in ℝ) \land b \in A) \to b \in ℝ$
7	6	recnd	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land c \in ℝ) \land b \in A) \to b \in ℂ$
8		simp-4r	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land c \in ℝ) \land b \in A) \to B \in ℝ$
9	8	recnd	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land c \in ℝ) \land b \in A) \to B \in ℂ$
10	7 9	subcld	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land c \in ℝ) \land b \in A) \to b - B \in ℂ$
11		simprr	$⊢ ((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \to \neg B \in A$
12	11	ad2antrr	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land c \in ℝ) \land b \in A) \to \neg B \in A$
13		nelneq	$⊢ (b \in A \land \neg B \in A) \to \neg b = B$
14	5 12 13	syl2anc	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land c \in ℝ) \land b \in A) \to \neg b = B$
15		subeq0	$⊢ (b \in ℂ \land B \in ℂ) \to (b - B = 0 \leftrightarrow b = B)$
16	15	necon3abid	$⊢ (b \in ℂ \land B \in ℂ) \to (b - B \neq 0 \leftrightarrow \neg b = B)$
17	7 9 16	syl2anc	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land c \in ℝ) \land b \in A) \to (b - B \neq 0 \leftrightarrow \neg b = B)$
18	14 17	mpbird	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land c \in ℝ) \land b \in A) \to b - B \neq 0$
19	10 18	absrpcld	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land c \in ℝ) \land b \in A) \to \|b - B\| \in ℝ^{+}$
20		eleq1	$⊢ c = \|b - B\| \to (c \in ℝ^{+} \leftrightarrow \|b - B\| \in ℝ^{+})$
21	19 20	syl5ibrcom	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land c \in ℝ) \land b \in A) \to (c = \|b - B\| \to c \in ℝ^{+})$
22	21	rexlimdva	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land c \in ℝ) \to (\exists b \in A c = \|b - B\| \to c \in ℝ^{+})$
23	22	expimpd	$⊢ ((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \to ((c \in ℝ \land \exists b \in A c = \|b - B\|) \to c \in ℝ^{+})$
24	3 23	biimtrid	$⊢ ((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \to (c \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \to c \in ℝ^{+})$
25	24	ssrdv	$⊢ ((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \to \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \subseteq ℝ^{+}$
26	25	adantr	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \subseteq ℝ^{+}$
27		abrexfi	$⊢ A \in Fin \to \{a \| \exists b \in A a = \|b - B\|\} \in Fin$
28		rabssab	$⊢ \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \subseteq \{a \| \exists b \in A a = \|b - B\|\}$
29		ssfi	$⊢ (\{a \| \exists b \in A a = \|b - B\|\} \in Fin \land \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \subseteq \{a \| \exists b \in A a = \|b - B\|\}) \to \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \in Fin$
30	27 28 29	sylancl	$⊢ A \in Fin \to \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \in Fin$
31	30	adantl	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \in Fin$
32		simplrl	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to A \neq \emptyset$
33		n0	$⊢ A \neq \emptyset \leftrightarrow \exists y y \in A$
34	32 33	sylib	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to \exists y y \in A$
35		simp-4l	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to A \subseteq ℝ$
36		simpr	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to y \in A$
37	35 36	sseldd	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to y \in ℝ$
38	37	recnd	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to y \in ℂ$
39		simp-4r	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to B \in ℝ$
40	39	recnd	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to B \in ℂ$
41	38 40	subcld	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to y - B \in ℂ$
42	41	abscld	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to \|y - B\| \in ℝ$
43		eqid	$⊢ \|y - B\| = \|y - B\|$
44		fvoveq1	$⊢ b = y \to \|b - B\| = \|y - B\|$
45	44	rspceeqv	$⊢ (y \in A \land \|y - B\| = \|y - B\|) \to \exists b \in A \|y - B\| = \|b - B\|$
46	43 45	mpan2	$⊢ y \in A \to \exists b \in A \|y - B\| = \|b - B\|$
47	46	adantl	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to \exists b \in A \|y - B\| = \|b - B\|$
48		eqeq1	$⊢ a = \|y - B\| \to (a = \|b - B\| \leftrightarrow \|y - B\| = \|b - B\|)$
49	48	rexbidv	$⊢ a = \|y - B\| \to (\exists b \in A a = \|b - B\| \leftrightarrow \exists b \in A \|y - B\| = \|b - B\|)$
50	49	elrab	$⊢ \|y - B\| \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \leftrightarrow (\|y - B\| \in ℝ \land \exists b \in A \|y - B\| = \|b - B\|)$
51	42 47 50	sylanbrc	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to \|y - B\| \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\}$
52	51	ne0d	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \neq \emptyset$
53	34 52	exlimddv	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \neq \emptyset$
54		ssrab2	$⊢ \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \subseteq ℝ$
55	54	a1i	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \subseteq ℝ$
56		gtso	$⊢ <^{-1} Or ℝ$
57		fisupcl	$⊢ (<^{-1} Or ℝ \land (\{a \in ℝ \| \exists b \in A a = \|b - B\|\} \in Fin \land \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \neq \emptyset \land \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \subseteq ℝ)) \to sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}) \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\}$
58	56 57	mpan	$⊢ (\{a \in ℝ \| \exists b \in A a = \|b - B\|\} \in Fin \land \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \neq \emptyset \land \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \subseteq ℝ) \to sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}) \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\}$
59	31 53 55 58	syl3anc	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}) \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\}$
60	26 59	sseldd	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}) \in ℝ^{+}$
61	54	a1i	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \subseteq ℝ$
62		soss	$⊢ \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \subseteq ℝ \to (<^{-1} Or ℝ \to <^{-1} Or \{a \in ℝ \| \exists b \in A a = \|b - B\|\})$
63	54 56 62	mp2	$⊢ <^{-1} Or \{a \in ℝ \| \exists b \in A a = \|b - B\|\}$
64	63	a1i	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to <^{-1} Or \{a \in ℝ \| \exists b \in A a = \|b - B\|\}$
65		fisupg	$⊢ (<^{-1} Or \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \land \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \in Fin \land \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \neq \emptyset) \to \exists c \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} (\forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \neg c <^{-1} d \land \forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} (d <^{-1} c \to \exists x \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} d <^{-1} x))$
66	64 31 53 65	syl3anc	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to \exists c \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} (\forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \neg c <^{-1} d \land \forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} (d <^{-1} c \to \exists x \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} d <^{-1} x))$
67		elrabi	$⊢ c \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \to c \in ℝ$
68		elrabi	$⊢ d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \to d \in ℝ$
69		vex	$⊢ c \in V$
70		vex	$⊢ d \in V$
71	69 70	brcnv	$⊢ c <^{-1} d \leftrightarrow d < c$
72	71	notbii	$⊢ \neg c <^{-1} d \leftrightarrow \neg d < c$
73		lenlt	$⊢ (c \in ℝ \land d \in ℝ) \to (c \leq d \leftrightarrow \neg d < c)$
74	73	biimprd	$⊢ (c \in ℝ \land d \in ℝ) \to (\neg d < c \to c \leq d)$
75	72 74	biimtrid	$⊢ (c \in ℝ \land d \in ℝ) \to (\neg c <^{-1} d \to c \leq d)$
76	75	adantll	$⊢ (((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land c \in ℝ) \land d \in ℝ) \to (\neg c <^{-1} d \to c \leq d)$
77	68 76	sylan2	$⊢ (((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land c \in ℝ) \land d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\}) \to (\neg c <^{-1} d \to c \leq d)$
78	77	ralimdva	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land c \in ℝ) \to (\forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \neg c <^{-1} d \to \forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} c \leq d)$
79	78	adantrd	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land c \in ℝ) \to ((\forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \neg c <^{-1} d \land \forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} (d <^{-1} c \to \exists x \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} d <^{-1} x)) \to \forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} c \leq d)$
80	67 79	sylan2	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land c \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\}) \to ((\forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \neg c <^{-1} d \land \forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} (d <^{-1} c \to \exists x \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} d <^{-1} x)) \to \forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} c \leq d)$
81	80	reximdva	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to (\exists c \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} (\forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \neg c <^{-1} d \land \forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} (d <^{-1} c \to \exists x \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} d <^{-1} x)) \to \exists c \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} c \leq d)$
82	66 81	mpd	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to \exists c \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} c \leq d$
83	82	adantr	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to \exists c \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} c \leq d$
84		lbinfle	$⊢ (\{a \in ℝ \| \exists b \in A a = \|b - B\|\} \subseteq ℝ \land \exists c \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} \forall d \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\} c \leq d \land \|y - B\| \in \{a \in ℝ \| \exists b \in A a = \|b - B\|\}) \to inf (\{a \in ℝ \| \exists b \in A a = \|b - B\|\} ℝ <) \leq \|y - B\|$
85	61 83 51 84	syl3anc	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to inf (\{a \in ℝ \| \exists b \in A a = \|b - B\|\} ℝ <) \leq \|y - B\|$
86		df-inf	$⊢ inf (\{a \in ℝ \| \exists b \in A a = \|b - B\|\} ℝ <) = sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1})$
87	86	eqcomi	$⊢ sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}) = inf (\{a \in ℝ \| \exists b \in A a = \|b - B\|\} ℝ <)$
88	87	breq1i	$⊢ sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}) \leq \|y - B\| \leftrightarrow inf (\{a \in ℝ \| \exists b \in A a = \|b - B\|\} ℝ <) \leq \|y - B\|$
89	85 88	sylibr	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}) \leq \|y - B\|$
90	54 59	sselid	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}) \in ℝ$
91	90	adantr	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}) \in ℝ$
92	91 42	lenltd	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to (sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}) \leq \|y - B\| \leftrightarrow \neg \|y - B\| < sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}))$
93	89 92	mpbid	$⊢ ((((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \land y \in A) \to \neg \|y - B\| < sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1})$
94	93	ralrimiva	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to \forall y \in A \neg \|y - B\| < sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1})$
95		breq2	$⊢ x = sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}) \to (\|y - B\| < x \leftrightarrow \|y - B\| < sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}))$
96	95	notbid	$⊢ x = sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}) \to (\neg \|y - B\| < x \leftrightarrow \neg \|y - B\| < sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}))$
97	96	ralbidv	$⊢ x = sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}) \to (\forall y \in A \neg \|y - B\| < x \leftrightarrow \forall y \in A \neg \|y - B\| < sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}))$
98	97	rspcev	$⊢ (sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1}) \in ℝ^{+} \land \forall y \in A \neg \|y - B\| < sup (\{a \in ℝ \| \exists b \in A a = \|b - B\|\}, ℝ, <^{-1})) \to \exists x \in ℝ^{+} \forall y \in A \neg \|y - B\| < x$
99	60 94 98	syl2anc	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to \exists x \in ℝ^{+} \forall y \in A \neg \|y - B\| < x$
100		ralnex	$⊢ \forall y \in A \neg \|y - B\| < x \leftrightarrow \neg \exists y \in A \|y - B\| < x$
101	100	rexbii	$⊢ \exists x \in ℝ^{+} \forall y \in A \neg \|y - B\| < x \leftrightarrow \exists x \in ℝ^{+} \neg \exists y \in A \|y - B\| < x$
102		rexnal	$⊢ \exists x \in ℝ^{+} \neg \exists y \in A \|y - B\| < x \leftrightarrow \neg \forall x \in ℝ^{+} \exists y \in A \|y - B\| < x$
103	101 102	bitri	$⊢ \exists x \in ℝ^{+} \forall y \in A \neg \|y - B\| < x \leftrightarrow \neg \forall x \in ℝ^{+} \exists y \in A \|y - B\| < x$
104	99 103	sylib	$⊢ (((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \land A \in Fin) \to \neg \forall x \in ℝ^{+} \exists y \in A \|y - B\| < x$
105	104	ex	$⊢ ((A \subseteq ℝ \land B \in ℝ) \land (A \neq \emptyset \land \neg B \in A)) \to (A \in Fin \to \neg \forall x \in ℝ^{+} \exists y \in A \|y - B\| < x)$
106	105	3impa	$⊢ (A \subseteq ℝ \land B \in ℝ \land (A \neq \emptyset \land \neg B \in A)) \to (A \in Fin \to \neg \forall x \in ℝ^{+} \exists y \in A \|y - B\| < x)$
107	106	con2d	$⊢ (A \subseteq ℝ \land B \in ℝ \land (A \neq \emptyset \land \neg B \in A)) \to (\forall x \in ℝ^{+} \exists y \in A \|y - B\| < x \to \neg A \in Fin)$
108	107	imp	$⊢ ((A \subseteq ℝ \land B \in ℝ \land (A \neq \emptyset \land \neg B \in A)) \land \forall x \in ℝ^{+} \exists y \in A \|y - B\| < x) \to \neg A \in Fin$

Metamath Proof Explorer

Theorem rencldnfilem

Proof