Metamath Proof Explorer

Theorem imasdsfn

Description: The distance function is a function on the base set. (Contributed by Mario Carneiro, 20-Aug-2015) (Proof shortened by AV, 6-Oct-2020)

Ref Expression
Hypotheses imasbas.u ⊢ φ → U = F “ 𝑠 R
imasbas.v ⊢ φ → V = Base R
imasbas.f ⊢ φ → F : V ⟶ onto B
imasbas.r ⊢ φ → R ∈ Z
imasds.e ⊢ E = dist ⁡ R
imasds.d ⊢ D = dist ⁡ U
Assertion imasdsfn ⊢ φ → D Fn B × B

Proof

Step Hyp Ref Expression
1 imasbas.u ⊢ φ → U = F “ 𝑠 R
2 imasbas.v ⊢ φ → V = Base R
3 imasbas.f ⊢ φ → F : V ⟶ onto B
4 imasbas.r ⊢ φ → R ∈ Z
5 imasds.e ⊢ E = dist ⁡ R
6 imasds.d ⊢ D = dist ⁡ U
7 eqid ⊢ x ∈ B , y ∈ B ⟼ inf ⋃ n ∈ ℕ ran ⁡ g ∈ h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = x ∧ F ⁡ 2 nd ⁡ h ⁡ n = y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 ⟼ ∑ ℝ 𝑠 * E ∘ g ℝ * < = x ∈ B , y ∈ B ⟼ inf ⋃ n ∈ ℕ ran ⁡ g ∈ h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = x ∧ F ⁡ 2 nd ⁡ h ⁡ n = y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 ⟼ ∑ ℝ 𝑠 * E ∘ g ℝ * <
8 xrltso ⊢ < Or ℝ *
9 8 infex ⊢ inf ⋃ n ∈ ℕ ran ⁡ g ∈ h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = x ∧ F ⁡ 2 nd ⁡ h ⁡ n = y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 ⟼ ∑ ℝ 𝑠 * E ∘ g ℝ * < ∈ V
10 7 9 fnmpoi ⊢ x ∈ B , y ∈ B ⟼ inf ⋃ n ∈ ℕ ran ⁡ g ∈ h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = x ∧ F ⁡ 2 nd ⁡ h ⁡ n = y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 ⟼ ∑ ℝ 𝑠 * E ∘ g ℝ * < Fn B × B
11 1 2 3 4 5 6 imasds ⊢ φ → D = x ∈ B , y ∈ B ⟼ inf ⋃ n ∈ ℕ ran ⁡ g ∈ h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = x ∧ F ⁡ 2 nd ⁡ h ⁡ n = y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 ⟼ ∑ ℝ 𝑠 * E ∘ g ℝ * <
12 11 fneq1d ⊢ φ → D Fn B × B ↔ x ∈ B , y ∈ B ⟼ inf ⋃ n ∈ ℕ ran ⁡ g ∈ h ∈ V × V 1 … n | F ⁡ 1 st ⁡ h ⁡ 1 = x ∧ F ⁡ 2 nd ⁡ h ⁡ n = y ∧ ∀ i ∈ 1 … n − 1 F ⁡ 2 nd ⁡ h ⁡ i = F ⁡ 1 st ⁡ h ⁡ i + 1 ⟼ ∑ ℝ 𝑠 * E ∘ g ℝ * < Fn B × B
13 10 12 mpbiri ⊢ φ → D Fn B × B