Step |
Hyp |
Ref |
Expression |
1 |
|
tfrALT.1 |
|- F = recs ( G ) |
2 |
|
predon |
|- ( x e. On -> Pred ( _E , On , x ) = x ) |
3 |
2
|
reseq2d |
|- ( x e. On -> ( B |` Pred ( _E , On , x ) ) = ( B |` x ) ) |
4 |
3
|
fveq2d |
|- ( x e. On -> ( G ` ( B |` Pred ( _E , On , x ) ) ) = ( G ` ( B |` x ) ) ) |
5 |
4
|
eqeq2d |
|- ( x e. On -> ( ( B ` x ) = ( G ` ( B |` Pred ( _E , On , x ) ) ) <-> ( B ` x ) = ( G ` ( B |` x ) ) ) ) |
6 |
5
|
ralbiia |
|- ( A. x e. On ( B ` x ) = ( G ` ( B |` Pred ( _E , On , x ) ) ) <-> A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) |
7 |
|
epweon |
|- _E We On |
8 |
|
epse |
|- _E Se On |
9 |
|
df-recs |
|- recs ( G ) = wrecs ( _E , On , G ) |
10 |
1 9
|
eqtri |
|- F = wrecs ( _E , On , G ) |
11 |
10
|
wfr3 |
|- ( ( ( _E We On /\ _E Se On ) /\ ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` Pred ( _E , On , x ) ) ) ) ) -> F = B ) |
12 |
7 8 11
|
mpanl12 |
|- ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` Pred ( _E , On , x ) ) ) ) -> F = B ) |
13 |
6 12
|
sylan2br |
|- ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> F = B ) |
14 |
13
|
eqcomd |
|- ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> B = F ) |