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	$$⊢AFnB\to \bigcup _{x\in B}A\left(x\right)=\bigcup \mathrm{ran}A$$

Proof

Step	Hyp	Ref	Expression
1		fvex	$$⊢A\left(x\right)\in \mathrm{V}$$
2	1	dfiun3	$$⊢\bigcup _{x\in B}A\left(x\right)=\bigcup \mathrm{ran}\left(x\in B⟼A\left(x\right)\right)$$
3		dffn5	$$⊢AFnB\leftrightarrow A=\left(x\in B⟼A\left(x\right)\right)$$
4	3	biimpi	$$⊢AFnB\to A=\left(x\in B⟼A\left(x\right)\right)$$
5	4	rneqd	$$⊢AFnB\to \mathrm{ran}A=\mathrm{ran}\left(x\in B⟼A\left(x\right)\right)$$
6	5	unieqd	$$⊢AFnB\to \bigcup \mathrm{ran}A=\bigcup \mathrm{ran}\left(x\in B⟼A\left(x\right)\right)$$
7	2 6	eqtr4id	$$⊢AFnB\to \bigcup _{x\in B}A\left(x\right)=\bigcup \mathrm{ran}A$$