iccntr

Description: The interior of a closed interval in the standard topology on RR is the corresponding open interval. (Contributed by Mario Carneiro, 1-Sep-2014)

		Ref	Expression
	Assertion	iccntr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$

Proof

Step	Hyp	Ref	Expression
1		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
2		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
3		icc0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B] = \emptyset \leftrightarrow B < A)$
4	1 2 3	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to ([A, B] = \emptyset \leftrightarrow B < A)$
5	4	biimpar	$⊢ ((A \in ℝ \land B \in ℝ) \land B < A) \to [A, B] = \emptyset$
6	5	fveq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land B < A) \to int (topGen (ran (.))) ([A, B]) = int (topGen (ran (.))) (\emptyset)$
7		retop	$⊢ topGen (ran (.)) \in Top$
8		ntr0	$⊢ topGen (ran (.)) \in Top \to int (topGen (ran (.))) (\emptyset) = \emptyset$
9	7 8	ax-mp	$⊢ int (topGen (ran (.))) (\emptyset) = \emptyset$
10		0ss	$⊢ \emptyset \subseteq \{A, B\} \cup (A, B)$
11	9 10	eqsstri	$⊢ int (topGen (ran (.))) (\emptyset) \subseteq \{A, B\} \cup (A, B)$
12	6 11	eqsstrdi	$⊢ ((A \in ℝ \land B \in ℝ) \land B < A) \to int (topGen (ran (.))) ([A, B]) \subseteq \{A, B\} \cup (A, B)$
13		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
14		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
15	14	ntrss2	$⊢ (topGen (ran (.)) \in Top \land [A, B] \subseteq ℝ) \to int (topGen (ran (.))) ([A, B]) \subseteq [A, B]$
16	7 13 15	sylancr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) \subseteq [A, B]$
17	16	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land A \leq B) \to int (topGen (ran (.))) ([A, B]) \subseteq [A, B]$
18	1 2	anim12i	$⊢ (A \in ℝ \land B \in ℝ) \to (A \in ℝ^{} \land B \in ℝ^{})$
19		uncom	$⊢ \{A, B\} \cup (A, B) = (A, B) \cup \{A, B\}$
20		prunioo	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A, B) \cup \{A, B\} = [A, B]$
21	19 20	eqtrid	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to \{A, B\} \cup (A, B) = [A, B]$
22	21	3expa	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land A \leq B) \to \{A, B\} \cup (A, B) = [A, B]$
23	18 22	sylan	$⊢ ((A \in ℝ \land B \in ℝ) \land A \leq B) \to \{A, B\} \cup (A, B) = [A, B]$
24	17 23	sseqtrrd	$⊢ ((A \in ℝ \land B \in ℝ) \land A \leq B) \to int (topGen (ran (.))) ([A, B]) \subseteq \{A, B\} \cup (A, B)$
25		simpr	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℝ$
26		simpl	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℝ$
27	12 24 25 26	ltlecasei	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) \subseteq \{A, B\} \cup (A, B)$
28	14	ntropn	$⊢ (topGen (ran (.)) \in Top \land [A, B] \subseteq ℝ) \to int (topGen (ran (.))) ([A, B]) \in topGen (ran (.))$
29	7 13 28	sylancr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) \in topGen (ran (.))$
30		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
31	30	rexmet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
32		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
33	30 32	tgioo	$⊢ topGen (ran (.)) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
34	33	mopni2	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land int (topGen (ran (.))) ([A, B]) \in topGen (ran (.)) \land A \in int (topGen (ran (.))) ([A, B])) \to \exists x \in ℝ^{+} A ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B])$
35	31 34	mp3an1	$⊢ (int (topGen (ran (.))) ([A, B]) \in topGen (ran (.)) \land A \in int (topGen (ran (.))) ([A, B])) \to \exists x \in ℝ^{+} A ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B])$
36	29 35	sylan	$⊢ ((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \to \exists x \in ℝ^{+} A ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B])$
37	26	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to A \in ℝ$
38		rphalfcl	$⊢ x \in ℝ^{+} \to \frac{x}{2} \in ℝ^{+}$
39	38	adantl	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to \frac{x}{2} \in ℝ^{+}$
40	37 39	ltsubrpd	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to A - (\frac{x}{2}) < A$
41	39	rpred	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to \frac{x}{2} \in ℝ$
42	37 41	resubcld	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to A - (\frac{x}{2}) \in ℝ$
43	42 37	ltnled	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to (A - (\frac{x}{2}) < A \leftrightarrow \neg A \leq A - (\frac{x}{2}))$
44	40 43	mpbid	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to \neg A \leq A - (\frac{x}{2})$
45		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
46	45	adantl	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to x \in ℝ$
47		rphalflt	$⊢ x \in ℝ^{+} \to \frac{x}{2} < x$
48	47	adantl	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to \frac{x}{2} < x$
49	41 46 37 48	ltsub2dd	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to A - x < A - (\frac{x}{2})$
50	37 46	readdcld	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to A + x \in ℝ$
51		ltaddrp	$⊢ (A \in ℝ \land x \in ℝ^{+}) \to A < A + x$
52	37 51	sylancom	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to A < A + x$
53	42 37 50 40 52	lttrd	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to A - (\frac{x}{2}) < A + x$
54	37 46	resubcld	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to A - x \in ℝ$
55	54	rexrd	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to A - x \in ℝ^{*}$
56	50	rexrd	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to A + x \in ℝ^{*}$
57		elioo2	$⊢ (A - x \in ℝ^{} \land A + x \in ℝ^{}) \to (A - (\frac{x}{2}) \in (A - x, A + x) \leftrightarrow (A - (\frac{x}{2}) \in ℝ \land A - x < A - (\frac{x}{2}) \land A - (\frac{x}{2}) < A + x))$
58	55 56 57	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to (A - (\frac{x}{2}) \in (A - x, A + x) \leftrightarrow (A - (\frac{x}{2}) \in ℝ \land A - x < A - (\frac{x}{2}) \land A - (\frac{x}{2}) < A + x))$
59	42 49 53 58	mpbir3and	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to A - (\frac{x}{2}) \in (A - x, A + x)$
60	30	bl2ioo	$⊢ (A \in ℝ \land x \in ℝ) \to A ball ({(abs \circ -) ↾}_{ℝ^{2}}) x = (A - x, A + x)$
61	37 46 60	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to A ball ({(abs \circ -) ↾}_{ℝ^{2}}) x = (A - x, A + x)$
62	59 61	eleqtrrd	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to A - (\frac{x}{2}) \in (A ball ({(abs \circ -) ↾}_{ℝ^{2}}) x)$
63		ssel	$⊢ A ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B]) \to (A - (\frac{x}{2}) \in (A ball ({(abs \circ -) ↾}_{ℝ^{2}}) x) \to A - (\frac{x}{2}) \in int (topGen (ran (.))) ([A, B]))$
64	62 63	syl5com	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to (A ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B]) \to A - (\frac{x}{2}) \in int (topGen (ran (.))) ([A, B]))$
65	16	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to int (topGen (ran (.))) ([A, B]) \subseteq [A, B]$
66	65	sseld	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to (A - (\frac{x}{2}) \in int (topGen (ran (.))) ([A, B]) \to A - (\frac{x}{2}) \in [A, B])$
67		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (A - (\frac{x}{2}) \in [A, B] \leftrightarrow (A - (\frac{x}{2}) \in ℝ \land A \leq A - (\frac{x}{2}) \land A - (\frac{x}{2}) \leq B))$
68		simp2	$⊢ (A - (\frac{x}{2}) \in ℝ \land A \leq A - (\frac{x}{2}) \land A - (\frac{x}{2}) \leq B) \to A \leq A - (\frac{x}{2})$
69	67 68	biimtrdi	$⊢ (A \in ℝ \land B \in ℝ) \to (A - (\frac{x}{2}) \in [A, B] \to A \leq A - (\frac{x}{2}))$
70	69	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to (A - (\frac{x}{2}) \in [A, B] \to A \leq A - (\frac{x}{2}))$
71	64 66 70	3syld	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to (A ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B]) \to A \leq A - (\frac{x}{2}))$
72	44 71	mtod	$⊢ (((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to \neg A ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B])$
73	72	nrexdv	$⊢ ((A \in ℝ \land B \in ℝ) \land A \in int (topGen (ran (.))) ([A, B])) \to \neg \exists x \in ℝ^{+} A ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B])$
74	36 73	pm2.65da	$⊢ (A \in ℝ \land B \in ℝ) \to \neg A \in int (topGen (ran (.))) ([A, B])$
75	33	mopni2	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land int (topGen (ran (.))) ([A, B]) \in topGen (ran (.)) \land B \in int (topGen (ran (.))) ([A, B])) \to \exists x \in ℝ^{+} B ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B])$
76	31 75	mp3an1	$⊢ (int (topGen (ran (.))) ([A, B]) \in topGen (ran (.)) \land B \in int (topGen (ran (.))) ([A, B])) \to \exists x \in ℝ^{+} B ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B])$
77	29 76	sylan	$⊢ ((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \to \exists x \in ℝ^{+} B ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B])$
78	25	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to B \in ℝ$
79	38	adantl	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to \frac{x}{2} \in ℝ^{+}$
80	78 79	ltaddrpd	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to B < B + (\frac{x}{2})$
81	79	rpred	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to \frac{x}{2} \in ℝ$
82	78 81	readdcld	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to B + (\frac{x}{2}) \in ℝ$
83	78 82	ltnled	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to (B < B + (\frac{x}{2}) \leftrightarrow \neg B + (\frac{x}{2}) \leq B)$
84	80 83	mpbid	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to \neg B + (\frac{x}{2}) \leq B$
85	45	adantl	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to x \in ℝ$
86	78 85	resubcld	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to B - x \in ℝ$
87		ltsubrp	$⊢ (B \in ℝ \land x \in ℝ^{+}) \to B - x < B$
88	78 87	sylancom	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to B - x < B$
89	86 78 82 88 80	lttrd	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to B - x < B + (\frac{x}{2})$
90	47	adantl	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to \frac{x}{2} < x$
91	81 85 78 90	ltadd2dd	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to B + (\frac{x}{2}) < B + x$
92	86	rexrd	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to B - x \in ℝ^{*}$
93	78 85	readdcld	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to B + x \in ℝ$
94	93	rexrd	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to B + x \in ℝ^{*}$
95		elioo2	$⊢ (B - x \in ℝ^{} \land B + x \in ℝ^{}) \to (B + (\frac{x}{2}) \in (B - x, B + x) \leftrightarrow (B + (\frac{x}{2}) \in ℝ \land B - x < B + (\frac{x}{2}) \land B + (\frac{x}{2}) < B + x))$
96	92 94 95	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to (B + (\frac{x}{2}) \in (B - x, B + x) \leftrightarrow (B + (\frac{x}{2}) \in ℝ \land B - x < B + (\frac{x}{2}) \land B + (\frac{x}{2}) < B + x))$
97	82 89 91 96	mpbir3and	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to B + (\frac{x}{2}) \in (B - x, B + x)$
98	30	bl2ioo	$⊢ (B \in ℝ \land x \in ℝ) \to B ball ({(abs \circ -) ↾}_{ℝ^{2}}) x = (B - x, B + x)$
99	78 85 98	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to B ball ({(abs \circ -) ↾}_{ℝ^{2}}) x = (B - x, B + x)$
100	97 99	eleqtrrd	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to B + (\frac{x}{2}) \in (B ball ({(abs \circ -) ↾}_{ℝ^{2}}) x)$
101		ssel	$⊢ B ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B]) \to (B + (\frac{x}{2}) \in (B ball ({(abs \circ -) ↾}_{ℝ^{2}}) x) \to B + (\frac{x}{2}) \in int (topGen (ran (.))) ([A, B]))$
102	100 101	syl5com	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to (B ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B]) \to B + (\frac{x}{2}) \in int (topGen (ran (.))) ([A, B]))$
103	16	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to int (topGen (ran (.))) ([A, B]) \subseteq [A, B]$
104	103	sseld	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to (B + (\frac{x}{2}) \in int (topGen (ran (.))) ([A, B]) \to B + (\frac{x}{2}) \in [A, B])$
105		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (B + (\frac{x}{2}) \in [A, B] \leftrightarrow (B + (\frac{x}{2}) \in ℝ \land A \leq B + (\frac{x}{2}) \land B + (\frac{x}{2}) \leq B))$
106		simp3	$⊢ (B + (\frac{x}{2}) \in ℝ \land A \leq B + (\frac{x}{2}) \land B + (\frac{x}{2}) \leq B) \to B + (\frac{x}{2}) \leq B$
107	105 106	biimtrdi	$⊢ (A \in ℝ \land B \in ℝ) \to (B + (\frac{x}{2}) \in [A, B] \to B + (\frac{x}{2}) \leq B)$
108	107	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to (B + (\frac{x}{2}) \in [A, B] \to B + (\frac{x}{2}) \leq B)$
109	102 104 108	3syld	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to (B ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B]) \to B + (\frac{x}{2}) \leq B)$
110	84 109	mtod	$⊢ (((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \land x \in ℝ^{+}) \to \neg B ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B])$
111	110	nrexdv	$⊢ ((A \in ℝ \land B \in ℝ) \land B \in int (topGen (ran (.))) ([A, B])) \to \neg \exists x \in ℝ^{+} B ball ({(abs \circ -) ↾}_{ℝ^{2}}) x \subseteq int (topGen (ran (.))) ([A, B])$
112	77 111	pm2.65da	$⊢ (A \in ℝ \land B \in ℝ) \to \neg B \in int (topGen (ran (.))) ([A, B])$
113		eleq1	$⊢ x = A \to (x \in int (topGen (ran (.))) ([A, B]) \leftrightarrow A \in int (topGen (ran (.))) ([A, B]))$
114	113	notbid	$⊢ x = A \to (\neg x \in int (topGen (ran (.))) ([A, B]) \leftrightarrow \neg A \in int (topGen (ran (.))) ([A, B]))$
115		eleq1	$⊢ x = B \to (x \in int (topGen (ran (.))) ([A, B]) \leftrightarrow B \in int (topGen (ran (.))) ([A, B]))$
116	115	notbid	$⊢ x = B \to (\neg x \in int (topGen (ran (.))) ([A, B]) \leftrightarrow \neg B \in int (topGen (ran (.))) ([A, B]))$
117	114 116	ralprg	$⊢ (A \in ℝ \land B \in ℝ) \to (\forall x \in \{A, B\} \neg x \in int (topGen (ran (.))) ([A, B]) \leftrightarrow (\neg A \in int (topGen (ran (.))) ([A, B]) \land \neg B \in int (topGen (ran (.))) ([A, B])))$
118	74 112 117	mpbir2and	$⊢ (A \in ℝ \land B \in ℝ) \to \forall x \in \{A, B\} \neg x \in int (topGen (ran (.))) ([A, B])$
119		disjr	$⊢ int (topGen (ran (.))) ([A, B]) \cap \{A, B\} = \emptyset \leftrightarrow \forall x \in \{A, B\} \neg x \in int (topGen (ran (.))) ([A, B])$
120	118 119	sylibr	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) \cap \{A, B\} = \emptyset$
121		disjssun	$⊢ int (topGen (ran (.))) ([A, B]) \cap \{A, B\} = \emptyset \to (int (topGen (ran (.))) ([A, B]) \subseteq \{A, B\} \cup (A, B) \leftrightarrow int (topGen (ran (.))) ([A, B]) \subseteq (A, B))$
122	120 121	syl	$⊢ (A \in ℝ \land B \in ℝ) \to (int (topGen (ran (.))) ([A, B]) \subseteq \{A, B\} \cup (A, B) \leftrightarrow int (topGen (ran (.))) ([A, B]) \subseteq (A, B))$
123	27 122	mpbid	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) \subseteq (A, B)$
124		iooretop	$⊢ (A, B) \in topGen (ran (.))$
125		ioossicc	$⊢ (A, B) \subseteq [A, B]$
126	14	ssntr	$⊢ ((topGen (ran (.)) \in Top \land [A, B] \subseteq ℝ) \land ((A, B) \in topGen (ran (.)) \land (A, B) \subseteq [A, B])) \to (A, B) \subseteq int (topGen (ran (.))) ([A, B])$
127	124 125 126	mpanr12	$⊢ (topGen (ran (.)) \in Top \land [A, B] \subseteq ℝ) \to (A, B) \subseteq int (topGen (ran (.))) ([A, B])$
128	7 13 127	sylancr	$⊢ (A \in ℝ \land B \in ℝ) \to (A, B) \subseteq int (topGen (ran (.))) ([A, B])$
129	123 128	eqssd	$⊢ (A \in ℝ \land B \in ℝ) \to int (topGen (ran (.))) ([A, B]) = (A, B)$

Metamath Proof Explorer

Theorem iccntr

Proof