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 ( F , A ) " _om ) e. _V

Proof

Step	Hyp	Ref	Expression
1		rdgfun	|- Fun rec ( F , A )
2		omex	|- _om e. _V
3	2	funimaex	|- ( Fun rec ( F , A ) -> ( rec ( F , A ) " _om ) e. _V )
4	1 3	ax-mp	|- ( rec ( F , A ) " _om ) e. _V