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 ∈ rec ⁡ F A ω → F ⁡ B ∈ rec ⁡ F A ω

Proof

Step Hyp Ref Expression
1 frfnom ⊢ rec ⁡ F A ↾ ω Fn ω
2 fvelrnb ⊢ rec ⁡ F A ↾ ω Fn ω → B ∈ ran ⁡ rec ⁡ F A ↾ ω ↔ ∃ x ∈ ω rec ⁡ F A ↾ ω ⁡ x = B
3 1 2 ax-mp ⊢ B ∈ ran ⁡ rec ⁡ F A ↾ ω ↔ ∃ x ∈ ω rec ⁡ F A ↾ ω ⁡ x = B
4 frsuc ⊢ x ∈ ω → rec ⁡ F A ↾ ω ⁡ suc ⁡ x = F ⁡ rec ⁡ F A ↾ ω ⁡ x
5 peano2 ⊢ x ∈ ω → suc ⁡ x ∈ ω
6 fnfvelrn ⊢ rec ⁡ F A ↾ ω Fn ω ∧ suc ⁡ x ∈ ω → rec ⁡ F A ↾ ω ⁡ suc ⁡ x ∈ ran ⁡ rec ⁡ F A ↾ ω
7 1 5 6 sylancr ⊢ x ∈ ω → rec ⁡ F A ↾ ω ⁡ suc ⁡ x ∈ ran ⁡ rec ⁡ F A ↾ ω
8 4 7 eqeltrrd ⊢ x ∈ ω → F ⁡ rec ⁡ F A ↾ ω ⁡ x ∈ ran ⁡ rec ⁡ F A ↾ ω
9 fveq2 ⊢ rec ⁡ F A ↾ ω ⁡ x = B → F ⁡ rec ⁡ F A ↾ ω ⁡ x = F ⁡ B
10 9 eleq1d ⊢ rec ⁡ F A ↾ ω ⁡ x = B → F ⁡ rec ⁡ F A ↾ ω ⁡ x ∈ ran ⁡ rec ⁡ F A ↾ ω ↔ F ⁡ B ∈ ran ⁡ rec ⁡ F A ↾ ω
11 8 10 syl5ibcom ⊢ x ∈ ω → rec ⁡ F A ↾ ω ⁡ x = B → F ⁡ B ∈ ran ⁡ rec ⁡ F A ↾ ω
12 11 rexlimiv ⊢ ∃ x ∈ ω rec ⁡ F A ↾ ω ⁡ x = B → F ⁡ B ∈ ran ⁡ rec ⁡ F A ↾ ω
13 3 12 sylbi ⊢ B ∈ ran ⁡ rec ⁡ F A ↾ ω → F ⁡ B ∈ ran ⁡ rec ⁡ F A ↾ ω
14 df-ima ⊢ rec ⁡ F A ω = ran ⁡ rec ⁡ F A ↾ ω
15 13 14 eleq2s ⊢ B ∈ rec ⁡ F A ω → F ⁡ B ∈ ran ⁡ rec ⁡ F A ↾ ω
16 15 14 eleqtrrdi ⊢ B ∈ rec ⁡ F A ω → F ⁡ B ∈ rec ⁡ F A ω