Theorem untint

Description: If there is an untangled element of a class, then the intersection of the class is untangled. (Contributed by Scott Fenton, 1-Mar-2011)

	Ref	Expression
Assertion	untint	$$⊢\exists x\in A\forall y\in x\neg y\in y\to \forall y\in \bigcap A\neg y\in y$$

Proof

Step	Hyp	Ref	Expression
1		intss1	$$⊢x\in A\to \bigcap A\subseteq x$$
2		ssralv	$$⊢\bigcap A\subseteq x\to \left(\forall y\in x\neg y\in y\to \forall y\in \bigcap A\neg y\in y\right)$$
3	1 2	syl	$$⊢x\in A\to \left(\forall y\in x\neg y\in y\to \forall y\in \bigcap A\neg y\in y\right)$$
4	3	rexlimiv	$$⊢\exists x\in A\forall y\in x\neg y\in y\to \forall y\in \bigcap A\neg y\in y$$