Theorem orbitcl

Description: The orbit under a function is closed under the function. (Contributed by Eric Schmidt, 6-Nov-2025)

	Ref	Expression
Assertion	orbitcl	⊢ ( 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) “ ω ) → ( 𝐹 ‘ 𝐵 ) ∈ ( rec ( 𝐹 , 𝐴 ) “ ω ) )

Proof

Step	Hyp	Ref	Expression
1		frfnom	⊢ ( rec ( 𝐹 , 𝐴 ) ↾ ω ) Fn ω
2		fvelrnb	⊢ ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) Fn ω → ( 𝐵 ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ↔ ∃ 𝑥 ∈ ω ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = 𝐵 ) )
3	1 2	ax-mp	⊢ ( 𝐵 ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ↔ ∃ 𝑥 ∈ ω ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = 𝐵 )
4		frsuc	⊢ ( 𝑥 ∈ ω → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ suc 𝑥 ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) )
5		peano2	⊢ ( 𝑥 ∈ ω → suc 𝑥 ∈ ω )
6		fnfvelrn	⊢ ( ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) Fn ω ∧ suc 𝑥 ∈ ω ) → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ suc 𝑥 ) ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω ) )
7	1 5 6	sylancr	⊢ ( 𝑥 ∈ ω → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ suc 𝑥 ) ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω ) )
8	4 7	eqeltrrd	⊢ ( 𝑥 ∈ ω → ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω ) )
9		fveq2	⊢ ( ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = 𝐵 → ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝐵 ) )
10	9	eleq1d	⊢ ( ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = 𝐵 → ( ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) ) ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ↔ ( 𝐹 ‘ 𝐵 ) ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ) )
11	8 10	syl5ibcom	⊢ ( 𝑥 ∈ ω → ( ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = 𝐵 → ( 𝐹 ‘ 𝐵 ) ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ) )
12	11	rexlimiv	⊢ ( ∃ 𝑥 ∈ ω ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ 𝑥 ) = 𝐵 → ( 𝐹 ‘ 𝐵 ) ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω ) )
13	3 12	sylbi	⊢ ( 𝐵 ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω ) → ( 𝐹 ‘ 𝐵 ) ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω ) )
14		df-ima	⊢ ( rec ( 𝐹 , 𝐴 ) “ ω ) = ran ( rec ( 𝐹 , 𝐴 ) ↾ ω )
15	13 14	eleq2s	⊢ ( 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) “ ω ) → ( 𝐹 ‘ 𝐵 ) ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω ) )
16	15 14	eleqtrrdi	⊢ ( 𝐵 ∈ ( rec ( 𝐹 , 𝐴 ) “ ω ) → ( 𝐹 ‘ 𝐵 ) ∈ ( rec ( 𝐹 , 𝐴 ) “ ω ) )