Theorem inf3lemc

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 28-Oct-1996)

	Ref	Expression
Hypotheses	inf3lem.1	$$⊢G=\left(y\in \mathrm{V}⟼\left\{w\in x|w\cap x\subseteq y\right\}\right)$$
	inf3lem.2	$$⊢F={\mathrm{rec}\left(G,\varnothing \right)\upharpoonright }_{\mathrm{\omega }}$$
	inf3lem.3	$$⊢A\in \mathrm{V}$$
	inf3lem.4	$$⊢B\in \mathrm{V}$$
Assertion	inf3lemc	$$⊢A\in \mathrm{\omega }\to F\left(\mathrm{suc}A\right)=G\left(F\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		inf3lem.1	$$⊢G=\left(y\in \mathrm{V}⟼\left\{w\in x|w\cap x\subseteq y\right\}\right)$$
2		inf3lem.2	$$⊢F={\mathrm{rec}\left(G,\varnothing \right)\upharpoonright }_{\mathrm{\omega }}$$
3		inf3lem.3	$$⊢A\in \mathrm{V}$$
4		inf3lem.4	$$⊢B\in \mathrm{V}$$
5		frsuc	$$⊢A\in \mathrm{\omega }\to \left({\mathrm{rec}\left(G,\varnothing \right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\mathrm{suc}A\right)=G\left(\left({\mathrm{rec}\left(G,\varnothing \right)\upharpoonright }_{\mathrm{\omega }}\right)\left(A\right)\right)$$
6	2	fveq1i	$$⊢F\left(\mathrm{suc}A\right)=\left({\mathrm{rec}\left(G,\varnothing \right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\mathrm{suc}A\right)$$
7	2	fveq1i	$$⊢F\left(A\right)=\left({\mathrm{rec}\left(G,\varnothing \right)\upharpoonright }_{\mathrm{\omega }}\right)\left(A\right)$$
8	7	fveq2i	$$⊢G\left(F\left(A\right)\right)=G\left(\left({\mathrm{rec}\left(G,\varnothing \right)\upharpoonright }_{\mathrm{\omega }}\right)\left(A\right)\right)$$
9	5 6 8	3eqtr4g	$$⊢A\in \mathrm{\omega }\to F\left(\mathrm{suc}A\right)=G\left(F\left(A\right)\right)$$