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 V if x = A if Lim dom x ran x H x dom x
tz7.44.2 y X F y = G F y
tz7.44-1.3 A V
Assertion tz7.44-1 X F = A

Proof

Step Hyp Ref Expression
1 tz7.44.1 G = x V if x = A if Lim dom x ran x H x dom x
2 tz7.44.2 y X F y = G F y
3 tz7.44-1.3 A 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 X F = G
11 0ex V
12 iftrue x = if x = A if Lim dom x ran x H x dom x = A
13 12 1 3 fvmpt V G = A
14 11 13 ax-mp G = A
15 10 14 eqtrdi X F = A