Metamath Proof Explorer

Theorem rdg0n

Description: If A is a proper class, then the recursive function generator at (/) is the empty set. (Contributed by Scott Fenton, 31-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 0elon 
 |-  (/) e. On
2 df-rdg 
 |-  rec ( F , A ) = recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )
3 2 tfr2 
 |-  ( (/) e. On -> ( rec ( F , A ) ` (/) ) = ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( rec ( F , A ) |` (/) ) ) )
4 1 3 ax-mp 
 |-  ( rec ( F , A ) ` (/) ) = ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( rec ( F , A ) |` (/) ) )
5 res0 
 |-  ( rec ( F , A ) |` (/) ) = (/)
6 5 fveq2i 
 |-  ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` ( rec ( F , A ) |` (/) ) ) = ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` (/) )
7 4 6 eqtri 
 |-  ( rec ( F , A ) ` (/) ) = ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` (/) )
8 iftrue 
 |-  ( g = (/) -> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) = A )
9 eqid 
 |-  ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) = ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) )
10 8 9 fvmptn 
 |-  ( -. A e. _V -> ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ` (/) ) = (/) )
11 7 10 eqtrid 
 |-  ( -. A e. _V -> ( rec ( F , A ) ` (/) ) = (/) )