Theorem setindtr

Description: Set induction for sets contained in a transitive set. If we are allowed to assume Infinity, then all sets have a transitive closure and this reduces to setind ; however, this version is useful without Infinity. (Contributed by Stefan O'Rear, 28-Oct-2014)

	Ref	Expression
Assertion	setindtr	$$⊢\forall x\left(x\subseteq A\to x\in A\right)\to \left(\exists y\left(\mathrm{Tr}y\wedge B\in y\right)\to B\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎx\mathrm{Tr}y$$
2		nfa1	$$⊢Ⅎx\forall x\left(x\subseteq A\to x\in A\right)$$
3	1 2	nfan	$$⊢Ⅎx\left(\mathrm{Tr}y\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)$$
4		eldifn	$$⊢x\in \left(y\setminus A\right)\to \neg x\in A$$
5	4	adantl	$$⊢\left(\left(\mathrm{Tr}y\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\wedge x\in \left(y\setminus A\right)\right)\to \neg x\in A$$
6		trss	$$⊢\mathrm{Tr}y\to \left(x\in y\to x\subseteq y\right)$$
7		eldifi	$$⊢x\in \left(y\setminus A\right)\to x\in y$$
8	6 7	impel	$$⊢\left(\mathrm{Tr}y\wedge x\in \left(y\setminus A\right)\right)\to x\subseteq y$$
9		df-ss	$$⊢x\subseteq y\leftrightarrow x\cap y=x$$
10	8 9	sylib	$$⊢\left(\mathrm{Tr}y\wedge x\in \left(y\setminus A\right)\right)\to x\cap y=x$$
11	10	adantlr	$$⊢\left(\left(\mathrm{Tr}y\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\wedge x\in \left(y\setminus A\right)\right)\to x\cap y=x$$
12	11	sseq1d	$$⊢\left(\left(\mathrm{Tr}y\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\wedge x\in \left(y\setminus A\right)\right)\to \left(x\cap y\subseteq A\leftrightarrow x\subseteq A\right)$$
13		sp	$$⊢\forall x\left(x\subseteq A\to x\in A\right)\to \left(x\subseteq A\to x\in A\right)$$
14	13	ad2antlr	$$⊢\left(\left(\mathrm{Tr}y\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\wedge x\in \left(y\setminus A\right)\right)\to \left(x\subseteq A\to x\in A\right)$$
15	12 14	sylbid	$$⊢\left(\left(\mathrm{Tr}y\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\wedge x\in \left(y\setminus A\right)\right)\to \left(x\cap y\subseteq A\to x\in A\right)$$
16	5 15	mtod	$$⊢\left(\left(\mathrm{Tr}y\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\wedge x\in \left(y\setminus A\right)\right)\to \neg x\cap y\subseteq A$$
17		inssdif0	$$⊢x\cap y\subseteq A\leftrightarrow x\cap \left(y\setminus A\right)=\varnothing$$
18	16 17	sylnib	$$⊢\left(\left(\mathrm{Tr}y\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\wedge x\in \left(y\setminus A\right)\right)\to \neg x\cap \left(y\setminus A\right)=\varnothing$$
19	18	ex	$$⊢\left(\mathrm{Tr}y\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\to \left(x\in \left(y\setminus A\right)\to \neg x\cap \left(y\setminus A\right)=\varnothing \right)$$
20	3 19	ralrimi	$$⊢\left(\mathrm{Tr}y\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\to \forall x\in \left(y\setminus A\right)\neg x\cap \left(y\setminus A\right)=\varnothing$$
21		ralnex	$$⊢\forall x\in \left(y\setminus A\right)\neg x\cap \left(y\setminus A\right)=\varnothing \leftrightarrow \neg \exists x\in \left(y\setminus A\right)x\cap \left(y\setminus A\right)=\varnothing$$
22	20 21	sylib	$$⊢\left(\mathrm{Tr}y\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\to \neg \exists x\in \left(y\setminus A\right)x\cap \left(y\setminus A\right)=\varnothing$$
23		vex	$$⊢y\in \mathrm{V}$$
24	23	difexi	$$⊢y\setminus A\in \mathrm{V}$$
25		zfreg	$$⊢\left(y\setminus A\in \mathrm{V}\wedge y\setminus A\ne \varnothing \right)\to \exists x\in \left(y\setminus A\right)x\cap \left(y\setminus A\right)=\varnothing$$
26	24 25	mpan	$$⊢y\setminus A\ne \varnothing \to \exists x\in \left(y\setminus A\right)x\cap \left(y\setminus A\right)=\varnothing$$
27	26	necon1bi	$$⊢\neg \exists x\in \left(y\setminus A\right)x\cap \left(y\setminus A\right)=\varnothing \to y\setminus A=\varnothing$$
28	22 27	syl	$$⊢\left(\mathrm{Tr}y\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\to y\setminus A=\varnothing$$
29		ssdif0	$$⊢y\subseteq A\leftrightarrow y\setminus A=\varnothing$$
30	28 29	sylibr	$$⊢\left(\mathrm{Tr}y\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\to y\subseteq A$$
31	30	adantlr	$$⊢\left(\left(\mathrm{Tr}y\wedge B\in y\right)\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\to y\subseteq A$$
32		simplr	$$⊢\left(\left(\mathrm{Tr}y\wedge B\in y\right)\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\to B\in y$$
33	31 32	sseldd	$$⊢\left(\left(\mathrm{Tr}y\wedge B\in y\right)\wedge \forall x\left(x\subseteq A\to x\in A\right)\right)\to B\in A$$
34	33	ex	$$⊢\left(\mathrm{Tr}y\wedge B\in y\right)\to \left(\forall x\left(x\subseteq A\to x\in A\right)\to B\in A\right)$$
35	34	exlimiv	$$⊢\exists y\left(\mathrm{Tr}y\wedge B\in y\right)\to \left(\forall x\left(x\subseteq A\to x\in A\right)\to B\in A\right)$$
36	35	com12	$$⊢\forall x\left(x\subseteq A\to x\in A\right)\to \left(\exists y\left(\mathrm{Tr}y\wedge B\in y\right)\to B\in A\right)$$