This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐾 ) ) )