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 \in ⋃ ran ∞Met \leftrightarrow D \in ∞Met (dom dom D)$

Step	Hyp	Ref	Expression
1		ovex	$⊢ {ℝ^{*}}^{(x \times x)} \in V$
2	1	rabex	$⊢ \{d \in ({ℝ^{*}}^{(x \times x)}) \| \forall y \in x \forall z \in x ((y d z = 0 \leftrightarrow y = z) \land \forall w \in x y d z \leq (w d y) +_{𝑒} (w d z))\} \in V$
3		df-xmet	$⊢ ∞Met = (x \in V ⟼ \{d \in ({ℝ^{*}}^{(x \times x)}) \| \forall y \in x \forall z \in x ((y d z = 0 \leftrightarrow y = z) \land \forall w \in x y d z \leq (w d y) +_{𝑒} (w d z))\})$
4	2 3	fnmpti	$⊢ ∞Met Fn V$
5		fnunirn	$⊢ ∞Met Fn V \to (D \in ⋃ ran ∞Met \leftrightarrow \exists x \in V D \in ∞Met (x))$
6	4 5	ax-mp	$⊢ D \in ⋃ ran ∞Met \leftrightarrow \exists x \in V D \in ∞Met (x)$
7		id	$⊢ D \in ∞Met (x) \to D \in ∞Met (x)$
8		xmetdmdm	$⊢ D \in ∞Met (x) \to x = dom dom D$
9	8	fveq2d	$⊢ D \in ∞Met (x) \to ∞Met (x) = ∞Met (dom dom D)$
10	7 9	eleqtrd	$⊢ D \in ∞Met (x) \to D \in ∞Met (dom dom D)$
11	10	rexlimivw	$⊢ \exists x \in V D \in ∞Met (x) \to D \in ∞Met (dom dom D)$
12	6 11	sylbi	$⊢ D \in ⋃ ran ∞Met \to D \in ∞Met (dom dom D)$
13		fvssunirn	$⊢ ∞Met (dom dom D) \subseteq ⋃ ran ∞Met$
14	13	sseli	$⊢ D \in ∞Met (dom dom D) \to D \in ⋃ ran ∞Met$
15	12 14	impbii	$⊢ D \in ⋃ ran ∞Met \leftrightarrow D \in ∞Met (dom dom D)$

Metamath Proof Explorer