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

Metamath Proof Explorer

Theorem xmetunirn

Description: Two ways to express an extended metric on an unspecified base. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion xmetunirn ⊢ D ∈ ⋃ ran ⁡ ∞Met ↔ D ∈ ∞Met ⁡ dom ⁡ dom ⁡ D

Proof

Step Hyp Ref Expression
1 ovex ⊢ ℝ * x × x ∈ V
2 1 rabex ⊢ d ∈ ℝ * x × x | ∀ y ∈ x ∀ z ∈ x y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z ∈ V
3 df-xmet ⊢ ∞Met = x ∈ V ⟼ d ∈ ℝ * x × x | ∀ y ∈ x ∀ z ∈ x y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + 𝑒 w d z
4 2 3 fnmpti ⊢ ∞Met Fn V
5 fnunirn ⊢ ∞Met Fn V → D ∈ ⋃ ran ⁡ ∞Met ↔ ∃ x ∈ V D ∈ ∞Met ⁡ x
6 4 5 ax-mp ⊢ D ∈ ⋃ ran ⁡ ∞Met ↔ ∃ x ∈ V D ∈ ∞Met ⁡ x
7 id ⊢ D ∈ ∞Met ⁡ x → D ∈ ∞Met ⁡ x
8 xmetdmdm ⊢ D ∈ ∞Met ⁡ x → x = dom ⁡ dom ⁡ D
9 8 fveq2d ⊢ D ∈ ∞Met ⁡ x → ∞Met ⁡ x = ∞Met ⁡ dom ⁡ dom ⁡ D
10 7 9 eleqtrd ⊢ D ∈ ∞Met ⁡ x → D ∈ ∞Met ⁡ dom ⁡ dom ⁡ D
11 10 rexlimivw ⊢ ∃ x ∈ V D ∈ ∞Met ⁡ x → D ∈ ∞Met ⁡ dom ⁡ dom ⁡ D
12 6 11 sylbi ⊢ D ∈ ⋃ ran ⁡ ∞Met → D ∈ ∞Met ⁡ dom ⁡ dom ⁡ D
13 fvssunirn ⊢ ∞Met ⁡ dom ⁡ dom ⁡ D ⊆ ⋃ ran ⁡ ∞Met
14 13 sseli ⊢ D ∈ ∞Met ⁡ dom ⁡ dom ⁡ D → D ∈ ⋃ ran ⁡ ∞Met
15 12 14 impbii ⊢ D ∈ ⋃ ran ⁡ ∞Met ↔ D ∈ ∞Met ⁡ dom ⁡ dom ⁡ D