Metamath Proof Explorer

Theorem rdglim2

Description: The value of the recursive definition generator at a limit ordinal, in terms of the union of all smaller values. (Contributed by NM, 23-Apr-1995)

Ref Expression
Assertion rdglim2 
|- ( ( B e. C /\ Lim B ) -> ( rec ( F , A ) ` B ) = U. { y | E. x e. B y = ( rec ( F , A ) ` x ) } )

Proof

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 bitrid 
 |-  ( 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 ) } )