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	⊢ ( 𝐴 Fn 𝐵 → ∪ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) = ∪ ran 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( 𝐴 ‘ 𝑥 ) ∈ V
2	1	dfiun3	⊢ ∪ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) = ∪ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) )
3		dffn5	⊢ ( 𝐴 Fn 𝐵 ↔ 𝐴 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) )
4	3	biimpi	⊢ ( 𝐴 Fn 𝐵 → 𝐴 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) )
5	4	rneqd	⊢ ( 𝐴 Fn 𝐵 → ran 𝐴 = ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) )
6	5	unieqd	⊢ ( 𝐴 Fn 𝐵 → ∪ ran 𝐴 = ∪ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 ‘ 𝑥 ) ) )
7	2 6	eqtr4id	⊢ ( 𝐴 Fn 𝐵 → ∪ 𝑥 ∈ 𝐵 ( 𝐴 ‘ 𝑥 ) = ∪ ran 𝐴 )