Theorem inf3lemd

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	inf3lemd	$$⊢A\in \mathrm{\omega }\to F\left(A\right)\subseteq x$$

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		fveq2	$$⊢A=\varnothing \to F\left(A\right)=F\left(\varnothing \right)$$
6	1 2 3 4	inf3lemb	$$⊢F\left(\varnothing \right)=\varnothing$$
7	5 6	eqtrdi	$$⊢A=\varnothing \to F\left(A\right)=\varnothing$$
8		0ss	$$⊢\varnothing \subseteq x$$
9	7 8	eqsstrdi	$$⊢A=\varnothing \to F\left(A\right)\subseteq x$$
10	9	a1d	$$⊢A=\varnothing \to \left(A\in \mathrm{\omega }\to F\left(A\right)\subseteq x\right)$$
11		nnsuc	$$⊢\left(A\in \mathrm{\omega }\wedge A\ne \varnothing \right)\to \exists v\in \mathrm{\omega }A=\mathrm{suc}v$$
12		vex	$$⊢v\in \mathrm{V}$$
13	1 2 12 4	inf3lemc	$$⊢v\in \mathrm{\omega }\to F\left(\mathrm{suc}v\right)=G\left(F\left(v\right)\right)$$
14	13	eleq2d	$$⊢v\in \mathrm{\omega }\to \left(u\in F\left(\mathrm{suc}v\right)\leftrightarrow u\in G\left(F\left(v\right)\right)\right)$$
15		vex	$$⊢u\in \mathrm{V}$$
16		fvex	$$⊢F\left(v\right)\in \mathrm{V}$$
17	1 2 15 16	inf3lema	$$⊢u\in G\left(F\left(v\right)\right)\leftrightarrow \left(u\in x\wedge u\cap x\subseteq F\left(v\right)\right)$$
18	17	simplbi	$$⊢u\in G\left(F\left(v\right)\right)\to u\in x$$
19	14 18	syl6bi	$$⊢v\in \mathrm{\omega }\to \left(u\in F\left(\mathrm{suc}v\right)\to u\in x\right)$$
20	19	ssrdv	$$⊢v\in \mathrm{\omega }\to F\left(\mathrm{suc}v\right)\subseteq x$$
21		fveq2	$$⊢A=\mathrm{suc}v\to F\left(A\right)=F\left(\mathrm{suc}v\right)$$
22	21	sseq1d	$$⊢A=\mathrm{suc}v\to \left(F\left(A\right)\subseteq x\leftrightarrow F\left(\mathrm{suc}v\right)\subseteq x\right)$$
23	20 22	syl5ibrcom	$$⊢v\in \mathrm{\omega }\to \left(A=\mathrm{suc}v\to F\left(A\right)\subseteq x\right)$$
24	23	rexlimiv	$$⊢\exists v\in \mathrm{\omega }A=\mathrm{suc}v\to F\left(A\right)\subseteq x$$
25	11 24	syl	$$⊢\left(A\in \mathrm{\omega }\wedge A\ne \varnothing \right)\to F\left(A\right)\subseteq x$$
26	25	expcom	$$⊢A\ne \varnothing \to \left(A\in \mathrm{\omega }\to F\left(A\right)\subseteq x\right)$$
27	10 26	pm2.61ine	$$⊢A\in \mathrm{\omega }\to F\left(A\right)\subseteq x$$