Theorem inf3lem1

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	inf3lem1	$$⊢A\in \mathrm{\omega }\to F\left(A\right)\subseteq F\left(\mathrm{suc}A\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		fveq2	$$⊢v=\varnothing \to F\left(v\right)=F\left(\varnothing \right)$$
6		suceq	$$⊢v=\varnothing \to \mathrm{suc}v=\mathrm{suc}\varnothing$$
7	6	fveq2d	$$⊢v=\varnothing \to F\left(\mathrm{suc}v\right)=F\left(\mathrm{suc}\varnothing \right)$$
8	5 7	sseq12d	$$⊢v=\varnothing \to \left(F\left(v\right)\subseteq F\left(\mathrm{suc}v\right)\leftrightarrow F\left(\varnothing \right)\subseteq F\left(\mathrm{suc}\varnothing \right)\right)$$
9		fveq2	$$⊢v=u\to F\left(v\right)=F\left(u\right)$$
10		suceq	$$⊢v=u\to \mathrm{suc}v=\mathrm{suc}u$$
11	10	fveq2d	$$⊢v=u\to F\left(\mathrm{suc}v\right)=F\left(\mathrm{suc}u\right)$$
12	9 11	sseq12d	$$⊢v=u\to \left(F\left(v\right)\subseteq F\left(\mathrm{suc}v\right)\leftrightarrow F\left(u\right)\subseteq F\left(\mathrm{suc}u\right)\right)$$
13		fveq2	$$⊢v=\mathrm{suc}u\to F\left(v\right)=F\left(\mathrm{suc}u\right)$$
14		suceq	$$⊢v=\mathrm{suc}u\to \mathrm{suc}v=\mathrm{suc}\mathrm{suc}u$$
15	14	fveq2d	$$⊢v=\mathrm{suc}u\to F\left(\mathrm{suc}v\right)=F\left(\mathrm{suc}\mathrm{suc}u\right)$$
16	13 15	sseq12d	$$⊢v=\mathrm{suc}u\to \left(F\left(v\right)\subseteq F\left(\mathrm{suc}v\right)\leftrightarrow F\left(\mathrm{suc}u\right)\subseteq F\left(\mathrm{suc}\mathrm{suc}u\right)\right)$$
17		fveq2	$$⊢v=A\to F\left(v\right)=F\left(A\right)$$
18		suceq	$$⊢v=A\to \mathrm{suc}v=\mathrm{suc}A$$
19	18	fveq2d	$$⊢v=A\to F\left(\mathrm{suc}v\right)=F\left(\mathrm{suc}A\right)$$
20	17 19	sseq12d	$$⊢v=A\to \left(F\left(v\right)\subseteq F\left(\mathrm{suc}v\right)\leftrightarrow F\left(A\right)\subseteq F\left(\mathrm{suc}A\right)\right)$$
21	1 2 3 3	inf3lemb	$$⊢F\left(\varnothing \right)=\varnothing$$
22		0ss	$$⊢\varnothing \subseteq F\left(\mathrm{suc}\varnothing \right)$$
23	21 22	eqsstri	$$⊢F\left(\varnothing \right)\subseteq F\left(\mathrm{suc}\varnothing \right)$$
24		sstr2	$$⊢v\cap x\subseteq F\left(u\right)\to \left(F\left(u\right)\subseteq F\left(\mathrm{suc}u\right)\to v\cap x\subseteq F\left(\mathrm{suc}u\right)\right)$$
25	24	com12	$$⊢F\left(u\right)\subseteq F\left(\mathrm{suc}u\right)\to \left(v\cap x\subseteq F\left(u\right)\to v\cap x\subseteq F\left(\mathrm{suc}u\right)\right)$$
26	25	anim2d	$$⊢F\left(u\right)\subseteq F\left(\mathrm{suc}u\right)\to \left(\left(v\in x\wedge v\cap x\subseteq F\left(u\right)\right)\to \left(v\in x\wedge v\cap x\subseteq F\left(\mathrm{suc}u\right)\right)\right)$$
27		vex	$$⊢u\in \mathrm{V}$$
28	1 2 27 3	inf3lemc	$$⊢u\in \mathrm{\omega }\to F\left(\mathrm{suc}u\right)=G\left(F\left(u\right)\right)$$
29	28	eleq2d	$$⊢u\in \mathrm{\omega }\to \left(v\in F\left(\mathrm{suc}u\right)\leftrightarrow v\in G\left(F\left(u\right)\right)\right)$$
30		vex	$$⊢v\in \mathrm{V}$$
31		fvex	$$⊢F\left(u\right)\in \mathrm{V}$$
32	1 2 30 31	inf3lema	$$⊢v\in G\left(F\left(u\right)\right)\leftrightarrow \left(v\in x\wedge v\cap x\subseteq F\left(u\right)\right)$$
33	29 32	bitrdi	$$⊢u\in \mathrm{\omega }\to \left(v\in F\left(\mathrm{suc}u\right)\leftrightarrow \left(v\in x\wedge v\cap x\subseteq F\left(u\right)\right)\right)$$
34		peano2b	$$⊢u\in \mathrm{\omega }\leftrightarrow \mathrm{suc}u\in \mathrm{\omega }$$
35	27	sucex	$$⊢\mathrm{suc}u\in \mathrm{V}$$
36	1 2 35 3	inf3lemc	$$⊢\mathrm{suc}u\in \mathrm{\omega }\to F\left(\mathrm{suc}\mathrm{suc}u\right)=G\left(F\left(\mathrm{suc}u\right)\right)$$
37	34 36	sylbi	$$⊢u\in \mathrm{\omega }\to F\left(\mathrm{suc}\mathrm{suc}u\right)=G\left(F\left(\mathrm{suc}u\right)\right)$$
38	37	eleq2d	$$⊢u\in \mathrm{\omega }\to \left(v\in F\left(\mathrm{suc}\mathrm{suc}u\right)\leftrightarrow v\in G\left(F\left(\mathrm{suc}u\right)\right)\right)$$
39		fvex	$$⊢F\left(\mathrm{suc}u\right)\in \mathrm{V}$$
40	1 2 30 39	inf3lema	$$⊢v\in G\left(F\left(\mathrm{suc}u\right)\right)\leftrightarrow \left(v\in x\wedge v\cap x\subseteq F\left(\mathrm{suc}u\right)\right)$$
41	38 40	bitrdi	$$⊢u\in \mathrm{\omega }\to \left(v\in F\left(\mathrm{suc}\mathrm{suc}u\right)\leftrightarrow \left(v\in x\wedge v\cap x\subseteq F\left(\mathrm{suc}u\right)\right)\right)$$
42	33 41	imbi12d	$$⊢u\in \mathrm{\omega }\to \left(\left(v\in F\left(\mathrm{suc}u\right)\to v\in F\left(\mathrm{suc}\mathrm{suc}u\right)\right)\leftrightarrow \left(\left(v\in x\wedge v\cap x\subseteq F\left(u\right)\right)\to \left(v\in x\wedge v\cap x\subseteq F\left(\mathrm{suc}u\right)\right)\right)\right)$$
43	26 42	syl5ibr	$$⊢u\in \mathrm{\omega }\to \left(F\left(u\right)\subseteq F\left(\mathrm{suc}u\right)\to \left(v\in F\left(\mathrm{suc}u\right)\to v\in F\left(\mathrm{suc}\mathrm{suc}u\right)\right)\right)$$
44	43	imp	$$⊢\left(u\in \mathrm{\omega }\wedge F\left(u\right)\subseteq F\left(\mathrm{suc}u\right)\right)\to \left(v\in F\left(\mathrm{suc}u\right)\to v\in F\left(\mathrm{suc}\mathrm{suc}u\right)\right)$$
45	44	ssrdv	$$⊢\left(u\in \mathrm{\omega }\wedge F\left(u\right)\subseteq F\left(\mathrm{suc}u\right)\right)\to F\left(\mathrm{suc}u\right)\subseteq F\left(\mathrm{suc}\mathrm{suc}u\right)$$
46	45	ex	$$⊢u\in \mathrm{\omega }\to \left(F\left(u\right)\subseteq F\left(\mathrm{suc}u\right)\to F\left(\mathrm{suc}u\right)\subseteq F\left(\mathrm{suc}\mathrm{suc}u\right)\right)$$
47	8 12 16 20 23 46	finds	$$⊢A\in \mathrm{\omega }\to F\left(A\right)\subseteq F\left(\mathrm{suc}A\right)$$