Metamath Proof Explorer

Theorem frsucmptn

Description: The value of the finite recursive definition generator at a successor (special case where the characteristic function is a mapping abstraction and where the mapping class D is a proper class). This is a technical lemma that can be used together with frsucmpt to help eliminate redundant sethood antecedents. (Contributed by Scott Fenton, 19-Feb-2011) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses frsucmpt.1 ⊢ Ⅎ 𝑥 𝐴
frsucmpt.2 ⊢ Ⅎ 𝑥 𝐵
frsucmpt.3 ⊢ Ⅎ 𝑥 𝐷
frsucmpt.4 ⊢ 𝐹 = ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω )
frsucmpt.5 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝐵 ) → 𝐶 = 𝐷 )
Assertion frsucmptn ( ¬ 𝐷 ∈ V → ( 𝐹 ‘ suc 𝐵 ) = ∅ )

Proof

Step Hyp Ref Expression
1 frsucmpt.1 ⊢ Ⅎ 𝑥 𝐴
2 frsucmpt.2 ⊢ Ⅎ 𝑥 𝐵
3 frsucmpt.3 ⊢ Ⅎ 𝑥 𝐷
4 frsucmpt.4 ⊢ 𝐹 = ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω )
5 frsucmpt.5 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝐵 ) → 𝐶 = 𝐷 )
6 4 fveq1i ⊢ ( 𝐹 ‘ suc 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 )
7 frfnom ⊢ ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) Fn ω
8 fndm ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) Fn ω → dom ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) = ω )
9 7 8 ax-mp ⊢ dom ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) = ω
10 9 eleq2i ⊢ ( suc 𝐵 ∈ dom ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ↔ suc 𝐵 ∈ ω )
11 peano2b ⊢ ( 𝐵 ∈ ω ↔ suc 𝐵 ∈ ω )
12 frsuc ⊢ ( 𝐵 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) )
13 4 fveq1i ⊢ ( 𝐹 ‘ 𝐵 ) = ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 )
14 13 fveq2i ⊢ ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝐵 ) ) = ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) )
15 12 14 eqtr4di ⊢ ( 𝐵 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝐵 ) ) )
16 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ V ↦ 𝐶 )
17 16 1 nfrdg ⊢ Ⅎ 𝑥 rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 )
18 nfcv ⊢ Ⅎ 𝑥 ω
19 17 18 nfres ⊢ Ⅎ 𝑥 ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω )
20 4 19 nfcxfr ⊢ Ⅎ 𝑥 𝐹
21 20 2 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝐵 )
22 eqid ⊢ ( 𝑥 ∈ V ↦ 𝐶 ) = ( 𝑥 ∈ V ↦ 𝐶 )
23 21 3 5 22 fvmptnf ⊢ ( ¬ 𝐷 ∈ V → ( ( 𝑥 ∈ V ↦ 𝐶 ) ‘ ( 𝐹 ‘ 𝐵 ) ) = ∅ )
24 15 23 sylan9eqr ⊢ ( ( ¬ 𝐷 ∈ V ∧ 𝐵 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ∅ )
25 24 ex ⊢ ( ¬ 𝐷 ∈ V → ( 𝐵 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ∅ ) )
26 11 25 syl5bir ⊢ ( ¬ 𝐷 ∈ V → ( suc 𝐵 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ∅ ) )
27 10 26 syl5bi ⊢ ( ¬ 𝐷 ∈ V → ( suc 𝐵 ∈ dom ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ∅ ) )
28 ndmfv ⊢ ( ¬ suc 𝐵 ∈ dom ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) → ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ∅ )
29 27 28 pm2.61d1 ⊢ ( ¬ 𝐷 ∈ V → ( ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ∅ )
30 6 29 syl5eq ⊢ ( ¬ 𝐷 ∈ V → ( 𝐹 ‘ suc 𝐵 ) = ∅ )