Metamath Proof Explorer

Theorem tmslemOLD

Description: Obsolete version of tmslem as of 28-Oct-2024. Lemma for tmsbas , tmsds , and tmstopn . (Contributed by Mario Carneiro, 2-Sep-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses tmsval.m ⊒ 𝑀 = { ⟨ ( Base β€˜ ndx ) , 𝑋 ⟩ , ⟨ ( dist β€˜ ndx ) , 𝐷 ⟩ }
tmsval.k ⊒ 𝐾 = ( toMetSp β€˜ 𝐷 )
Assertion tmslemOLD ( 𝐷 ∈ ( ∞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 β€˜ 𝐾 ) ) )