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

Metamath Proof Explorer

Theorem cfilfval

Description: The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion cfilfval ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( CauFil ‘ 𝐷 ) = { 𝑓 ∈ ( Fil ‘ 𝑋 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 fvssunirn ⊢ ( ∞Met ‘ 𝑋 ) ⊆ ∪ ran ∞Met
2 1 sseli ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ∪ ran ∞Met )
3 dmeq ⊢ ( 𝑑 = 𝐷 → dom 𝑑 = dom 𝐷 )
4 3 dmeqd ⊢ ( 𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷 )
5 4 fveq2d ⊢ ( 𝑑 = 𝐷 → ( Fil ‘ dom dom 𝑑 ) = ( Fil ‘ dom dom 𝐷 ) )
6 imaeq1 ⊢ ( 𝑑 = 𝐷 → ( 𝑑 “ ( 𝑦 × 𝑦 ) ) = ( 𝐷 “ ( 𝑦 × 𝑦 ) ) )
7 6 sseq1d ⊢ ( 𝑑 = 𝐷 → ( ( 𝑑 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ↔ ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
8 7 rexbidv ⊢ ( 𝑑 = 𝐷 → ( ∃ 𝑦 ∈ 𝑓 ( 𝑑 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ↔ ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
9 8 ralbidv ⊢ ( 𝑑 = 𝐷 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝑑 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) )
10 5 9 rabeqbidv ⊢ ( 𝑑 = 𝐷 → { 𝑓 ∈ ( Fil ‘ dom dom 𝑑 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝑑 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } = { 𝑓 ∈ ( Fil ‘ dom dom 𝐷 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } )
11 df-cfil ⊢ CauFil = ( 𝑑 ∈ ∪ ran ∞Met ↦ { 𝑓 ∈ ( Fil ‘ dom dom 𝑑 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝑑 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } )
12 fvex ⊢ ( Fil ‘ dom dom 𝐷 ) ∈ V
13 12 rabex ⊢ { 𝑓 ∈ ( Fil ‘ dom dom 𝐷 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } ∈ V
14 10 11 13 fvmpt ⊢ ( 𝐷 ∈ ∪ ran ∞Met → ( CauFil ‘ 𝐷 ) = { 𝑓 ∈ ( Fil ‘ dom dom 𝐷 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } )
15 2 14 syl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( CauFil ‘ 𝐷 ) = { 𝑓 ∈ ( Fil ‘ dom dom 𝐷 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } )
16 xmetdmdm ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = dom dom 𝐷 )
17 16 fveq2d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( Fil ‘ 𝑋 ) = ( Fil ‘ dom dom 𝐷 ) )
18 17 rabeqdv ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → { 𝑓 ∈ ( Fil ‘ 𝑋 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } = { 𝑓 ∈ ( Fil ‘ dom dom 𝐷 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } )
19 15 18 eqtr4d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( CauFil ‘ 𝐷 ) = { 𝑓 ∈ ( Fil ‘ 𝑋 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } )