Metamath Proof Explorer

Theorem orbitcl

Description: The orbit under a function is closed under the function. (Contributed by Eric Schmidt, 6-Nov-2025)

Ref Expression
Assertion orbitcl 
|- ( B e. ( rec ( F , A ) " _om ) -> ( F ` B ) e. ( rec ( F , A ) " _om ) )

Proof

Step Hyp Ref Expression
1 frfnom 
 |-  ( rec ( F , A ) |` _om ) Fn _om
2 fvelrnb 
 |-  ( ( rec ( F , A ) |` _om ) Fn _om -> ( B e. ran ( rec ( F , A ) |` _om ) <-> E. x e. _om ( ( rec ( F , A ) |` _om ) ` x ) = B ) )
3 1 2 ax-mp 
 |-  ( B e. ran ( rec ( F , A ) |` _om ) <-> E. x e. _om ( ( rec ( F , A ) |` _om ) ` x ) = B )
4 frsuc 
 |-  ( x e. _om -> ( ( rec ( F , A ) |` _om ) ` suc x ) = ( F ` ( ( rec ( F , A ) |` _om ) ` x ) ) )
5 peano2 
 |-  ( x e. _om -> suc x e. _om )
6 fnfvelrn 
 |-  ( ( ( rec ( F , A ) |` _om ) Fn _om /\ suc x e. _om ) -> ( ( rec ( F , A ) |` _om ) ` suc x ) e. ran ( rec ( F , A ) |` _om ) )
7 1 5 6 sylancr 
 |-  ( x e. _om -> ( ( rec ( F , A ) |` _om ) ` suc x ) e. ran ( rec ( F , A ) |` _om ) )
8 4 7 eqeltrrd 
 |-  ( x e. _om -> ( F ` ( ( rec ( F , A ) |` _om ) ` x ) ) e. ran ( rec ( F , A ) |` _om ) )
9 fveq2 
 |-  ( ( ( rec ( F , A ) |` _om ) ` x ) = B -> ( F ` ( ( rec ( F , A ) |` _om ) ` x ) ) = ( F ` B ) )
10 9 eleq1d 
 |-  ( ( ( rec ( F , A ) |` _om ) ` x ) = B -> ( ( F ` ( ( rec ( F , A ) |` _om ) ` x ) ) e. ran ( rec ( F , A ) |` _om ) <-> ( F ` B ) e. ran ( rec ( F , A ) |` _om ) ) )
11 8 10 syl5ibcom 
 |-  ( x e. _om -> ( ( ( rec ( F , A ) |` _om ) ` x ) = B -> ( F ` B ) e. ran ( rec ( F , A ) |` _om ) ) )
12 11 rexlimiv 
 |-  ( E. x e. _om ( ( rec ( F , A ) |` _om ) ` x ) = B -> ( F ` B ) e. ran ( rec ( F , A ) |` _om ) )
13 3 12 sylbi 
 |-  ( B e. ran ( rec ( F , A ) |` _om ) -> ( F ` B ) e. ran ( rec ( F , A ) |` _om ) )
14 df-ima 
 |-  ( rec ( F , A ) " _om ) = ran ( rec ( F , A ) |` _om )
15 13 14 eleq2s 
 |-  ( B e. ( rec ( F , A ) " _om ) -> ( F ` B ) e. ran ( rec ( F , A ) |` _om ) )
16 15 14 eleqtrrdi 
 |-  ( B e. ( rec ( F , A ) " _om ) -> ( F ` B ) e. ( rec ( F , A ) " _om ) )