Metamath Proof Explorer

Theorem rdgsucmptf

Description: The value of the recursive definition generator at a successor (special case where the characteristic function uses the map operation). (Contributed by NM, 22-Oct-2003) (Revised by Mario Carneiro, 15-Oct-2016)

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

Proof

Step Hyp Ref Expression
1 rdgsucmptf.1 ⊢ Ⅎ _ x A
2 rdgsucmptf.2 ⊢ Ⅎ _ x B
3 rdgsucmptf.3 ⊢ Ⅎ _ x D
4 rdgsucmptf.4 ⊢ F = rec ⁡ x ∈ V ⟼ C A
5 rdgsucmptf.5 ⊢ x = F ⁡ B → C = D
6 rdgsuc ⊢ B ∈ On → 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 ∈ On → 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 4 13 nfcxfr ⊢ Ⅎ _ x F
15 14 2 nffv ⊢ Ⅎ _ x F ⁡ B
16 eqid ⊢ x ∈ V ⟼ C = x ∈ V ⟼ C
17 15 3 5 16 fvmptf ⊢ F ⁡ B ∈ V ∧ D ∈ V → x ∈ V ⟼ C ⁡ F ⁡ B = D
18 11 17 mpan ⊢ D ∈ V → x ∈ V ⟼ C ⁡ F ⁡ B = D
19 10 18 sylan9eq ⊢ B ∈ On ∧ D ∈ V → F ⁡ suc ⁡ B = D