Metamath Proof Explorer


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 ( ⇝𝑢𝑆 )