Metamath Proof Explorer

Theorem frsucmpt2

Description: The successor value resulting from finite recursive definition generation (special case where the generation function is expressed in maps-to notation), using double-substitution instead of a bound variable condition. (Contributed by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses frsucmpt2.1 ⊢ F = rec ⁡ x ∈ V ⟼ C A ↾ ω
frsucmpt2.2 ⊢ y = x → E = C
frsucmpt2.3 ⊢ y = F ⁡ B → E = D
Assertion frsucmpt2 ⊢ B ∈ ω ∧ D ∈ V → F ⁡ suc ⁡ B = D

Proof

Step Hyp Ref Expression
1 frsucmpt2.1 ⊢ F = rec ⁡ x ∈ V ⟼ C A ↾ ω
2 frsucmpt2.2 ⊢ y = x → E = C
3 frsucmpt2.3 ⊢ y = F ⁡ B → E = D
4 nfcv ⊢ Ⅎ _ y A
5 nfcv ⊢ Ⅎ _ y B
6 nfcv ⊢ Ⅎ _ y D
7 2 cbvmptv ⊢ y ∈ V ⟼ E = x ∈ V ⟼ C
8 rdgeq1 ⊢ y ∈ V ⟼ E = x ∈ V ⟼ C → rec ⁡ y ∈ V ⟼ E A = rec ⁡ x ∈ V ⟼ C A
9 7 8 ax-mp ⊢ rec ⁡ y ∈ V ⟼ E A = rec ⁡ x ∈ V ⟼ C A
10 9 reseq1i ⊢ rec ⁡ y ∈ V ⟼ E A ↾ ω = rec ⁡ x ∈ V ⟼ C A ↾ ω
11 1 10 eqtr4i ⊢ F = rec ⁡ y ∈ V ⟼ E A ↾ ω
12 4 5 6 11 3 frsucmpt ⊢ B ∈ ω ∧ D ∈ V → F ⁡ suc ⁡ B = D