Theorem cnmpt2ds

Description: Continuity of the metric function; analogue of cnmpt22f which cannot be used directly because D is not necessarily a function. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	cnmpt1ds.d	⊢ 𝐷 = ( dist ‘ 𝐺 )
	cnmpt1ds.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
	cnmpt1ds.r	⊢ 𝑅 = ( topGen ‘ ran (,) )
	cnmpt1ds.g	⊢ ( 𝜑 → 𝐺 ∈ MetSp )
	cnmpt1ds.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
	cnmpt2ds.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
	cnmpt2ds.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
	cnmpt2ds.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
Assertion	cnmpt2ds	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 𝐷 𝐵 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		cnmpt1ds.d	⊢ 𝐷 = ( dist ‘ 𝐺 )
2		cnmpt1ds.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
3		cnmpt1ds.r	⊢ 𝑅 = ( topGen ‘ ran (,) )
4		cnmpt1ds.g	⊢ ( 𝜑 → 𝐺 ∈ MetSp )
5		cnmpt1ds.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
6		cnmpt2ds.l	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
7		cnmpt2ds.a	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
8		cnmpt2ds.b	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) )
9		txtopon	⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
10	5 6 9	syl2anc	⊢ ( 𝜑 → ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
11		mstps	⊢ ( 𝐺 ∈ MetSp → 𝐺 ∈ TopSp )
12	4 11	syl	⊢ ( 𝜑 → 𝐺 ∈ TopSp )
13		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
14	13 2	istps	⊢ ( 𝐺 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
15	12 14	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
16		cnf2	⊢ ( ( ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐺 ) )
17	10 15 7 16	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐺 ) )
18		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 )
19	18	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝐺 ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐴 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐺 ) )
20	17 19	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝐺 ) )
21	20	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 𝐴 ∈ ( Base ‘ 𝐺 ) )
22	21	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ ( Base ‘ 𝐺 ) )
23		cnf2	⊢ ( ( ( 𝐾 ×t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐺 ) )
24	10 15 8 23	syl3anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐺 ) )
25		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 )
26	25	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝐺 ) ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐵 ) : ( 𝑋 × 𝑌 ) ⟶ ( Base ‘ 𝐺 ) )
27	24 26	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝐺 ) )
28	27	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑌 𝐵 ∈ ( Base ‘ 𝐺 ) )
29	28	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → 𝐵 ∈ ( Base ‘ 𝐺 ) )
30	22 29	ovresd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 ( 𝐷 ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝐵 ) = ( 𝐴 𝐷 𝐵 ) )
31	30	3impa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 ( 𝐷 ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝐵 ) = ( 𝐴 𝐷 𝐵 ) )
32	31	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 ( 𝐷 ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝐵 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 𝐷 𝐵 ) ) )
33	13 1 2 3	msdcn	⊢ ( 𝐺 ∈ MetSp → ( 𝐷 ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝑅 ) )
34	4 33	syl	⊢ ( 𝜑 → ( 𝐷 ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝑅 ) )
35	5 6 7 8 34	cnmpt22f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 ( 𝐷 ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝐵 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝑅 ) )
36	32 35	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝐴 𝐷 𝐵 ) ) ∈ ( ( 𝐾 ×t 𝐿 ) Cn 𝑅 ) )