Theorem untangtr

Description: A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011)

	Ref	Expression
Assertion	untangtr	$$⊢\mathrm{Tr}A\to \left(\forall x\in A\neg x\in x\leftrightarrow \forall x\in A\forall y\in x\neg y\in y\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-tr	$$⊢\mathrm{Tr}A\leftrightarrow \bigcup A\subseteq A$$
2		ssralv	$$⊢\bigcup A\subseteq A\to \left(\forall x\in A\neg x\in x\to \forall x\in \bigcup A\neg x\in x\right)$$
3	1 2	sylbi	$$⊢\mathrm{Tr}A\to \left(\forall x\in A\neg x\in x\to \forall x\in \bigcup A\neg x\in x\right)$$
4		elequ1	$$⊢x=y\to \left(x\in x\leftrightarrow y\in x\right)$$
5		elequ2	$$⊢x=y\to \left(y\in x\leftrightarrow y\in y\right)$$
6	4 5	bitrd	$$⊢x=y\to \left(x\in x\leftrightarrow y\in y\right)$$
7	6	notbid	$$⊢x=y\to \left(\neg x\in x\leftrightarrow \neg y\in y\right)$$
8	7	cbvralvw	$$⊢\forall x\in \bigcup A\neg x\in x\leftrightarrow \forall y\in \bigcup A\neg y\in y$$
9		untuni	$$⊢\forall y\in \bigcup A\neg y\in y\leftrightarrow \forall x\in A\forall y\in x\neg y\in y$$
10	8 9	bitri	$$⊢\forall x\in \bigcup A\neg x\in x\leftrightarrow \forall x\in A\forall y\in x\neg y\in y$$
11	3 10	imbitrdi	$$⊢\mathrm{Tr}A\to \left(\forall x\in A\neg x\in x\to \forall x\in A\forall y\in x\neg y\in y\right)$$
12		untelirr	$$⊢\forall y\in x\neg y\in y\to \neg x\in x$$
13	12	ralimi	$$⊢\forall x\in A\forall y\in x\neg y\in y\to \forall x\in A\neg x\in x$$
14	11 13	impbid1	$$⊢\mathrm{Tr}A\to \left(\forall x\in A\neg x\in x\leftrightarrow \forall x\in A\forall y\in x\neg y\in y\right)$$