Step |
Hyp |
Ref |
Expression |
1 |
|
rdglim |
|- ( ( B e. C /\ Lim B ) -> ( rec ( F , A ) ` B ) = U. ( rec ( F , A ) " B ) ) |
2 |
|
dfima3 |
|- ( rec ( F , A ) " B ) = { y | E. x ( x e. B /\ <. x , y >. e. rec ( F , A ) ) } |
3 |
|
df-rex |
|- ( E. x e. B y = ( rec ( F , A ) ` x ) <-> E. x ( x e. B /\ y = ( rec ( F , A ) ` x ) ) ) |
4 |
|
limord |
|- ( Lim B -> Ord B ) |
5 |
|
ordelord |
|- ( ( Ord B /\ x e. B ) -> Ord x ) |
6 |
5
|
ex |
|- ( Ord B -> ( x e. B -> Ord x ) ) |
7 |
|
vex |
|- x e. _V |
8 |
7
|
elon |
|- ( x e. On <-> Ord x ) |
9 |
6 8
|
syl6ibr |
|- ( Ord B -> ( x e. B -> x e. On ) ) |
10 |
4 9
|
syl |
|- ( Lim B -> ( x e. B -> x e. On ) ) |
11 |
|
eqcom |
|- ( y = ( rec ( F , A ) ` x ) <-> ( rec ( F , A ) ` x ) = y ) |
12 |
|
rdgfnon |
|- rec ( F , A ) Fn On |
13 |
|
fnopfvb |
|- ( ( rec ( F , A ) Fn On /\ x e. On ) -> ( ( rec ( F , A ) ` x ) = y <-> <. x , y >. e. rec ( F , A ) ) ) |
14 |
12 13
|
mpan |
|- ( x e. On -> ( ( rec ( F , A ) ` x ) = y <-> <. x , y >. e. rec ( F , A ) ) ) |
15 |
11 14
|
syl5bb |
|- ( x e. On -> ( y = ( rec ( F , A ) ` x ) <-> <. x , y >. e. rec ( F , A ) ) ) |
16 |
10 15
|
syl6 |
|- ( Lim B -> ( x e. B -> ( y = ( rec ( F , A ) ` x ) <-> <. x , y >. e. rec ( F , A ) ) ) ) |
17 |
16
|
pm5.32d |
|- ( Lim B -> ( ( x e. B /\ y = ( rec ( F , A ) ` x ) ) <-> ( x e. B /\ <. x , y >. e. rec ( F , A ) ) ) ) |
18 |
17
|
exbidv |
|- ( Lim B -> ( E. x ( x e. B /\ y = ( rec ( F , A ) ` x ) ) <-> E. x ( x e. B /\ <. x , y >. e. rec ( F , A ) ) ) ) |
19 |
3 18
|
bitr2id |
|- ( Lim B -> ( E. x ( x e. B /\ <. x , y >. e. rec ( F , A ) ) <-> E. x e. B y = ( rec ( F , A ) ` x ) ) ) |
20 |
19
|
abbidv |
|- ( Lim B -> { y | E. x ( x e. B /\ <. x , y >. e. rec ( F , A ) ) } = { y | E. x e. B y = ( rec ( F , A ) ` x ) } ) |
21 |
2 20
|
eqtrid |
|- ( Lim B -> ( rec ( F , A ) " B ) = { y | E. x e. B y = ( rec ( F , A ) ` x ) } ) |
22 |
21
|
unieqd |
|- ( Lim B -> U. ( rec ( F , A ) " B ) = U. { y | E. x e. B y = ( rec ( F , A ) ` x ) } ) |
23 |
22
|
adantl |
|- ( ( B e. C /\ Lim B ) -> U. ( rec ( F , A ) " B ) = U. { y | E. x e. B y = ( rec ( F , A ) ` x ) } ) |
24 |
1 23
|
eqtrd |
|- ( ( B e. C /\ Lim B ) -> ( rec ( F , A ) ` B ) = U. { y | E. x e. B y = ( rec ( F , A ) ` x ) } ) |