This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfrdg3

Description: Generalization of dfrdg2 to remove sethood requirement. (Contributed by Scott Fenton, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion dfrdg3 
|- rec ( F , I ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) }

Proof

Step Hyp Ref Expression
1 dfrdg2 
 |-  ( I e. _V -> rec ( F , I ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } )
2 iftrue 
 |-  ( I e. _V -> if ( I e. _V , I , (/) ) = I )
3 2 ifeq1d 
 |-  ( I e. _V -> if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) )
4 3 eqeq2d 
 |-  ( I e. _V -> ( ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) <-> ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
5 4 ralbidv 
 |-  ( I e. _V -> ( A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) <-> A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
6 5 anbi2d 
 |-  ( I e. _V -> ( ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) <-> ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
7 6 rexbidv 
 |-  ( I e. _V -> ( E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) <-> E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
8 7 abbidv 
 |-  ( I e. _V -> { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } )
9 8 unieqd 
 |-  ( I e. _V -> U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , I , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } )
10 1 9 eqtr4d 
 |-  ( I e. _V -> rec ( F , I ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } )
11 0ex 
 |-  (/) e. _V
12 dfrdg2 
 |-  ( (/) e. _V -> rec ( F , (/) ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , (/) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } )
13 11 12 ax-mp 
 |-  rec ( F , (/) ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , (/) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) }
14 rdgprc 
 |-  ( -. I e. _V -> rec ( F , I ) = rec ( F , (/) ) )
15 iffalse 
 |-  ( -. I e. _V -> if ( I e. _V , I , (/) ) = (/) )
16 15 ifeq1d 
 |-  ( -. I e. _V -> if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) = if ( y = (/) , (/) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) )
17 16 eqeq2d 
 |-  ( -. I e. _V -> ( ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) <-> ( f ` y ) = if ( y = (/) , (/) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
18 17 ralbidv 
 |-  ( -. I e. _V -> ( A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) <-> A. y e. x ( f ` y ) = if ( y = (/) , (/) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) )
19 18 anbi2d 
 |-  ( -. I e. _V -> ( ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) <-> ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , (/) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
20 19 rexbidv 
 |-  ( -. I e. _V -> ( E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) <-> E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , (/) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) ) )
21 20 abbidv 
 |-  ( -. I e. _V -> { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , (/) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } )
22 21 unieqd 
 |-  ( -. I e. _V -> U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , (/) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } )
23 13 14 22 3eqtr4a 
 |-  ( -. I e. _V -> rec ( F , I ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) } )
24 10 23 pm2.61i 
 |-  rec ( F , I ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = if ( y = (/) , if ( I e. _V , I , (/) ) , if ( Lim y , U. ( f " y ) , ( F ` ( f ` U. y ) ) ) ) ) }