Theorem orbitex

Description: Orbits exist. Given a set A and a function F , the orbit of A under F is the smallest set Z such that A e. Z and Z is closed under F . (Contributed by Eric Schmidt, 6-Nov-2025)

	Ref	Expression
Assertion	orbitex	⊢ ( rec ( 𝐹 , 𝐴 ) “ ω ) ∈ V

Proof

Step	Hyp	Ref	Expression
1		rdgfun	⊢ Fun rec ( 𝐹 , 𝐴 )
2		omex	⊢ ω ∈ V
3	2	funimaex	⊢ ( Fun rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) “ ω ) ∈ V )
4	1 3	ax-mp	⊢ ( rec ( 𝐹 , 𝐴 ) “ ω ) ∈ V