Metamath Proof Explorer

Theorem csbwrecsg

Description: Move class substitution in and out of the well-founded recursive function generator. (Contributed by ML, 25-Oct-2020)

Ref Expression
Assertion csbwrecsg ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ wrecs ( 𝑅 , 𝐷 , 𝐹 ) = wrecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 csbuni ⊢ ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) } = ∪ ⦋ 𝐴 / 𝑥 ⦌ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) }
2 csbab ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) } = { 𝑓 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) }
3 sbcex2 ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) ↔ ∃ 𝑧 [ 𝐴 / 𝑥 ] ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) )
4 sbc3an ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑓 Fn 𝑧 ∧ [ 𝐴 / 𝑥 ] ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) )
5 sbcg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑓 Fn 𝑧 ↔ 𝑓 Fn 𝑧 ) )
6 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 ⊆ 𝐷 ∧ [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) )
7 sbcssg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 ⊆ 𝐷 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )
8 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑧 = 𝑧 )
9 8 sseq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ↔ 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )
10 7 9 bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 ⊆ 𝐷 ↔ 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )
11 sbcralg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ↔ ∀ 𝑦 ∈ 𝑧 [ 𝐴 / 𝑥 ] Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) )
12 sbcssg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ↔ ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ) )
13 8 sseq2d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ↔ ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) )
14 csbpredg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑦 ) = Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ) )
15 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦 )
16 predeq3 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦 → Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ) = Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) )
17 15 16 syl ⊢ ( 𝐴 ∈ 𝑉 → Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ) = Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) )
18 14 17 eqtrd ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑦 ) = Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) )
19 18 sseq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ↔ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) )
20 12 13 19 3bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ↔ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) )
21 20 ralbidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝑧 [ 𝐴 / 𝑥 ] Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ↔ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) )
22 11 21 bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ↔ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) )
23 10 22 anbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑧 ⊆ 𝐷 ∧ [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ↔ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ) )
24 6 23 syl5bb ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ↔ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ) )
25 sbcralg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑧 [ 𝐴 / 𝑥 ] ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) )
26 sbceqg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝑓 ‘ 𝑦 ) = ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) )
27 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑦 ) )
28 csbfv12 ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) )
29 csbres ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝑓 ↾ ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑦 ) )
30 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑓 = 𝑓 )
31 30 18 reseq12d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑓 ↾ ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) = ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) )
32 29 31 syl5eq ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) = ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) )
33 32 fveq2d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) )
34 28 33 syl5eq ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) )
35 27 34 eqeq12d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝑓 ‘ 𝑦 ) = ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ↔ ( 𝑓 ‘ 𝑦 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) )
36 26 35 bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ↔ ( 𝑓 ‘ 𝑦 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) )
37 36 ralbidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝑧 [ 𝐴 / 𝑥 ] ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) )
38 25 37 bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) )
39 5 24 38 3anbi123d ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑓 Fn 𝑧 ∧ [ 𝐴 / 𝑥 ] ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) ↔ ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) ) )
40 4 39 syl5bb ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) ↔ ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) ) )
41 40 exbidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑧 [ 𝐴 / 𝑥 ] ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) ↔ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) ) )
42 3 41 syl5bb ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) ↔ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) ) )
43 42 abbidv ⊢ ( 𝐴 ∈ 𝑉 → { 𝑓 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) } )
44 2 43 syl5eq ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) } )
45 44 unieqd ⊢ ( 𝐴 ∈ 𝑉 → ∪ ⦋ 𝐴 / 𝑥 ⦌ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) } = ∪ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) } )
46 1 45 syl5eq ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) } = ∪ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) } )
47 df-wrecs ⊢ wrecs ( 𝑅 , 𝐷 , 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) }
48 47 csbeq2i ⊢ ⦋ 𝐴 / 𝑥 ⦌ wrecs ( 𝑅 , 𝐷 , 𝐹 ) = ⦋ 𝐴 / 𝑥 ⦌ ∪ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( 𝑅 , 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ Pred ( 𝑅 , 𝐷 , 𝑦 ) ) ) ) }
49 df-wrecs ⊢ wrecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑧 ( 𝑓 Fn 𝑧 ∧ ( 𝑧 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∧ ∀ 𝑦 ∈ 𝑧 Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ⊆ 𝑧 ) ∧ ∀ 𝑦 ∈ 𝑧 ( 𝑓 ‘ 𝑦 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑓 ↾ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , 𝑦 ) ) ) ) }
50 46 48 49 3eqtr4g ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ wrecs ( 𝑅 , 𝐷 , 𝐹 ) = wrecs ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ) )