Theorem inf3lem4

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 29-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	inf3lem4	$$⊢\left(x\ne \varnothing \wedge x\subseteq \bigcup x\right)\to \left(A\in \mathrm{\omega }\to F\left(A\right)\subset F\left(\mathrm{suc}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	1 2 3 4	inf3lem1	$$⊢A\in \mathrm{\omega }\to F\left(A\right)\subseteq F\left(\mathrm{suc}A\right)$$
6	5	a1i	$$⊢\left(x\ne \varnothing \wedge x\subseteq \bigcup x\right)\to \left(A\in \mathrm{\omega }\to F\left(A\right)\subseteq F\left(\mathrm{suc}A\right)\right)$$
7	1 2 3 4	inf3lem3	$$⊢\left(x\ne \varnothing \wedge x\subseteq \bigcup x\right)\to \left(A\in \mathrm{\omega }\to F\left(A\right)\ne F\left(\mathrm{suc}A\right)\right)$$
8	6 7	jcad	$$⊢\left(x\ne \varnothing \wedge x\subseteq \bigcup x\right)\to \left(A\in \mathrm{\omega }\to \left(F\left(A\right)\subseteq F\left(\mathrm{suc}A\right)\wedge F\left(A\right)\ne F\left(\mathrm{suc}A\right)\right)\right)$$
9		df-pss	$$⊢F\left(A\right)\subset F\left(\mathrm{suc}A\right)\leftrightarrow \left(F\left(A\right)\subseteq F\left(\mathrm{suc}A\right)\wedge F\left(A\right)\ne F\left(\mathrm{suc}A\right)\right)$$
10	8 9	imbitrrdi	$$⊢\left(x\ne \varnothing \wedge x\subseteq \bigcup x\right)\to \left(A\in \mathrm{\omega }\to F\left(A\right)\subset F\left(\mathrm{suc}A\right)\right)$$