Theorem inf3lem3

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg . (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	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)$$

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	inf3lemd	$$⊢A\in \mathrm{\omega }\to F\left(A\right)\subseteq x$$
6	1 2 3 4	inf3lem2	$$⊢\left(x\ne \varnothing \wedge x\subseteq \bigcup x\right)\to \left(A\in \mathrm{\omega }\to F\left(A\right)\ne x\right)$$
7	6	com12	$$⊢A\in \mathrm{\omega }\to \left(\left(x\ne \varnothing \wedge x\subseteq \bigcup x\right)\to F\left(A\right)\ne x\right)$$
8		pssdifn0	$$⊢\left(F\left(A\right)\subseteq x\wedge F\left(A\right)\ne x\right)\to x\setminus F\left(A\right)\ne \varnothing$$
9	5 7 8	syl6an	$$⊢A\in \mathrm{\omega }\to \left(\left(x\ne \varnothing \wedge x\subseteq \bigcup x\right)\to x\setminus F\left(A\right)\ne \varnothing \right)$$
10		vex	$$⊢x\in \mathrm{V}$$
11	10	difexi	$$⊢x\setminus F\left(A\right)\in \mathrm{V}$$
12		zfreg	$$⊢\left(x\setminus F\left(A\right)\in \mathrm{V}\wedge x\setminus F\left(A\right)\ne \varnothing \right)\to \exists v\in \left(x\setminus F\left(A\right)\right)v\cap \left(x\setminus F\left(A\right)\right)=\varnothing$$
13	11 12	mpan	$$⊢x\setminus F\left(A\right)\ne \varnothing \to \exists v\in \left(x\setminus F\left(A\right)\right)v\cap \left(x\setminus F\left(A\right)\right)=\varnothing$$
14		eldifi	$$⊢v\in \left(x\setminus F\left(A\right)\right)\to v\in x$$
15		inssdif0	$$⊢v\cap x\subseteq F\left(A\right)\leftrightarrow v\cap \left(x\setminus F\left(A\right)\right)=\varnothing$$
16	15	biimpri	$$⊢v\cap \left(x\setminus F\left(A\right)\right)=\varnothing \to v\cap x\subseteq F\left(A\right)$$
17	14 16	anim12i	$$⊢\left(v\in \left(x\setminus F\left(A\right)\right)\wedge v\cap \left(x\setminus F\left(A\right)\right)=\varnothing \right)\to \left(v\in x\wedge v\cap x\subseteq F\left(A\right)\right)$$
18		vex	$$⊢v\in \mathrm{V}$$
19		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
20	1 2 18 19	inf3lema	$$⊢v\in G\left(F\left(A\right)\right)\leftrightarrow \left(v\in x\wedge v\cap x\subseteq F\left(A\right)\right)$$
21	17 20	sylibr	$$⊢\left(v\in \left(x\setminus F\left(A\right)\right)\wedge v\cap \left(x\setminus F\left(A\right)\right)=\varnothing \right)\to v\in G\left(F\left(A\right)\right)$$
22	1 2 3 4	inf3lemc	$$⊢A\in \mathrm{\omega }\to F\left(\mathrm{suc}A\right)=G\left(F\left(A\right)\right)$$
23	22	eleq2d	$$⊢A\in \mathrm{\omega }\to \left(v\in F\left(\mathrm{suc}A\right)\leftrightarrow v\in G\left(F\left(A\right)\right)\right)$$
24	21 23	syl5ibr	$$⊢A\in \mathrm{\omega }\to \left(\left(v\in \left(x\setminus F\left(A\right)\right)\wedge v\cap \left(x\setminus F\left(A\right)\right)=\varnothing \right)\to v\in F\left(\mathrm{suc}A\right)\right)$$
25		eldifn	$$⊢v\in \left(x\setminus F\left(A\right)\right)\to \neg v\in F\left(A\right)$$
26	25	adantr	$$⊢\left(v\in \left(x\setminus F\left(A\right)\right)\wedge v\cap \left(x\setminus F\left(A\right)\right)=\varnothing \right)\to \neg v\in F\left(A\right)$$
27	24 26	jca2	$$⊢A\in \mathrm{\omega }\to \left(\left(v\in \left(x\setminus F\left(A\right)\right)\wedge v\cap \left(x\setminus F\left(A\right)\right)=\varnothing \right)\to \left(v\in F\left(\mathrm{suc}A\right)\wedge \neg v\in F\left(A\right)\right)\right)$$
28		eleq2	$$⊢F\left(A\right)=F\left(\mathrm{suc}A\right)\to \left(v\in F\left(A\right)\leftrightarrow v\in F\left(\mathrm{suc}A\right)\right)$$
29	28	biimprd	$$⊢F\left(A\right)=F\left(\mathrm{suc}A\right)\to \left(v\in F\left(\mathrm{suc}A\right)\to v\in F\left(A\right)\right)$$
30		iman	$$⊢\left(v\in F\left(\mathrm{suc}A\right)\to v\in F\left(A\right)\right)\leftrightarrow \neg \left(v\in F\left(\mathrm{suc}A\right)\wedge \neg v\in F\left(A\right)\right)$$
31	29 30	sylib	$$⊢F\left(A\right)=F\left(\mathrm{suc}A\right)\to \neg \left(v\in F\left(\mathrm{suc}A\right)\wedge \neg v\in F\left(A\right)\right)$$
32	31	necon2ai	$$⊢\left(v\in F\left(\mathrm{suc}A\right)\wedge \neg v\in F\left(A\right)\right)\to F\left(A\right)\ne F\left(\mathrm{suc}A\right)$$
33	27 32	syl6	$$⊢A\in \mathrm{\omega }\to \left(\left(v\in \left(x\setminus F\left(A\right)\right)\wedge v\cap \left(x\setminus F\left(A\right)\right)=\varnothing \right)\to F\left(A\right)\ne F\left(\mathrm{suc}A\right)\right)$$
34	33	expd	$$⊢A\in \mathrm{\omega }\to \left(v\in \left(x\setminus F\left(A\right)\right)\to \left(v\cap \left(x\setminus F\left(A\right)\right)=\varnothing \to F\left(A\right)\ne F\left(\mathrm{suc}A\right)\right)\right)$$
35	34	rexlimdv	$$⊢A\in \mathrm{\omega }\to \left(\exists v\in \left(x\setminus F\left(A\right)\right)v\cap \left(x\setminus F\left(A\right)\right)=\varnothing \to F\left(A\right)\ne F\left(\mathrm{suc}A\right)\right)$$
36	13 35	syl5	$$⊢A\in \mathrm{\omega }\to \left(x\setminus F\left(A\right)\ne \varnothing \to F\left(A\right)\ne F\left(\mathrm{suc}A\right)\right)$$
37	9 36	syldc	$$⊢\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)$$