Metamath Proof Explorer

Theorem tfrlem9

Description: Lemma for transfinite recursion. Here we compute the value of recs (the union of all acceptable functions). (Contributed by NM, 17-Aug-1994)

Ref Expression
Hypothesis tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
Assertion tfrlem9 ( 𝐵 ∈ dom recs ( 𝐹 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2 eldm2g ⊢ ( 𝐵 ∈ dom recs ( 𝐹 ) → ( 𝐵 ∈ dom recs ( 𝐹 ) ↔ ∃ 𝑧 ⟨ 𝐵 , 𝑧 ⟩ ∈ recs ( 𝐹 ) ) )
3 2 ibi ⊢ ( 𝐵 ∈ dom recs ( 𝐹 ) → ∃ 𝑧 ⟨ 𝐵 , 𝑧 ⟩ ∈ recs ( 𝐹 ) )
4 dfrecs3 ⊢ recs ( 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
5 4 eleq2i ⊢ ( ⟨ 𝐵 , 𝑧 ⟩ ∈ recs ( 𝐹 ) ↔ ⟨ 𝐵 , 𝑧 ⟩ ∈ ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } )
6 eluniab ⊢ ( ⟨ 𝐵 , 𝑧 ⟩ ∈ ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } ↔ ∃ 𝑓 ( ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝑓 ∧ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
7 5 6 bitri ⊢ ( ⟨ 𝐵 , 𝑧 ⟩ ∈ recs ( 𝐹 ) ↔ ∃ 𝑓 ( ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝑓 ∧ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) )
8 fnop ⊢ ( ( 𝑓 Fn 𝑥 ∧ ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝑓 ) → 𝐵 ∈ 𝑥 )
9 rspe ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) → ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
10 1 eqabri ⊢ ( 𝑓 ∈ 𝐴 ↔ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) )
11 elssuni ⊢ ( 𝑓 ∈ 𝐴 → 𝑓 ⊆ ∪ 𝐴 )
12 1 recsfval ⊢ recs ( 𝐹 ) = ∪ 𝐴
13 11 12 sseqtrrdi ⊢ ( 𝑓 ∈ 𝐴 → 𝑓 ⊆ recs ( 𝐹 ) )
14 10 13 sylbir ⊢ ( ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) → 𝑓 ⊆ recs ( 𝐹 ) )
15 9 14 syl ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) → 𝑓 ⊆ recs ( 𝐹 ) )
16 fveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝐵 ) )
17 reseq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑓 ↾ 𝑦 ) = ( 𝑓 ↾ 𝐵 ) )
18 17 fveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝐵 ) ) )
19 16 18 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ↔ ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝐵 ) ) ) )
20 19 rspcv ⊢ ( 𝐵 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) → ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝐵 ) ) ) )
21 fndm ⊢ ( 𝑓 Fn 𝑥 → dom 𝑓 = 𝑥 )
22 21 eleq2d ⊢ ( 𝑓 Fn 𝑥 → ( 𝐵 ∈ dom 𝑓 ↔ 𝐵 ∈ 𝑥 ) )
23 1 tfrlem7 ⊢ Fun recs ( 𝐹 )
24 funssfv ⊢ ( ( Fun recs ( 𝐹 ) ∧ 𝑓 ⊆ recs ( 𝐹 ) ∧ 𝐵 ∈ dom 𝑓 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝑓 ‘ 𝐵 ) )
25 23 24 mp3an1 ⊢ ( ( 𝑓 ⊆ recs ( 𝐹 ) ∧ 𝐵 ∈ dom 𝑓 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝑓 ‘ 𝐵 ) )
26 25 adantrl ⊢ ( ( 𝑓 ⊆ recs ( 𝐹 ) ∧ ( ( 𝑓 Fn 𝑥 ∧ 𝑥 ∈ On ) ∧ 𝐵 ∈ dom 𝑓 ) ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝑓 ‘ 𝐵 ) )
27 21 eleq1d ⊢ ( 𝑓 Fn 𝑥 → ( dom 𝑓 ∈ On ↔ 𝑥 ∈ On ) )
28 onelss ⊢ ( dom 𝑓 ∈ On → ( 𝐵 ∈ dom 𝑓 → 𝐵 ⊆ dom 𝑓 ) )
29 27 28 biimtrrdi ⊢ ( 𝑓 Fn 𝑥 → ( 𝑥 ∈ On → ( 𝐵 ∈ dom 𝑓 → 𝐵 ⊆ dom 𝑓 ) ) )
30 29 imp31 ⊢ ( ( ( 𝑓 Fn 𝑥 ∧ 𝑥 ∈ On ) ∧ 𝐵 ∈ dom 𝑓 ) → 𝐵 ⊆ dom 𝑓 )
31 fun2ssres ⊢ ( ( Fun recs ( 𝐹 ) ∧ 𝑓 ⊆ recs ( 𝐹 ) ∧ 𝐵 ⊆ dom 𝑓 ) → ( recs ( 𝐹 ) ↾ 𝐵 ) = ( 𝑓 ↾ 𝐵 ) )
32 31 fveq2d ⊢ ( ( Fun recs ( 𝐹 ) ∧ 𝑓 ⊆ recs ( 𝐹 ) ∧ 𝐵 ⊆ dom 𝑓 ) → ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝐵 ) ) )
33 23 32 mp3an1 ⊢ ( ( 𝑓 ⊆ recs ( 𝐹 ) ∧ 𝐵 ⊆ dom 𝑓 ) → ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝐵 ) ) )
34 30 33 sylan2 ⊢ ( ( 𝑓 ⊆ recs ( 𝐹 ) ∧ ( ( 𝑓 Fn 𝑥 ∧ 𝑥 ∈ On ) ∧ 𝐵 ∈ dom 𝑓 ) ) → ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝐵 ) ) )
35 26 34 eqeq12d ⊢ ( ( 𝑓 ⊆ recs ( 𝐹 ) ∧ ( ( 𝑓 Fn 𝑥 ∧ 𝑥 ∈ On ) ∧ 𝐵 ∈ dom 𝑓 ) ) → ( ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ↔ ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝐵 ) ) ) )
36 35 exbiri ⊢ ( 𝑓 ⊆ recs ( 𝐹 ) → ( ( ( 𝑓 Fn 𝑥 ∧ 𝑥 ∈ On ) ∧ 𝐵 ∈ dom 𝑓 ) → ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝐵 ) ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) )
37 36 com3l ⊢ ( ( ( 𝑓 Fn 𝑥 ∧ 𝑥 ∈ On ) ∧ 𝐵 ∈ dom 𝑓 ) → ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝐵 ) ) → ( 𝑓 ⊆ recs ( 𝐹 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) )
38 37 exp31 ⊢ ( 𝑓 Fn 𝑥 → ( 𝑥 ∈ On → ( 𝐵 ∈ dom 𝑓 → ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝐵 ) ) → ( 𝑓 ⊆ recs ( 𝐹 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) ) ) )
39 38 com34 ⊢ ( 𝑓 Fn 𝑥 → ( 𝑥 ∈ On → ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝐵 ) ) → ( 𝐵 ∈ dom 𝑓 → ( 𝑓 ⊆ recs ( 𝐹 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) ) ) )
40 39 com24 ⊢ ( 𝑓 Fn 𝑥 → ( 𝐵 ∈ dom 𝑓 → ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝐵 ) ) → ( 𝑥 ∈ On → ( 𝑓 ⊆ recs ( 𝐹 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) ) ) )
41 22 40 sylbird ⊢ ( 𝑓 Fn 𝑥 → ( 𝐵 ∈ 𝑥 → ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝐵 ) ) → ( 𝑥 ∈ On → ( 𝑓 ⊆ recs ( 𝐹 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) ) ) )
42 41 com3l ⊢ ( 𝐵 ∈ 𝑥 → ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝐵 ) ) → ( 𝑓 Fn 𝑥 → ( 𝑥 ∈ On → ( 𝑓 ⊆ recs ( 𝐹 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) ) ) )
43 20 42 syld ⊢ ( 𝐵 ∈ 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) → ( 𝑓 Fn 𝑥 → ( 𝑥 ∈ On → ( 𝑓 ⊆ recs ( 𝐹 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) ) ) )
44 43 com24 ⊢ ( 𝐵 ∈ 𝑥 → ( 𝑥 ∈ On → ( 𝑓 Fn 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) → ( 𝑓 ⊆ recs ( 𝐹 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) ) ) )
45 44 imp4d ⊢ ( 𝐵 ∈ 𝑥 → ( ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) → ( 𝑓 ⊆ recs ( 𝐹 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) )
46 15 45 mpdi ⊢ ( 𝐵 ∈ 𝑥 → ( ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) )
47 8 46 syl ⊢ ( ( 𝑓 Fn 𝑥 ∧ ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝑓 ) → ( ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) )
48 47 exp4d ⊢ ( ( 𝑓 Fn 𝑥 ∧ ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝑓 ) → ( 𝑥 ∈ On → ( 𝑓 Fn 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) ) )
49 48 ex ⊢ ( 𝑓 Fn 𝑥 → ( ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝑓 → ( 𝑥 ∈ On → ( 𝑓 Fn 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) ) ) )
50 49 com4r ⊢ ( 𝑓 Fn 𝑥 → ( 𝑓 Fn 𝑥 → ( ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝑓 → ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) ) ) )
51 50 pm2.43i ⊢ ( 𝑓 Fn 𝑥 → ( ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝑓 → ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) ) )
52 51 com3l ⊢ ( ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝑓 → ( 𝑥 ∈ On → ( 𝑓 Fn 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) ) )
53 52 imp4a ⊢ ( ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝑓 → ( 𝑥 ∈ On → ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) ) )
54 53 rexlimdv ⊢ ( ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝑓 → ( ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) ) )
55 54 imp ⊢ ( ( ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝑓 ∧ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) )
56 55 exlimiv ⊢ ( ∃ 𝑓 ( ⟨ 𝐵 , 𝑧 ⟩ ∈ 𝑓 ∧ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) )
57 7 56 sylbi ⊢ ( ⟨ 𝐵 , 𝑧 ⟩ ∈ recs ( 𝐹 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) )
58 57 exlimiv ⊢ ( ∃ 𝑧 ⟨ 𝐵 , 𝑧 ⟩ ∈ recs ( 𝐹 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) )
59 3 58 syl ⊢ ( 𝐵 ∈ dom recs ( 𝐹 ) → ( recs ( 𝐹 ) ‘ 𝐵 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐵 ) ) )