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 )