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 df-ss ⊒ ( ( 𝐽 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 β€˜ 𝐽 ) ) )