Metamath Proof Explorer

Theorem frsucmpt

Description: The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation). (Contributed by NM, 14-Sep-2003) (Revised by Scott Fenton, 2-Nov-2011)

Ref Expression
Hypotheses frsucmpt.1 ⊢ Ⅎ _ x A
frsucmpt.2 ⊢ Ⅎ _ x B
frsucmpt.3 ⊢ Ⅎ _ x D
frsucmpt.4 ⊢ F = rec ⁡ x ∈ V ⟼ C A ↾ ω
frsucmpt.5 ⊢ x = F ⁡ B → C = D
Assertion frsucmpt ⊢ B ∈ ω ∧ D ∈ V → F ⁡ suc ⁡ B = D

Proof

Step Hyp Ref Expression
1 frsucmpt.1 ⊢ Ⅎ _ x A
2 frsucmpt.2 ⊢ Ⅎ _ x B
3 frsucmpt.3 ⊢ Ⅎ _ x D
4 frsucmpt.4 ⊢ F = rec ⁡ x ∈ V ⟼ C A ↾ ω
5 frsucmpt.5 ⊢ x = F ⁡ B → C = D
6 frsuc ⊢ B ∈ ω → rec ⁡ x ∈ V ⟼ C A ↾ ω ⁡ suc ⁡ B = x ∈ V ⟼ C ⁡ rec ⁡ x ∈ V ⟼ C A ↾ ω ⁡ B
7 4 fveq1i ⊢ F ⁡ suc ⁡ B = rec ⁡ x ∈ V ⟼ C A ↾ ω ⁡ suc ⁡ B
8 4 fveq1i ⊢ F ⁡ B = rec ⁡ x ∈ V ⟼ C A ↾ ω ⁡ B
9 8 fveq2i ⊢ x ∈ V ⟼ C ⁡ F ⁡ B = x ∈ V ⟼ C ⁡ rec ⁡ x ∈ V ⟼ C A ↾ ω ⁡ B
10 6 7 9 3eqtr4g ⊢ B ∈ ω → F ⁡ suc ⁡ B = x ∈ V ⟼ C ⁡ F ⁡ B
11 fvex ⊢ F ⁡ B ∈ V
12 nfmpt1 ⊢ Ⅎ _ x x ∈ V ⟼ C
13 12 1 nfrdg ⊢ Ⅎ _ x rec ⁡ x ∈ V ⟼ C A
14 nfcv ⊢ Ⅎ _ x ω
15 13 14 nfres ⊢ Ⅎ _ x rec ⁡ x ∈ V ⟼ C A ↾ ω
16 4 15 nfcxfr ⊢ Ⅎ _ x F
17 16 2 nffv ⊢ Ⅎ _ x F ⁡ B
18 eqid ⊢ x ∈ V ⟼ C = x ∈ V ⟼ C
19 17 3 5 18 fvmptf ⊢ F ⁡ B ∈ V ∧ D ∈ V → x ∈ V ⟼ C ⁡ F ⁡ B = D
20 11 19 mpan ⊢ D ∈ V → x ∈ V ⟼ C ⁡ F ⁡ B = D
21 10 20 sylan9eq ⊢ B ∈ ω ∧ D ∈ V → F ⁡ suc ⁡ B = D