Metamath Proof Explorer

Theorem bj-rdg0gALT

Description: Alternate proof of rdg0g . More direct since it bypasses tz7.44-1 and rdg0 (and vtoclg , vtoclga ). (Contributed by NM, 25-Apr-1995) More direct proof. (Revised by BJ, 17-Nov-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-rdg0gALT 
|- ( A e. V -> ( rec ( F , A ) ` (/) ) = A )

Proof

Step Hyp Ref Expression
1 rdgdmlim 
 |-  Lim dom rec ( F , A )
2 limomss 
 |-  ( Lim dom rec ( F , A ) -> _om C_ dom rec ( F , A ) )
3 1 2 ax-mp 
 |-  _om C_ dom rec ( F , A )
4 peano1 
 |-  (/) e. _om
5 3 4 sselii 
 |-  (/) e. dom rec ( F , A )
6 rdgvalg 
 |-  ( (/) e. dom rec ( F , A ) -> ( rec ( F , A ) ` (/) ) = ( ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) ) ` ( rec ( F , A ) |` (/) ) ) )
7 5 6 ax-mp 
 |-  ( rec ( F , A ) ` (/) ) = ( ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) ) ` ( rec ( F , A ) |` (/) ) )
8 res0 
 |-  ( rec ( F , A ) |` (/) ) = (/)
9 8 fveq2i 
 |-  ( ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) ) ` ( rec ( F , A ) |` (/) ) ) = ( ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) ) ` (/) )
10 eqid 
 |-  ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) ) = ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) )
11 simpr 
 |-  ( ( A e. V /\ x = (/) ) -> x = (/) )
12 11 iftrued 
 |-  ( ( A e. V /\ x = (/) ) -> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) = A )
13 0ex 
 |-  (/) e. _V
14 13 a1i 
 |-  ( A e. V -> (/) e. _V )
15 id 
 |-  ( A e. V -> A e. V )
16 10 12 14 15 fvmptd2 
 |-  ( A e. V -> ( ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) ) ` (/) ) = A )
17 9 16 syl5eq 
 |-  ( A e. V -> ( ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( F ` ( x ` U. dom x ) ) ) ) ) ` ( rec ( F , A ) |` (/) ) ) = A )
18 7 17 syl5eq 
 |-  ( A e. V -> ( rec ( F , A ) ` (/) ) = A )