Theorem ulmrel

Description: The uniform limit relation is a relation. (Contributed by Mario Carneiro, 26-Feb-2015)

	Ref	Expression
Assertion	ulmrel	⊢ Rel ( ⇝𝑢 ‘ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		df-ulm	⊢ ⇝𝑢 = ( 𝑠 ∈ V ↦ { ⟨ 𝑓 , 𝑦 ⟩ ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑠 ) ∧ 𝑦 : 𝑠 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } )
2	1	relmptopab	⊢ Rel ( ⇝𝑢 ‘ 𝑆 )