Theorem orbitinit

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

	Ref	Expression
Assertion	orbitinit	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ ( rec ( 𝐹 , 𝐴 ) “ ω ) )

Proof

Step	Hyp	Ref	Expression
1		fr0g	⊢ ( 𝐴 ∈ 𝑉 → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ ∅ ) = 𝐴 )
2		frfnom	⊢ ( rec ( 𝐹 , 𝐴 ) ↾ ω ) Fn ω
3		peano1	⊢ ∅ ∈ ω
4		fnfvelrn	⊢ ( ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) Fn ω ∧ ∅ ∈ ω ) → ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω ) )
5	2 3 4	mp2an	⊢ ( ( rec ( 𝐹 , 𝐴 ) ↾ ω ) ‘ ∅ ) ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω )
6	1 5	eqeltrrdi	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ ran ( rec ( 𝐹 , 𝐴 ) ↾ ω ) )
7		df-ima	⊢ ( rec ( 𝐹 , 𝐴 ) “ ω ) = ran ( rec ( 𝐹 , 𝐴 ) ↾ ω )
8	6 7	eleqtrrdi	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ ( rec ( 𝐹 , 𝐴 ) “ ω ) )