Metamath Proof Explorer

Theorem iscmet

Description: The property " D is a complete metric." meaning all Cauchy filters converge to a point in the space. (Contributed by Mario Carneiro, 1-May-2014) (Revised by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypothesis iscmet.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion iscmet ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 iscmet.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 elfvex ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝑋 ∈ V )
3 elfvex ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝑋 ∈ V )
4 3 adantr ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) → 𝑋 ∈ V )
5 fveq2 ⊢ ( 𝑥 = 𝑋 → ( Met ‘ 𝑥 ) = ( Met ‘ 𝑋 ) )
6 5 rabeqdv ⊢ ( 𝑥 = 𝑋 → { 𝑑 ∈ ( Met ‘ 𝑥 ) ∣ ∀ 𝑓 ∈ ( CauFil ‘ 𝑑 ) ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅ } = { 𝑑 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑓 ∈ ( CauFil ‘ 𝑑 ) ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅ } )
7 df-cmet ⊢ CMet = ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( Met ‘ 𝑥 ) ∣ ∀ 𝑓 ∈ ( CauFil ‘ 𝑑 ) ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅ } )
8 fvex ⊢ ( Met ‘ 𝑋 ) ∈ V
9 8 rabex ⊢ { 𝑑 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑓 ∈ ( CauFil ‘ 𝑑 ) ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅ } ∈ V
10 6 7 9 fvmpt ⊢ ( 𝑋 ∈ V → ( CMet ‘ 𝑋 ) = { 𝑑 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑓 ∈ ( CauFil ‘ 𝑑 ) ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅ } )
11 10 eleq2d ⊢ ( 𝑋 ∈ V → ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ↔ 𝐷 ∈ { 𝑑 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑓 ∈ ( CauFil ‘ 𝑑 ) ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅ } ) )
12 fveq2 ⊢ ( 𝑑 = 𝐷 → ( CauFil ‘ 𝑑 ) = ( CauFil ‘ 𝐷 ) )
13 fveq2 ⊢ ( 𝑑 = 𝐷 → ( MetOpen ‘ 𝑑 ) = ( MetOpen ‘ 𝐷 ) )
14 13 1 eqtr4di ⊢ ( 𝑑 = 𝐷 → ( MetOpen ‘ 𝑑 ) = 𝐽 )
15 14 oveq1d ⊢ ( 𝑑 = 𝐷 → ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) = ( 𝐽 fLim 𝑓 ) )
16 15 neeq1d ⊢ ( 𝑑 = 𝐷 → ( ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅ ↔ ( 𝐽 fLim 𝑓 ) ≠ ∅ ) )
17 12 16 raleqbidv ⊢ ( 𝑑 = 𝐷 → ( ∀ 𝑓 ∈ ( CauFil ‘ 𝑑 ) ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅ ↔ ∀ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) )
18 17 elrab ⊢ ( 𝐷 ∈ { 𝑑 ∈ ( Met ‘ 𝑋 ) ∣ ∀ 𝑓 ∈ ( CauFil ‘ 𝑑 ) ( ( MetOpen ‘ 𝑑 ) fLim 𝑓 ) ≠ ∅ } ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) )
19 11 18 bitrdi ⊢ ( 𝑋 ∈ V → ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) ) )
20 2 4 19 pm5.21nii ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) )