Step |
Hyp |
Ref |
Expression |
1 |
|
tfr.1 |
|- F = recs ( G ) |
2 |
|
ordeleqon |
|- ( Ord A <-> ( A e. On \/ A = On ) ) |
3 |
|
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 ) ) ) } |
4 |
3
|
tfrlem15 |
|- ( A e. On -> ( A e. dom recs ( G ) <-> ( recs ( G ) |` A ) e. _V ) ) |
5 |
1
|
dmeqi |
|- dom F = dom recs ( G ) |
6 |
5
|
eleq2i |
|- ( A e. dom F <-> A e. dom recs ( G ) ) |
7 |
1
|
reseq1i |
|- ( F |` A ) = ( recs ( G ) |` A ) |
8 |
7
|
eleq1i |
|- ( ( F |` A ) e. _V <-> ( recs ( G ) |` A ) e. _V ) |
9 |
4 6 8
|
3bitr4g |
|- ( A e. On -> ( A e. dom F <-> ( F |` A ) e. _V ) ) |
10 |
|
onprc |
|- -. On e. _V |
11 |
|
elex |
|- ( On e. dom F -> On e. _V ) |
12 |
10 11
|
mto |
|- -. On e. dom F |
13 |
|
eleq1 |
|- ( A = On -> ( A e. dom F <-> On e. dom F ) ) |
14 |
12 13
|
mtbiri |
|- ( A = On -> -. A e. dom F ) |
15 |
3
|
tfrlem13 |
|- -. recs ( G ) e. _V |
16 |
1 15
|
eqneltri |
|- -. F e. _V |
17 |
|
reseq2 |
|- ( A = On -> ( F |` A ) = ( F |` On ) ) |
18 |
1
|
tfr1a |
|- ( Fun F /\ Lim dom F ) |
19 |
18
|
simpli |
|- Fun F |
20 |
|
funrel |
|- ( Fun F -> Rel F ) |
21 |
19 20
|
ax-mp |
|- Rel F |
22 |
18
|
simpri |
|- Lim dom F |
23 |
|
limord |
|- ( Lim dom F -> Ord dom F ) |
24 |
|
ordsson |
|- ( Ord dom F -> dom F C_ On ) |
25 |
22 23 24
|
mp2b |
|- dom F C_ On |
26 |
|
relssres |
|- ( ( Rel F /\ dom F C_ On ) -> ( F |` On ) = F ) |
27 |
21 25 26
|
mp2an |
|- ( F |` On ) = F |
28 |
17 27
|
eqtrdi |
|- ( A = On -> ( F |` A ) = F ) |
29 |
28
|
eleq1d |
|- ( A = On -> ( ( F |` A ) e. _V <-> F e. _V ) ) |
30 |
16 29
|
mtbiri |
|- ( A = On -> -. ( F |` A ) e. _V ) |
31 |
14 30
|
2falsed |
|- ( A = On -> ( A e. dom F <-> ( F |` A ) e. _V ) ) |
32 |
9 31
|
jaoi |
|- ( ( A e. On \/ A = On ) -> ( A e. dom F <-> ( F |` A ) e. _V ) ) |
33 |
2 32
|
sylbi |
|- ( Ord A -> ( A e. dom F <-> ( F |` A ) e. _V ) ) |