Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) ) = ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) ) |
2 |
|
rdgvalg |
⊢ ( 𝑦 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ V ↦ if ( 𝑥 = ∅ , 𝐴 , if ( Lim dom 𝑥 , ∪ ran 𝑥 , ( 𝐹 ‘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) ) ) ) ‘ ( rec ( 𝐹 , 𝐴 ) ↾ 𝑦 ) ) ) |
3 |
|
rdgseg |
⊢ ( 𝑦 ∈ dom rec ( 𝐹 , 𝐴 ) → ( rec ( 𝐹 , 𝐴 ) ↾ 𝑦 ) ∈ V ) |
4 |
|
rdgfun |
⊢ Fun rec ( 𝐹 , 𝐴 ) |
5 |
|
funfn |
⊢ ( Fun rec ( 𝐹 , 𝐴 ) ↔ rec ( 𝐹 , 𝐴 ) Fn dom rec ( 𝐹 , 𝐴 ) ) |
6 |
4 5
|
mpbi |
⊢ rec ( 𝐹 , 𝐴 ) Fn dom rec ( 𝐹 , 𝐴 ) |
7 |
|
rdgdmlim |
⊢ Lim dom rec ( 𝐹 , 𝐴 ) |
8 |
|
limord |
⊢ ( Lim dom rec ( 𝐹 , 𝐴 ) → Ord dom rec ( 𝐹 , 𝐴 ) ) |
9 |
7 8
|
ax-mp |
⊢ Ord dom rec ( 𝐹 , 𝐴 ) |
10 |
1 2 3 6 9
|
tz7.44-3 |
⊢ ( ( 𝐵 ∈ dom rec ( 𝐹 , 𝐴 ) ∧ Lim 𝐵 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝐵 ) = ∪ ( rec ( 𝐹 , 𝐴 ) “ 𝐵 ) ) |