Theorem tmslem

Description: Lemma for tmsbas , tmsds , and tmstopn . (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	tmsval.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ }
	tmsval.k	⊢ 𝐾 = ( toMetSp ‘ 𝐷 )
Assertion	tmslem	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋 = ( Base ‘ 𝐾 ) ∧ 𝐷 = ( dist ‘ 𝐾 ) ∧ ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tmsval.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ }
2		tmsval.k	⊢ 𝐾 = ( toMetSp ‘ 𝐷 )
3		elfvdm	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
4		df-ds	⊢ dist = Slot ; 1 2
5		1nn	⊢ 1 ∈ ℕ
6		2nn0	⊢ 2 ∈ ℕ0
7		1nn0	⊢ 1 ∈ ℕ0
8		1lt10	⊢ 1 < ; 1 0
9	5 6 7 8	declti	⊢ 1 < ; 1 2
10		2nn	⊢ 2 ∈ ℕ
11	7 10	decnncl	⊢ ; 1 2 ∈ ℕ
12	1 4 9 11	2strbas	⊢ ( 𝑋 ∈ dom ∞Met → 𝑋 = ( Base ‘ 𝑀 ) )
13	3 12	syl	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ( Base ‘ 𝑀 ) )
14		xmetf	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
15		ffn	⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → 𝐷 Fn ( 𝑋 × 𝑋 ) )
16		fnresdm	⊢ ( 𝐷 Fn ( 𝑋 × 𝑋 ) → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = 𝐷 )
17	14 15 16	3syl	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = 𝐷 )
18	1 4 9 11	2strop	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 = ( dist ‘ 𝑀 ) )
19	18	reseq1d	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
20	17 19	eqtr3d	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
21	1 2	tmsval	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐾 = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )
22	13 20 21	setsmsbas	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ( Base ‘ 𝐾 ) )
23	13 20 21	setsmsds	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( dist ‘ 𝑀 ) = ( dist ‘ 𝐾 ) )
24	18 23	eqtrd	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 = ( dist ‘ 𝐾 ) )
25		prex	⊢ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∈ V
26	1 25	eqeltri	⊢ 𝑀 ∈ V
27	26	a1i	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑀 ∈ V )
28	13 20 21 27	setsmstopn	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐾 ) )
29	22 24 28	3jca	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋 = ( Base ‘ 𝐾 ) ∧ 𝐷 = ( dist ‘ 𝐾 ) ∧ ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐾 ) ) )