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
|
syl5eq |
⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) |
12 |
6 7 11
|
ifbieq12d |
⊢ ( 𝐴 ∈ 𝑉 → if ( [ 𝐴 / 𝑥 ] Lim dom 𝑔 , ⦋ 𝐴 / 𝑥 ⦌ ∪ ran 𝑔 , ⦋ 𝐴 / 𝑥 ⦌ ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) = if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) |
13 |
5 12
|
syl5eq |
⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 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
|
syl5eq |
⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 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 ( ⦋ 𝐴 / 𝑥 ⦌ 𝐹 , ⦋ 𝐴 / 𝑥 ⦌ 𝐼 ) ) |