Theorem ulmrel

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

	Ref	Expression
Assertion	ulmrel	$$⊢\mathrm{Rel}\underset{u}{⇝}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ulm	$$⊢\underset{u}{⇝}=\left(s\in \mathrm{V}⟼\left\{⟨f,y⟩|\exists n\in \mathbb{Z}\left(f:{\mathbb{Z}}_{\ge n}⟶{ℂ}^s\wedge y:s⟶ℂ\wedge \forall x\in {ℝ}^{+}\exists j\in {\mathbb{Z}}_{\ge n}\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in s\left|f\left(k\right)\left(z\right)-y\left(z\right)\right|<x\right)\right\}\right)$$
2	1	relmptopab	$$⊢\mathrm{Rel}\underset{u}{⇝}\left(S\right)$$