This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
metdscn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
metnrmlem.1 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
metnrmlem.2 ⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
metnrmlem.3 ⊢ ( 𝜑 → 𝑇 ∈ ( Clsd ‘ 𝐽 ) )
metnrmlem.4 ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )
metnrmlem.u ⊢ 𝑈 = ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) )
Assertion metnrmlem2 ( 𝜑 → ( 𝑈 ∈ 𝐽 ∧ 𝑇 ⊆ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 metdscn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
2 metdscn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3 metnrmlem.1 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
4 metnrmlem.2 ⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
5 metnrmlem.3 ⊢ ( 𝜑 → 𝑇 ∈ ( Clsd ‘ 𝐽 ) )
6 metnrmlem.4 ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )
7 metnrmlem.u ⊢ 𝑈 = ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) )
8 2 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
9 3 8 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
11 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
12 11 cldss ⊢ ( 𝑇 ∈ ( Clsd ‘ 𝐽 ) → 𝑇 ⊆ ∪ 𝐽 )
13 5 12 syl ⊢ ( 𝜑 → 𝑇 ⊆ ∪ 𝐽 )
14 2 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
15 3 14 syl ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
16 13 15 sseqtrrd ⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 )
17 16 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑋 )
18 1 2 3 4 5 6 metnrmlem1a ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 0 < ( 𝐹 ‘ 𝑡 ) ∧ if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ+ ) )
19 18 simprd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ+ )
20 19 rphalfcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ∈ ℝ+ )
21 20 rpxrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ∈ ℝ* )
22 2 blopn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑡 ∈ 𝑋 ∧ ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ∈ ℝ* ) → ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ∈ 𝐽 )
23 10 17 21 22 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ∈ 𝐽 )
24 23 ralrimiva ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ∈ 𝐽 )
25 iunopn ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ∈ 𝐽 ) → ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ∈ 𝐽 )
26 9 24 25 syl2anc ⊢ ( 𝜑 → ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ∈ 𝐽 )
27 7 26 eqeltrid ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
28 blcntr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑡 ∈ 𝑋 ∧ ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ∈ ℝ+ ) → 𝑡 ∈ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) )
29 10 17 20 28 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) )
30 29 snssd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → { 𝑡 } ⊆ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) )
31 30 ralrimiva ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 { 𝑡 } ⊆ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) )
32 ss2iun ⊢ ( ∀ 𝑡 ∈ 𝑇 { 𝑡 } ⊆ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) → ∪ 𝑡 ∈ 𝑇 { 𝑡 } ⊆ ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) )
33 31 32 syl ⊢ ( 𝜑 → ∪ 𝑡 ∈ 𝑇 { 𝑡 } ⊆ ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) )
34 iunid ⊢ ∪ 𝑡 ∈ 𝑇 { 𝑡 } = 𝑇
35 34 eqcomi ⊢ 𝑇 = ∪ 𝑡 ∈ 𝑇 { 𝑡 }
36 33 35 7 3sstr4g ⊢ ( 𝜑 → 𝑇 ⊆ 𝑈 )
37 27 36 jca ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐽 ∧ 𝑇 ⊆ 𝑈 ) )