Theorem fr0g

Description: The initial value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996)

	Ref	Expression
Assertion	fr0g	$$⊢A\in B\to \left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)=A$$

Proof

Step	Hyp	Ref	Expression
1		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
2		fvres	$$⊢\varnothing \in \mathrm{\omega }\to \left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)=\mathrm{rec}\left(F,A\right)\left(\varnothing \right)$$
3	1 2	ax-mp	$$⊢\left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)=\mathrm{rec}\left(F,A\right)\left(\varnothing \right)$$
4		rdg0g	$$⊢A\in B\to \mathrm{rec}\left(F,A\right)\left(\varnothing \right)=A$$
5	3 4	eqtrid	$$⊢A\in B\to \left({\mathrm{rec}\left(F,A\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)=A$$