Theorem rp-tfslim

Description: The limit of a sequence of ordinals is the union of its range. (Contributed by RP, 1-Mar-2025)

	Ref	Expression
Assertion	rp-tfslim	|- ( A Fn B -> U_ x e. B ( A ` x ) = U. ran A )

Proof

Step	Hyp	Ref	Expression
1		fvex	|- ( A ` x ) e. _V
2	1	dfiun3	|- U_ x e. B ( A ` x ) = U. ran ( x e. B |-> ( A ` x ) )
3		dffn5	|- ( A Fn B <-> A = ( x e. B |-> ( A ` x ) ) )
4	3	biimpi	|- ( A Fn B -> A = ( x e. B |-> ( A ` x ) ) )
5	4	rneqd	|- ( A Fn B -> ran A = ran ( x e. B |-> ( A ` x ) ) )
6	5	unieqd	|- ( A Fn B -> U. ran A = U. ran ( x e. B |-> ( A ` x ) ) )
7	2 6	eqtr4id	|- ( A Fn B -> U_ x e. B ( A ` x ) = U. ran A )