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 2strbas1 ⊒ ( 𝑋 ∈ 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 2strop1 ⊒ ( 𝐷 ∈ ( ∞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 β€˜ 𝐾 ) ) )