Metamath Proof Explorer

Theorem metnrmlem2

Description: Lemma for metnrm . (Contributed by Mario Carneiro, 14-Jan-2014) (Revised by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypotheses metdscn.f ⊢F=x∈X⟼supran⁡y∈S⟼xDyℝ*<
metdscn.j ⊢J=MetOpen⁡D
metnrmlem.1 ⊢φ→D∈∞Met⁡X
metnrmlem.2 ⊢φ→S∈Clsd⁡J
metnrmlem.3 ⊢φ→T∈Clsd⁡J
metnrmlem.4 ⊢φ→S∩T=∅
metnrmlem.u ⊢U=⋃t∈Ttball⁡Dif1≤F⁡t1F⁡t2
Assertion metnrmlem2 ⊢φ→U∈J∧T⊆U

Proof

Step Hyp Ref Expression
1 metdscn.f ⊢F=x∈X⟼supran⁡y∈S⟼xDyℝ*<
2 metdscn.j ⊢J=MetOpen⁡D
3 metnrmlem.1 ⊢φ→D∈∞Met⁡X
4 metnrmlem.2 ⊢φ→S∈Clsd⁡J
5 metnrmlem.3 ⊢φ→T∈Clsd⁡J
6 metnrmlem.4 ⊢φ→S∩T=∅
7 metnrmlem.u ⊢U=⋃t∈Ttball⁡Dif1≤F⁡t1F⁡t2
8 2 mopntop ⊢D∈∞Met⁡X→J∈Top
9 3 8 syl ⊢φ→J∈Top
10 3 adantr ⊢φ∧t∈T→D∈∞Met⁡X
11 eqid ⊢⋃J=⋃J
12 11 cldss ⊢T∈Clsd⁡J→T⊆⋃J
13 5 12 syl ⊢φ→T⊆⋃J
14 2 mopnuni ⊢D∈∞Met⁡X→X=⋃J
15 3 14 syl ⊢φ→X=⋃J
16 13 15 sseqtrrd ⊢φ→T⊆X
17 16 sselda ⊢φ∧t∈T→t∈X
18 1 2 3 4 5 6 metnrmlem1a ⊢φ∧t∈T→0<F⁡t∧if1≤F⁡t1F⁡t∈ℝ+
19 18 simprd ⊢φ∧t∈T→if1≤F⁡t1F⁡t∈ℝ+
20 19 rphalfcld ⊢φ∧t∈T→if1≤F⁡t1F⁡t2∈ℝ+
21 20 rpxrd ⊢φ∧t∈T→if1≤F⁡t1F⁡t2∈ℝ*
22 2 blopn ⊢D∈∞Met⁡X∧t∈X∧if1≤F⁡t1F⁡t2∈ℝ*→tball⁡Dif1≤F⁡t1F⁡t2∈J
23 10 17 21 22 syl3anc ⊢φ∧t∈T→tball⁡Dif1≤F⁡t1F⁡t2∈J
24 23 ralrimiva ⊢φ→∀t∈Ttball⁡Dif1≤F⁡t1F⁡t2∈J
25 iunopn ⊢J∈Top∧∀t∈Ttball⁡Dif1≤F⁡t1F⁡t2∈J→⋃t∈Ttball⁡Dif1≤F⁡t1F⁡t2∈J
26 9 24 25 syl2anc ⊢φ→⋃t∈Ttball⁡Dif1≤F⁡t1F⁡t2∈J
27 7 26 eqeltrid ⊢φ→U∈J
28 blcntr ⊢D∈∞Met⁡X∧t∈X∧if1≤F⁡t1F⁡t2∈ℝ+→t∈tball⁡Dif1≤F⁡t1F⁡t2
29 10 17 20 28 syl3anc ⊢φ∧t∈T→t∈tball⁡Dif1≤F⁡t1F⁡t2
30 29 snssd ⊢φ∧t∈T→t⊆tball⁡Dif1≤F⁡t1F⁡t2
31 30 ralrimiva ⊢φ→∀t∈Tt⊆tball⁡Dif1≤F⁡t1F⁡t2
32 ss2iun ⊢∀t∈Tt⊆tball⁡Dif1≤F⁡t1F⁡t2→⋃t∈Tt⊆⋃t∈Ttball⁡Dif1≤F⁡t1F⁡t2
33 31 32 syl ⊢φ→⋃t∈Tt⊆⋃t∈Ttball⁡Dif1≤F⁡t1F⁡t2
34 iunid ⊢⋃t∈Tt=T
35 34 eqcomi ⊢T=⋃t∈Tt
36 33 35 7 3sstr4g ⊢φ→T⊆U
37 27 36 jca ⊢φ→U∈J∧T⊆U