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

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 )