Metamath Proof Explorer

Theorem csbrdgg

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

Ref Expression
Assertion csbrdgg ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ rec ( 𝐹 , 𝐼 ) = rec ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 csbrecsg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) = recs ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) )
2 csbmpt2 ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) = ( 𝑔 ∈ V ↦ ⦋ 𝐴 / 𝑥 ⦌ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
3 csbif ⊢ ⦋ 𝐴 / 𝑥 ⦌ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) = if ( [ 𝐴 / 𝑥 ] 𝑔 = ∅ , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 , ⦋ 𝐴 / 𝑥 ⦌ if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) )
4 sbcg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑔 = ∅ ↔ 𝑔 = ∅ ) )
5 csbif ⊢ ⦋ 𝐴 / 𝑥 ⦌ if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) = if ( [ 𝐴 / 𝑥 ] Lim dom 𝑔 , ⦋ 𝐴 / 𝑥 ⦌ ∪ ran 𝑔 , ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) )
6 sbcg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] Lim dom 𝑔 ↔ Lim dom 𝑔 ) )
7 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ∪ ran 𝑔 = ∪ ran 𝑔 )
8 csbfv12 ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ ( 𝑔 ‘ ∪ dom 𝑔 ) )
9 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑔 ‘ ∪ dom 𝑔 ) = ( 𝑔 ‘ ∪ dom 𝑔 ) )
10 9 fveq2d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ⦋ 𝐴 / 𝑥 ⦌ ( 𝑔 ‘ ∪ dom 𝑔 ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) )
11 8 10 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) )
12 6 7 11 ifbieq12d ⊢ ( 𝐴 ∈ 𝑉 → if ( [ 𝐴 / 𝑥 ] Lim dom 𝑔 , ⦋ 𝐴 / 𝑥 ⦌ ∪ ran 𝑔 , ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) = if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) )
13 5 12 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) = if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) )
14 4 13 ifbieq2d ⊢ ( 𝐴 ∈ 𝑉 → if ( [ 𝐴 / 𝑥 ] 𝑔 = ∅ , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 , ⦋ 𝐴 / 𝑥 ⦌ if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) = if ( 𝑔 = ∅ , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) )
15 3 14 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) = if ( 𝑔 = ∅ , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) )
16 15 mpteq2dv ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑔 ∈ V ↦ ⦋ 𝐴 / 𝑥 ⦌ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) = ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
17 2 16 eqtrd ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) = ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
18 recseq ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) = ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) → recs ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) )
19 17 18 syl ⊢ ( 𝐴 ∈ 𝑉 → recs ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) )
20 1 19 eqtrd ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) )
21 df-rdg ⊢ rec ( 𝐹 , 𝐼 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
22 21 csbeq2i ⊢ ⦋ 𝐴 / 𝑥 ⦌ rec ( 𝐹 , 𝐼 ) = ⦋ 𝐴 / 𝑥 ⦌ recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
23 df-rdg ⊢ rec ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
24 20 22 23 3eqtr4g ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ rec ( 𝐹 , 𝐼 ) = rec ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 ) )