Step |
Hyp |
Ref |
Expression |
1 |
|
tfr.1 |
|- F = recs ( G ) |
2 |
|
eqid |
|- { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) } = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) } |
3 |
2
|
tfrlem7 |
|- Fun recs ( G ) |
4 |
1
|
funeqi |
|- ( Fun F <-> Fun recs ( G ) ) |
5 |
3 4
|
mpbir |
|- Fun F |
6 |
2
|
tfrlem16 |
|- Lim dom recs ( G ) |
7 |
1
|
dmeqi |
|- dom F = dom recs ( G ) |
8 |
|
limeq |
|- ( dom F = dom recs ( G ) -> ( Lim dom F <-> Lim dom recs ( G ) ) ) |
9 |
7 8
|
ax-mp |
|- ( Lim dom F <-> Lim dom recs ( G ) ) |
10 |
6 9
|
mpbir |
|- Lim dom F |
11 |
5 10
|
pm3.2i |
|- ( Fun F /\ Lim dom F ) |