Theorem inf3lemb

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	inf3lemb	$$⊢F\left(\varnothing \right)=\varnothing$$

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	2	fveq1i	$$⊢F\left(\varnothing \right)=\left({\mathrm{rec}\left(G,\varnothing \right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)$$
6		0ex	$$⊢\varnothing \in \mathrm{V}$$
7		fr0g	$$⊢\varnothing \in \mathrm{V}\to \left({\mathrm{rec}\left(G,\varnothing \right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)=\varnothing$$
8	6 7	ax-mp	$$⊢\left({\mathrm{rec}\left(G,\varnothing \right)\upharpoonright }_{\mathrm{\omega }}\right)\left(\varnothing \right)=\varnothing$$
9	5 8	eqtri	$$⊢F\left(\varnothing \right)=\varnothing$$