Metamath Proof Explorer

Theorem orbitinit

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

Ref Expression
Assertion orbitinit 
|- ( A e. V -> A e. ( rec ( F , A ) " _om ) )

Proof

Step Hyp Ref Expression
1 fr0g 
 |-  ( A e. V -> ( ( rec ( F , A ) |` _om ) ` (/) ) = A )
2 frfnom 
 |-  ( rec ( F , A ) |` _om ) Fn _om
3 peano1 
 |-  (/) e. _om
4 fnfvelrn 
 |-  ( ( ( rec ( F , A ) |` _om ) Fn _om /\ (/) e. _om ) -> ( ( rec ( F , A ) |` _om ) ` (/) ) e. ran ( rec ( F , A ) |` _om ) )
5 2 3 4 mp2an 
 |-  ( ( rec ( F , A ) |` _om ) ` (/) ) e. ran ( rec ( F , A ) |` _om )
6 1 5 eqeltrrdi 
 |-  ( A e. V -> A e. ran ( rec ( F , A ) |` _om ) )
7 df-ima 
 |-  ( rec ( F , A ) " _om ) = ran ( rec ( F , A ) |` _om )
8 6 7 eleqtrrdi 
 |-  ( A e. V -> A e. ( rec ( F , A ) " _om ) )