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 𝐷 ) )