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	$$⊢\mathrm{rec}\left(F,A\right)\left[\mathrm{\omega }\right]\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		rdgfun	$$⊢\mathrm{Fun}\mathrm{rec}\left(F,A\right)$$
2		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
3	2	funimaex	$$⊢\mathrm{Fun}\mathrm{rec}\left(F,A\right)\to \mathrm{rec}\left(F,A\right)\left[\mathrm{\omega }\right]\in \mathrm{V}$$
4	1 3	ax-mp	$$⊢\mathrm{rec}\left(F,A\right)\left[\mathrm{\omega }\right]\in \mathrm{V}$$