Theorem infpssrlem1

Description: Lemma for infpssr . (Contributed by Stefan O'Rear, 30-Oct-2014)

	Ref	Expression
Hypotheses	infpssrlem.a	$$⊢\phi \to B\subseteq A$$
	infpssrlem.c	$$⊢\phi \to F:B\underset{1-1\; onto}{⟶}A$$
	infpssrlem.d	$$⊢\phi \to C\in \left(A\setminus B\right)$$
	infpssrlem.e	$$⊢G={\mathrm{rec}\left(F^{-1},C\right)\upharpoonright }_{\mathrm{\omega }}$$
Assertion	infpssrlem1	$$⊢\phi \to G\left(\varnothing \right)=C$$

Proof

Step	Hyp	Ref	Expression
1		infpssrlem.a	$$⊢\phi \to B\subseteq A$$
2		infpssrlem.c	$$⊢\phi \to F:B\underset{1-1\; onto}{⟶}A$$
3		infpssrlem.d	$$⊢\phi \to C\in \left(A\setminus B\right)$$
4		infpssrlem.e	$$⊢G={\mathrm{rec}\left(F^{-1},C\right)\upharpoonright }_{\mathrm{\omega }}$$
5	4	fveq1i	$$⊢G\left(\varnothing \right)=\left({\mathrm{rec}\left(F^{-1},C\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)$$
6		fr0g	$$⊢C\in \left(A\setminus B\right)\to \left({\mathrm{rec}\left(F^{-1},C\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)=C$$
7	3 6	syl	$$⊢\phi \to \left({\mathrm{rec}\left(F^{-1},C\right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)=C$$
8	5 7	syl5eq	$$⊢\phi \to G\left(\varnothing \right)=C$$