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 ( ~~>u ` S )

Proof

Step	Hyp	Ref	Expression
1		df-ulm	\|- ~~>u = ( s e. _V \|-> { <. f , y >. \| E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m s ) /\ y : s --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } )
2	1	relmptopab	\|- Rel ( ~~>u ` S )

Step

Hyp

Ref

Expression

df-ulm

 |-  ~~>u = ( s e. _V |-> { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m s ) /\ y : s --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } )

relmptopab

 |-  Rel ( ~~>u ` S )