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	|- ( E. x e. A A. y e. x -. y e. y -> A. y e. |^| A -. y e. y )

Proof

Step	Hyp	Ref	Expression
1		intss1	|- ( x e. A -> |^| A C_ x )
2		ssralv	|- ( |^| A C_ x -> ( A. y e. x -. y e. y -> A. y e. |^| A -. y e. y ) )
3	1 2	syl	|- ( x e. A -> ( A. y e. x -. y e. y -> A. y e. |^| A -. y e. y ) )
4	3	rexlimiv	|- ( E. x e. A A. y e. x -. y e. y -> A. y e. |^| A -. y e. y )