Metamath Proof Explorer


Theorem tz7.44-1

Description: The value of F at (/) . Part 1 of Theorem 7.44 of TakeutiZaring p. 49. (Contributed by NM, 23-Apr-1995) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Hypotheses tz7.44.1
|- G = ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( H ` ( x ` U. dom x ) ) ) ) )
tz7.44.2
|- ( y e. X -> ( F ` y ) = ( G ` ( F |` y ) ) )
tz7.44-1.3
|- A e. _V
Assertion tz7.44-1
|- ( (/) e. X -> ( F ` (/) ) = A )

Proof

Step Hyp Ref Expression
1 tz7.44.1
 |-  G = ( x e. _V |-> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( H ` ( x ` U. dom x ) ) ) ) )
2 tz7.44.2
 |-  ( y e. X -> ( F ` y ) = ( G ` ( F |` y ) ) )
3 tz7.44-1.3
 |-  A e. _V
4 fveq2
 |-  ( y = (/) -> ( F ` y ) = ( F ` (/) ) )
5 reseq2
 |-  ( y = (/) -> ( F |` y ) = ( F |` (/) ) )
6 res0
 |-  ( F |` (/) ) = (/)
7 5 6 eqtrdi
 |-  ( y = (/) -> ( F |` y ) = (/) )
8 7 fveq2d
 |-  ( y = (/) -> ( G ` ( F |` y ) ) = ( G ` (/) ) )
9 4 8 eqeq12d
 |-  ( y = (/) -> ( ( F ` y ) = ( G ` ( F |` y ) ) <-> ( F ` (/) ) = ( G ` (/) ) ) )
10 9 2 vtoclga
 |-  ( (/) e. X -> ( F ` (/) ) = ( G ` (/) ) )
11 0ex
 |-  (/) e. _V
12 iftrue
 |-  ( x = (/) -> if ( x = (/) , A , if ( Lim dom x , U. ran x , ( H ` ( x ` U. dom x ) ) ) ) = A )
13 12 1 3 fvmpt
 |-  ( (/) e. _V -> ( G ` (/) ) = A )
14 11 13 ax-mp
 |-  ( G ` (/) ) = A
15 10 14 eqtrdi
 |-  ( (/) e. X -> ( F ` (/) ) = A )