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=\left(x\in \mathrm{V}⟼if\left(x=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}x,\bigcup \mathrm{ran}x,H\left(x\left(\bigcup \mathrm{dom}x\right)\right)\right)\right)\right)$$
	tz7.44.2	$$⊢y\in X\to F\left(y\right)=G\left({F\upharpoonright }_y\right)$$
	tz7.44-1.3	$$⊢A\in \mathrm{V}$$
Assertion	tz7.44-1	$$⊢\varnothing \in X\to F\left(\varnothing \right)=A$$

Proof

Step	Hyp	Ref	Expression
1		tz7.44.1	$$⊢G=\left(x\in \mathrm{V}⟼if\left(x=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}x,\bigcup \mathrm{ran}x,H\left(x\left(\bigcup \mathrm{dom}x\right)\right)\right)\right)\right)$$
2		tz7.44.2	$$⊢y\in X\to F\left(y\right)=G\left({F\upharpoonright }_y\right)$$
3		tz7.44-1.3	$$⊢A\in \mathrm{V}$$
4		fveq2	$$⊢y=\varnothing \to F\left(y\right)=F\left(\varnothing \right)$$
5		reseq2	$$⊢y=\varnothing \to {F\upharpoonright }_y={F\upharpoonright }_{\varnothing }$$
6		res0	$$⊢{F\upharpoonright }_{\varnothing }=\varnothing$$
7	5 6	syl6eq	$$⊢y=\varnothing \to {F\upharpoonright }_y=\varnothing$$
8	7	fveq2d	$$⊢y=\varnothing \to G\left({F\upharpoonright }_y\right)=G\left(\varnothing \right)$$
9	4 8	eqeq12d	$$⊢y=\varnothing \to \left(F\left(y\right)=G\left({F\upharpoonright }_y\right)\leftrightarrow F\left(\varnothing \right)=G\left(\varnothing \right)\right)$$
10	9 2	vtoclga	$$⊢\varnothing \in X\to F\left(\varnothing \right)=G\left(\varnothing \right)$$
11		0ex	$$⊢\varnothing \in \mathrm{V}$$
12		iftrue	$$⊢x=\varnothing \to if\left(x=\varnothing ,A,if\left(\mathrm{Lim}\mathrm{dom}x,\bigcup \mathrm{ran}x,H\left(x\left(\bigcup \mathrm{dom}x\right)\right)\right)\right)=A$$
13	12 1 3	fvmpt	$$⊢\varnothing \in \mathrm{V}\to G\left(\varnothing \right)=A$$
14	11 13	ax-mp	$$⊢G\left(\varnothing \right)=A$$
15	10 14	syl6eq	$$⊢\varnothing \in X\to F\left(\varnothing \right)=A$$