This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )