Theorem 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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )

Proof

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