Theorem setind

Description: Set (epsilon) induction. Theorem 5.22 of TakeutiZaring p. 21. (Contributed by NM, 17-Sep-2003)

	Ref	Expression
Assertion	setind	$$⊢\forall x\left(x\subseteq A\to x\in A\right)\to A=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ssindif0	$$⊢y\subseteq A\leftrightarrow y\cap \left(\mathrm{V}\setminus A\right)=\varnothing$$
2		sseq1	$$⊢x=y\to \left(x\subseteq A\leftrightarrow y\subseteq A\right)$$
3		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
4	2 3	imbi12d	$$⊢x=y\to \left(\left(x\subseteq A\to x\in A\right)\leftrightarrow \left(y\subseteq A\to y\in A\right)\right)$$
5	4	spvv	$$⊢\forall x\left(x\subseteq A\to x\in A\right)\to \left(y\subseteq A\to y\in A\right)$$
6	1 5	syl5bir	$$⊢\forall x\left(x\subseteq A\to x\in A\right)\to \left(y\cap \left(\mathrm{V}\setminus A\right)=\varnothing \to y\in A\right)$$
7		eldifn	$$⊢y\in \left(\mathrm{V}\setminus A\right)\to \neg y\in A$$
8	6 7	nsyli	$$⊢\forall x\left(x\subseteq A\to x\in A\right)\to \left(y\in \left(\mathrm{V}\setminus A\right)\to \neg y\cap \left(\mathrm{V}\setminus A\right)=\varnothing \right)$$
9	8	imp	$$⊢\left(\forall x\left(x\subseteq A\to x\in A\right)\wedge y\in \left(\mathrm{V}\setminus A\right)\right)\to \neg y\cap \left(\mathrm{V}\setminus A\right)=\varnothing$$
10	9	nrexdv	$$⊢\forall x\left(x\subseteq A\to x\in A\right)\to \neg \exists y\in \left(\mathrm{V}\setminus A\right)y\cap \left(\mathrm{V}\setminus A\right)=\varnothing$$
11		zfregs	$$⊢\mathrm{V}\setminus A\ne \varnothing \to \exists y\in \left(\mathrm{V}\setminus A\right)y\cap \left(\mathrm{V}\setminus A\right)=\varnothing$$
12	11	necon1bi	$$⊢\neg \exists y\in \left(\mathrm{V}\setminus A\right)y\cap \left(\mathrm{V}\setminus A\right)=\varnothing \to \mathrm{V}\setminus A=\varnothing$$
13	10 12	syl	$$⊢\forall x\left(x\subseteq A\to x\in A\right)\to \mathrm{V}\setminus A=\varnothing$$
14		vdif0	$$⊢A=\mathrm{V}\leftrightarrow \mathrm{V}\setminus A=\varnothing$$
15	13 14	sylibr	$$⊢\forall x\left(x\subseteq A\to x\in A\right)\to A=\mathrm{V}$$