Description: The uniform limit relation is a relation. (Contributed by Mario Carneiro, 26-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ulmrel | ⊢ Rel ( ⇝𝑢 ‘ 𝑆 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ulm | ⊢ ⇝𝑢 = ( 𝑠 ∈ V ↦ { 〈 𝑓 , 𝑦 〉 ∣ ∃ 𝑛 ∈ ℤ ( 𝑓 : ( ℤ≥ ‘ 𝑛 ) ⟶ ( ℂ ↑m 𝑠 ) ∧ 𝑦 : 𝑠 ⟶ ℂ ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑛 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑠 ( abs ‘ ( ( ( 𝑓 ‘ 𝑘 ) ‘ 𝑧 ) − ( 𝑦 ‘ 𝑧 ) ) ) < 𝑥 ) } ) | |
2 | 1 | relmptopab | ⊢ Rel ( ⇝𝑢 ‘ 𝑆 ) |