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 ( 𝐷 ∈ ∪ ran ∞Met ↔ 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )

Proof

Step Hyp Ref Expression
1 ovex ⊢ ( ℝ* ↑m ( 𝑥 × 𝑥 ) ) ∈ V
2 1 rabex ⊢ { 𝑑 ∈ ( ℝ* ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( ( ( 𝑦 𝑑 𝑧 ) = 0 ↔ 𝑦 = 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +𝑒 ( 𝑤 𝑑 𝑧 ) ) ) } ∈ V
3 df-xmet ⊢ ∞Met = ( 𝑥 ∈ V ↦ { 𝑑 ∈ ( ℝ* ↑m ( 𝑥 × 𝑥 ) ) ∣ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( ( ( 𝑦 𝑑 𝑧 ) = 0 ↔ 𝑦 = 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑥 ( 𝑦 𝑑 𝑧 ) ≤ ( ( 𝑤 𝑑 𝑦 ) +𝑒 ( 𝑤 𝑑 𝑧 ) ) ) } )
4 2 3 fnmpti ⊢ ∞Met Fn V
5 fnunirn ⊢ ( ∞Met Fn V → ( 𝐷 ∈ ∪ ran ∞Met ↔ ∃ 𝑥 ∈ V 𝐷 ∈ ( ∞Met ‘ 𝑥 ) ) )
6 4 5 ax-mp ⊢ ( 𝐷 ∈ ∪ ran ∞Met ↔ ∃ 𝑥 ∈ V 𝐷 ∈ ( ∞Met ‘ 𝑥 ) )
7 id ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑥 ) → 𝐷 ∈ ( ∞Met ‘ 𝑥 ) )
8 xmetdmdm ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑥 ) → 𝑥 = dom dom 𝐷 )
9 8 fveq2d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑥 ) → ( ∞Met ‘ 𝑥 ) = ( ∞Met ‘ dom dom 𝐷 ) )
10 7 9 eleqtrd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑥 ) → 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )
11 10 rexlimivw ⊢ ( ∃ 𝑥 ∈ V 𝐷 ∈ ( ∞Met ‘ 𝑥 ) → 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )
12 6 11 sylbi ⊢ ( 𝐷 ∈ ∪ ran ∞Met → 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )
13 fvssunirn ⊢ ( ∞Met ‘ dom dom 𝐷 ) ⊆ ∪ ran ∞Met
14 13 sseli ⊢ ( 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) → 𝐷 ∈ ∪ ran ∞Met )
15 12 14 impbii ⊢ ( 𝐷 ∈ ∪ ran ∞Met ↔ 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )