Theorem untsucf

Description: If a class is untangled, then so is its successor. (Contributed by Scott Fenton, 28-Feb-2011) (Revised by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypothesis	untsucf.1	$$⊢\underset{\_}{Ⅎ}yA$$
Assertion	untsucf	$$⊢\forall x\in A\neg x\in x\to \forall y\in \mathrm{suc}A\neg y\in y$$

Proof

Step	Hyp	Ref	Expression
1		untsucf.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		nfv	$$⊢Ⅎy\neg x\in x$$
3	1 2	nfralw	$$⊢Ⅎy\forall x\in A\neg x\in x$$
4		vex	$$⊢y\in \mathrm{V}$$
5	4	elsuc	$$⊢y\in \mathrm{suc}A\leftrightarrow \left(y\in A\vee y=A\right)$$
6		elequ1	$$⊢x=y\to \left(x\in x\leftrightarrow y\in x\right)$$
7		elequ2	$$⊢x=y\to \left(y\in x\leftrightarrow y\in y\right)$$
8	6 7	bitrd	$$⊢x=y\to \left(x\in x\leftrightarrow y\in y\right)$$
9	8	notbid	$$⊢x=y\to \left(\neg x\in x\leftrightarrow \neg y\in y\right)$$
10	9	rspccv	$$⊢\forall x\in A\neg x\in x\to \left(y\in A\to \neg y\in y\right)$$
11		untelirr	$$⊢\forall x\in A\neg x\in x\to \neg A\in A$$
12		eleq1	$$⊢y=A\to \left(y\in y\leftrightarrow A\in y\right)$$
13		eleq2	$$⊢y=A\to \left(A\in y\leftrightarrow A\in A\right)$$
14	12 13	bitrd	$$⊢y=A\to \left(y\in y\leftrightarrow A\in A\right)$$
15	14	notbid	$$⊢y=A\to \left(\neg y\in y\leftrightarrow \neg A\in A\right)$$
16	11 15	syl5ibrcom	$$⊢\forall x\in A\neg x\in x\to \left(y=A\to \neg y\in y\right)$$
17	10 16	jaod	$$⊢\forall x\in A\neg x\in x\to \left(\left(y\in A\vee y=A\right)\to \neg y\in y\right)$$
18	5 17	biimtrid	$$⊢\forall x\in A\neg x\in x\to \left(y\in \mathrm{suc}A\to \neg y\in y\right)$$
19	3 18	ralrimi	$$⊢\forall x\in A\neg x\in x\to \forall y\in \mathrm{suc}A\neg y\in y$$