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	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐽 ∧ 𝑇 ⊆ 𝑈 ) )