Theorem orbitinit

Description: A set is contained in its orbit. (Contributed by Eric Schmidt, 6-Nov-2025)

	Ref	Expression
Assertion	orbitinit	$$⊢A\in V\to A\in \mathrm{rec}\left(F,A\right)\left[\mathrm{\omega }\right]$$

Proof

Step	Hyp	Ref	Expression
1		fr0g	$$⊢A\in V\to \left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)=A$$
2		frfnom	$$⊢\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)Fn\mathrm{\omega }$$
3		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
4		fnfvelrn	$$⊢\left(\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)Fn\mathrm{\omega }\wedge \varnothing \in \mathrm{\omega }\right)\to \left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)\in \mathrm{ran}\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)$$
5	2 3 4	mp2an	$$⊢\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)\in \mathrm{ran}\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)$$
6	1 5	eqeltrrdi	$$⊢A\in V\to A\in \mathrm{ran}\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)$$
7		df-ima	$$⊢\mathrm{rec}\left(F,A\right)\left[\mathrm{\omega }\right]=\mathrm{ran}\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)$$
8	6 7	eleqtrrdi	$$⊢A\in V\to A\in \mathrm{rec}\left(F,A\right)\left[\mathrm{\omega }\right]$$