Metamath Proof Explorer

Theorem metsscmetcld

Description: A complete subspace of a metric space is closed in the parent space. Formerly part of proof for cmetss . (Contributed by NM, 28-Jan-2008) (Revised by Mario Carneiro, 15-Oct-2015) (Revised by AV, 9-Oct-2022)

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

Proof

Step Hyp Ref Expression
1 metsscmetcld.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3 2 adantr ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
4 1 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5 3 4 syl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6 resss ⊢ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ⊆ 𝐷
7 dmss ⊢ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ⊆ 𝐷 → dom ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ⊆ dom 𝐷 )
8 dmss ⊢ ( dom ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ⊆ dom 𝐷 → dom dom ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ⊆ dom dom 𝐷 )
9 6 7 8 mp2b ⊢ dom dom ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ⊆ dom dom 𝐷
10 cmetmet ⊢ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Met ‘ 𝑌 ) )
11 metdmdm ⊢ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Met ‘ 𝑌 ) → 𝑌 = dom dom ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) )
12 10 11 syl ⊢ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) → 𝑌 = dom dom ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) )
13 metdmdm ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝑋 = dom dom 𝐷 )
14 sseq12 ⊢ ( ( 𝑌 = dom dom ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∧ 𝑋 = dom dom 𝐷 ) → ( 𝑌 ⊆ 𝑋 ↔ dom dom ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ⊆ dom dom 𝐷 ) )
15 12 13 14 syl2anr ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → ( 𝑌 ⊆ 𝑋 ↔ dom dom ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ⊆ dom dom 𝐷 ) )
16 9 15 mpbiri ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → 𝑌 ⊆ 𝑋 )
17 flimcls ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑌 ) ↔ ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) )
18 5 16 17 syl2anc ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑌 ) ↔ ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) )
19 simprrr ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝑥 ∈ ( 𝐽 fLim 𝑓 ) )
20 3 adantr ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
21 1 methaus ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Haus )
22 hausflimi ⊢ ( 𝐽 ∈ Haus → ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) )
23 20 21 22 3syl ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) )
24 20 4 syl ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
25 simprl ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
26 simprrl ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝑌 ∈ 𝑓 )
27 flimrest ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑓 ) → ( ( 𝐽 ↾t 𝑌 ) fLim ( 𝑓 ↾t 𝑌 ) ) = ( ( 𝐽 fLim 𝑓 ) ∩ 𝑌 ) )
28 24 25 26 27 syl3anc ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → ( ( 𝐽 ↾t 𝑌 ) fLim ( 𝑓 ↾t 𝑌 ) ) = ( ( 𝐽 fLim 𝑓 ) ∩ 𝑌 ) )
29 16 adantr ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝑌 ⊆ 𝑋 )
30 eqid ⊢ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) = ( 𝐷 ↾ ( 𝑌 × 𝑌 ) )
31 eqid ⊢ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) )
32 30 1 31 metrest ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑌 ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )
33 20 29 32 syl2anc ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → ( 𝐽 ↾t 𝑌 ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )
34 33 oveq1d ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → ( ( 𝐽 ↾t 𝑌 ) fLim ( 𝑓 ↾t 𝑌 ) ) = ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) fLim ( 𝑓 ↾t 𝑌 ) ) )
35 28 34 eqtr3d ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → ( ( 𝐽 fLim 𝑓 ) ∩ 𝑌 ) = ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) fLim ( 𝑓 ↾t 𝑌 ) ) )
36 simplr ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) )
37 1 flimcfil ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) → 𝑓 ∈ ( CauFil ‘ 𝐷 ) )
38 20 19 37 syl2anc ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝑓 ∈ ( CauFil ‘ 𝐷 ) )
39 cfilres ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝑓 ) → ( 𝑓 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝑓 ↾t 𝑌 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )
40 20 25 26 39 syl3anc ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → ( 𝑓 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝑓 ↾t 𝑌 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )
41 38 40 mpbid ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → ( 𝑓 ↾t 𝑌 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )
42 31 cmetcvg ⊢ ( ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ∧ ( 𝑓 ↾t 𝑌 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) fLim ( 𝑓 ↾t 𝑌 ) ) ≠ ∅ )
43 36 41 42 syl2anc ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) fLim ( 𝑓 ↾t 𝑌 ) ) ≠ ∅ )
44 35 43 eqnetrd ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → ( ( 𝐽 fLim 𝑓 ) ∩ 𝑌 ) ≠ ∅ )
45 ndisj ⊢ ( ( ( 𝐽 fLim 𝑓 ) ∩ 𝑌 ) ≠ ∅ ↔ ∃ 𝑥 ( 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ∧ 𝑥 ∈ 𝑌 ) )
46 44 45 sylib ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → ∃ 𝑥 ( 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ∧ 𝑥 ∈ 𝑌 ) )
47 mopick ⊢ ( ( ∃* 𝑥 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ∧ ∃ 𝑥 ( 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ∧ 𝑥 ∈ 𝑌 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝑓 ) → 𝑥 ∈ 𝑌 ) )
48 23 46 47 syl2anc ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝑓 ) → 𝑥 ∈ 𝑌 ) )
49 19 48 mpd ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) ) → 𝑥 ∈ 𝑌 )
50 49 rexlimdvaa ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → ( ∃ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑌 ∈ 𝑓 ∧ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) → 𝑥 ∈ 𝑌 ) )
51 18 50 sylbid ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑌 ) → 𝑥 ∈ 𝑌 ) )
52 51 ssrdv ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑌 ) ⊆ 𝑌 )
53 1 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
54 3 53 syl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → 𝐽 ∈ Top )
55 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
56 3 55 syl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → 𝑋 = ∪ 𝐽 )
57 16 56 sseqtrd ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → 𝑌 ⊆ ∪ 𝐽 )
58 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
59 58 iscld4 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ ∪ 𝐽 ) → ( 𝑌 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑌 ) ⊆ 𝑌 ) )
60 54 57 59 syl2anc ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → ( 𝑌 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑌 ) ⊆ 𝑌 ) )
61 52 60 mpbird ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( CMet ‘ 𝑌 ) ) → 𝑌 ∈ ( Clsd ‘ 𝐽 ) )