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 ( 𝜑 → ( 𝑈𝐽𝑇𝑈 ) )