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	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “_s 𝑅 ) )
		imasbas.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
		imasbas.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
		imasbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
		imasds.e	⊢ 𝐸 = ( dist ‘ 𝑅 )
		imasds.d	⊢ 𝐷 = ( dist ‘ 𝑈 )
	Assertion	imasdsfn	⊢ ( 𝜑 → 𝐷 Fn ( 𝐵 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		imasbas.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “_s 𝑅 ) )
2		imasbas.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		imasbas.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
4		imasbas.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑍 )
5		imasds.e	⊢ 𝐸 = ( dist ‘ 𝑅 )
6		imasds.d	⊢ 𝐷 = ( dist ‘ 𝑈 )
7		eqid	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) )
8		xrltso	⊢ < Or ℝ^*
9	8	infex	⊢ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ∈ V
10	7 9	fnmpoi	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) Fn ( 𝐵 × 𝐵 )
11	1 2 3 4 5 6	imasds	⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) )
12	11	fneq1d	⊢ ( 𝜑 → ( 𝐷 Fn ( 𝐵 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ inf ( ∪ 𝑛 ∈ ℕ ran ( 𝑔 ∈ { ℎ ∈ ( ( 𝑉 × 𝑉 ) ↑_m ( 1 ... 𝑛 ) ) ∣ ( ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ 1 ) ) ) = 𝑥 ∧ ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑛 ) ) ) = 𝑦 ∧ ∀ 𝑖 ∈ ( 1 ... ( 𝑛 − 1 ) ) ( 𝐹 ‘ ( 2^nd ‘ ( ℎ ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 1^st ‘ ( ℎ ‘ ( 𝑖 + 1 ) ) ) ) ) } ↦ ( ℝ^_𝑠 Σ_g ( 𝐸 ∘ 𝑔 ) ) ) , ℝ^ , < ) ) Fn ( 𝐵 × 𝐵 ) ) )
13	10 12	mpbiri	⊢ ( 𝜑 → 𝐷 Fn ( 𝐵 × 𝐵 ) )