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