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

Metamath Proof Explorer

Theorem rdgprc0

Description: The value of the recursive definition generator at (/) when the base value is a proper class. (Contributed by Scott Fenton, 26-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion rdgprc0 
|- ( -. I e. _V -> ( rec ( F , I ) ` (/) ) = (/) )

Proof

Step Hyp Ref Expression
1 0elon 
 |-  (/) e. On
2 rdgval 
 |-  ( (/) e. On -> ( rec ( F , I ) ` (/) ) = ( ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( rec ( F , I ) |` (/) ) ) )
3 1 2 ax-mp 
 |-  ( rec ( F , I ) ` (/) ) = ( ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( rec ( F , I ) |` (/) ) )
4 res0 
 |-  ( rec ( F , I ) |` (/) ) = (/)
5 4 fveq2i 
 |-  ( ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( rec ( F , I ) |` (/) ) ) = ( ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` (/) )
6 3 5 eqtri 
 |-  ( rec ( F , I ) ` (/) ) = ( ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` (/) )
7 eqeq1 
 |-  ( g = (/) -> ( g = (/) <-> (/) = (/) ) )
8 dmeq 
 |-  ( g = (/) -> dom g = dom (/) )
9 limeq 
 |-  ( dom g = dom (/) -> ( Lim dom g <-> Lim dom (/) ) )
10 8 9 syl 
 |-  ( g = (/) -> ( Lim dom g <-> Lim dom (/) ) )
11 rneq 
 |-  ( g = (/) -> ran g = ran (/) )
12 11 unieqd 
 |-  ( g = (/) -> U. ran g = U. ran (/) )
13 id 
 |-  ( g = (/) -> g = (/) )
14 8 unieqd 
 |-  ( g = (/) -> U. dom g = U. dom (/) )
15 13 14 fveq12d 
 |-  ( g = (/) -> ( g ` U. dom g ) = ( (/) ` U. dom (/) ) )
16 15 fveq2d 
 |-  ( g = (/) -> ( F ` ( g ` U. dom g ) ) = ( F ` ( (/) ` U. dom (/) ) ) )
17 10 12 16 ifbieq12d 
 |-  ( g = (/) -> if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) = if ( Lim dom (/) , U. ran (/) , ( F ` ( (/) ` U. dom (/) ) ) ) )
18 7 17 ifbieq2d 
 |-  ( g = (/) -> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) = if ( (/) = (/) , I , if ( Lim dom (/) , U. ran (/) , ( F ` ( (/) ` U. dom (/) ) ) ) ) )
19 18 eleq1d 
 |-  ( g = (/) -> ( if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) e. _V <-> if ( (/) = (/) , I , if ( Lim dom (/) , U. ran (/) , ( F ` ( (/) ` U. dom (/) ) ) ) ) e. _V ) )
20 eqid 
 |-  ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) = ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) )
21 20 dmmpt 
 |-  dom ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) = { g e. _V | if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) e. _V }
22 19 21 elrab2 
 |-  ( (/) e. dom ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) <-> ( (/) e. _V /\ if ( (/) = (/) , I , if ( Lim dom (/) , U. ran (/) , ( F ` ( (/) ` U. dom (/) ) ) ) ) e. _V ) )
23 eqid 
 |-  (/) = (/)
24 23 iftruei 
 |-  if ( (/) = (/) , I , if ( Lim dom (/) , U. ran (/) , ( F ` ( (/) ` U. dom (/) ) ) ) ) = I
25 24 eleq1i 
 |-  ( if ( (/) = (/) , I , if ( Lim dom (/) , U. ran (/) , ( F ` ( (/) ` U. dom (/) ) ) ) ) e. _V <-> I e. _V )
26 25 biimpi 
 |-  ( if ( (/) = (/) , I , if ( Lim dom (/) , U. ran (/) , ( F ` ( (/) ` U. dom (/) ) ) ) ) e. _V -> I e. _V )
27 22 26 simplbiim 
 |-  ( (/) e. dom ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) -> I e. _V )
28 ndmfv 
 |-  ( -. (/) e. dom ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) -> ( ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` (/) ) = (/) )
29 27 28 nsyl5 
 |-  ( -. I e. _V -> ( ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` (/) ) = (/) )
30 6 29 eqtrid 
 |-  ( -. I e. _V -> ( rec ( F , I ) ` (/) ) = (/) )