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

Metamath Proof Explorer

Theorem cmetss

Description: A subspace of a complete metric space is complete iff it is closed in the parent space. Theorem 1.4-7 of Kreyszig p. 30. (Contributed by NM, 28-Jan-2008) (Revised by Mario Carneiro, 15-Oct-2015) (Proof shortened by AV, 9-Oct-2022)

Ref Expression
Hypothesis metsscmetcld.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion cmetss ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ↔ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 metsscmetcld.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3 1 metsscmetcld ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → 𝑌 ∈ ( Clsd ‘ 𝐽 ) )
4 2 3 sylan ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → 𝑌 ∈ ( Clsd ‘ 𝐽 ) )
5 2 adantr ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
6 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
7 6 cldss ⊢ ( 𝑌 ∈ ( Clsd ‘ 𝐽 ) → 𝑌 ⊆ ∪ 𝐽 )
8 7 adantl ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑌 ⊆ ∪ 𝐽 )
9 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
10 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
11 5 9 10 3syl ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑋 = ∪ 𝐽 )
12 8 11 sseqtrrd ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑌 ⊆ 𝑋 )
13 metres2 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Met ‘ 𝑌 ) )
14 5 12 13 syl2anc ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Met ‘ 𝑌 ) )
15 2 9 syl ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
16 15 ad2antrr ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
17 12 adantr ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝑌 ⊆ 𝑋 )
18 eqid ⊢ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) = ( 𝐷 ↾ ( 𝑌 × 𝑌 ) )
19 eqid ⊢ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) )
20 18 1 19 metrest ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑌 ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )
21 16 17 20 syl2anc ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( 𝐽 ↾t 𝑌 ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )
22 21 eqcomd ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) = ( 𝐽 ↾t 𝑌 ) )
23 metxmet ⊢ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Met ‘ 𝑌 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
24 14 23 syl ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
25 cfilfil ⊢ ( ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝑓 ∈ ( Fil ‘ 𝑌 ) )
26 24 25 sylan ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝑓 ∈ ( Fil ‘ 𝑌 ) )
27 elfvdm ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝑋 ∈ dom CMet )
28 27 ad2antrr ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝑋 ∈ dom CMet )
29 trfg ⊢ ( ( 𝑓 ∈ ( Fil ‘ 𝑌 ) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ dom CMet ) → ( ( 𝑋 filGen 𝑓 ) ↾t 𝑌 ) = 𝑓 )
30 26 17 28 29 syl3anc ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( ( 𝑋 filGen 𝑓 ) ↾t 𝑌 ) = 𝑓 )
31 30 eqcomd ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝑓 = ( ( 𝑋 filGen 𝑓 ) ↾t 𝑌 ) )
32 22 31 oveq12d ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) fLim 𝑓 ) = ( ( 𝐽 ↾t 𝑌 ) fLim ( ( 𝑋 filGen 𝑓 ) ↾t 𝑌 ) ) )
33 1 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
34 16 33 syl ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
35 filfbas ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑌 ) → 𝑓 ∈ ( fBas ‘ 𝑌 ) )
36 26 35 syl ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝑓 ∈ ( fBas ‘ 𝑌 ) )
37 filsspw ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑌 ) → 𝑓 ⊆ 𝒫 𝑌 )
38 26 37 syl ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝑓 ⊆ 𝒫 𝑌 )
39 17 sspwd ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝒫 𝑌 ⊆ 𝒫 𝑋 )
40 38 39 sstrd ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝑓 ⊆ 𝒫 𝑋 )
41 fbasweak ⊢ ( ( 𝑓 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑓 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ dom CMet ) → 𝑓 ∈ ( fBas ‘ 𝑋 ) )
42 36 40 28 41 syl3anc ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝑓 ∈ ( fBas ‘ 𝑋 ) )
43 fgcl ⊢ ( 𝑓 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝑓 ) ∈ ( Fil ‘ 𝑋 ) )
44 42 43 syl ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( 𝑋 filGen 𝑓 ) ∈ ( Fil ‘ 𝑋 ) )
45 ssfg ⊢ ( 𝑓 ∈ ( fBas ‘ 𝑋 ) → 𝑓 ⊆ ( 𝑋 filGen 𝑓 ) )
46 42 45 syl ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝑓 ⊆ ( 𝑋 filGen 𝑓 ) )
47 filtop ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑌 ) → 𝑌 ∈ 𝑓 )
48 26 47 syl ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝑌 ∈ 𝑓 )
49 46 48 sseldd ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝑌 ∈ ( 𝑋 filGen 𝑓 ) )
50 flimrest ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ ( 𝑋 filGen 𝑓 ) ) → ( ( 𝐽 ↾t 𝑌 ) fLim ( ( 𝑋 filGen 𝑓 ) ↾t 𝑌 ) ) = ( ( 𝐽 fLim ( 𝑋 filGen 𝑓 ) ) ∩ 𝑌 ) )
51 34 44 49 50 syl3anc ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( ( 𝐽 ↾t 𝑌 ) fLim ( ( 𝑋 filGen 𝑓 ) ↾t 𝑌 ) ) = ( ( 𝐽 fLim ( 𝑋 filGen 𝑓 ) ) ∩ 𝑌 ) )
52 flimclsi ⊢ ( 𝑌 ∈ ( 𝑋 filGen 𝑓 ) → ( 𝐽 fLim ( 𝑋 filGen 𝑓 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑌 ) )
53 49 52 syl ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( 𝐽 fLim ( 𝑋 filGen 𝑓 ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑌 ) )
54 cldcls ⊢ ( 𝑌 ∈ ( Clsd ‘ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑌 ) = 𝑌 )
55 54 ad2antlr ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑌 ) = 𝑌 )
56 53 55 sseqtrd ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( 𝐽 fLim ( 𝑋 filGen 𝑓 ) ) ⊆ 𝑌 )
57 dfss2 ⊢ ( ( 𝐽 fLim ( 𝑋 filGen 𝑓 ) ) ⊆ 𝑌 ↔ ( ( 𝐽 fLim ( 𝑋 filGen 𝑓 ) ) ∩ 𝑌 ) = ( 𝐽 fLim ( 𝑋 filGen 𝑓 ) ) )
58 56 57 sylib ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( ( 𝐽 fLim ( 𝑋 filGen 𝑓 ) ) ∩ 𝑌 ) = ( 𝐽 fLim ( 𝑋 filGen 𝑓 ) ) )
59 32 51 58 3eqtrd ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) fLim 𝑓 ) = ( 𝐽 fLim ( 𝑋 filGen 𝑓 ) ) )
60 simpll ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
61 5 9 syl ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
62 cfilresi ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( 𝑋 filGen 𝑓 ) ∈ ( CauFil ‘ 𝐷 ) )
63 61 62 sylan ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( 𝑋 filGen 𝑓 ) ∈ ( CauFil ‘ 𝐷 ) )
64 1 cmetcvg ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ ( 𝑋 filGen 𝑓 ) ∈ ( CauFil ‘ 𝐷 ) ) → ( 𝐽 fLim ( 𝑋 filGen 𝑓 ) ) ≠ ∅ )
65 60 63 64 syl2anc ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( 𝐽 fLim ( 𝑋 filGen 𝑓 ) ) ≠ ∅ )
66 59 65 eqnetrd ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) fLim 𝑓 ) ≠ ∅ )
67 66 ralrimiva ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ∀ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) fLim 𝑓 ) ≠ ∅ )
68 19 iscmet ⊢ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ↔ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Met ‘ 𝑌 ) ∧ ∀ 𝑓 ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) fLim 𝑓 ) ≠ ∅ ) )
69 14 67 68 sylanbrc ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) )
70 4 69 impbida ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ↔ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) )