Theorem tskint

Description: The intersection of an element of a transitive Tarski class is an element of the class. (Contributed by FL, 17-Apr-2011) (Revised by Mario Carneiro, 20-Sep-2014)

	Ref	Expression
Assertion	tskint	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ A =/= (/) ) -> |^| A e. T )

Proof

Step	Hyp	Ref	Expression
1		simp1l	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ A =/= (/) ) -> T e. Tarski )
2		tskuni	|- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> U. A e. T )
3	2	3expa	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T ) -> U. A e. T )
4	3	3adant3	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ A =/= (/) ) -> U. A e. T )
5		intssuni	|- ( A =/= (/) -> |^| A C_ U. A )
6	5	3ad2ant3	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ A =/= (/) ) -> |^| A C_ U. A )
7		tskss	|- ( ( T e. Tarski /\ U. A e. T /\ |^| A C_ U. A ) -> |^| A e. T )
8	1 4 6 7	syl3anc	|- ( ( ( T e. Tarski /\ Tr T ) /\ A e. T /\ A =/= (/) ) -> |^| A e. T )