Metamath Proof Explorer

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 ⊢A∈ℝ∧B∈ℝ→int⁡topGen⁡ran⁡.⁡AB=AB

Proof

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