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		basendxltdsndx	⊢ ( Base ‘ ndx ) < ( dist ‘ ndx )
5		dsndxnn	⊢ ( dist ‘ ndx ) ∈ ℕ
6	1 4 5	2strbas	⊢ ( 𝑋 ∈ dom ∞Met → 𝑋 = ( Base ‘ 𝑀 ) )
7	3 6	syl	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ( Base ‘ 𝑀 ) )
8		xmetf	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
9		ffn	⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → 𝐷 Fn ( 𝑋 × 𝑋 ) )
10		fnresdm	⊢ ( 𝐷 Fn ( 𝑋 × 𝑋 ) → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = 𝐷 )
11	8 9 10	3syl	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = 𝐷 )
12		dsid	⊢ dist = Slot ( dist ‘ ndx )
13	1 4 5 12	2strop	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 = ( dist ‘ 𝑀 ) )
14	13	reseq1d	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑋 × 𝑋 ) ) = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
15	11 14	eqtr3d	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
16	1 2	tmsval	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐾 = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )
17	7 15 16	setsmsbas	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ( Base ‘ 𝐾 ) )
18	7 15 16	setsmsds	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( dist ‘ 𝑀 ) = ( dist ‘ 𝐾 ) )
19	13 18	eqtrd	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 = ( dist ‘ 𝐾 ) )
20		prex	⊢ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } ∈ V
21	1 20	eqeltri	⊢ 𝑀 ∈ V
22	21	a1i	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑀 ∈ V )
23	7 15 16 22	setsmstopn	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐾 ) )
24	17 19 23	3jca	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋 = ( Base ‘ 𝐾 ) ∧ 𝐷 = ( dist ‘ 𝐾 ) ∧ ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐾 ) ) )