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