Theorem tsksdom

Description: An element of a Tarski class is strictly dominated by the class. JFM CLASSES2 th. 1. (Contributed by FL, 22-Feb-2011) (Revised by Mario Carneiro, 18-Jun-2013)

	Ref	Expression
Assertion	tsksdom	|- ( ( T e. Tarski /\ A e. T ) -> A ~< T )

Proof

Step	Hyp	Ref	Expression
1		canth2g	|- ( A e. T -> A ~< ~P A )
2		simpl	|- ( ( T e. Tarski /\ A e. T ) -> T e. Tarski )
3		tskpwss	|- ( ( T e. Tarski /\ A e. T ) -> ~P A C_ T )
4		ssdomg	|- ( T e. Tarski -> ( ~P A C_ T -> ~P A ~<_ T ) )
5	2 3 4	sylc	|- ( ( T e. Tarski /\ A e. T ) -> ~P A ~<_ T )
6		sdomdomtr	|- ( ( A ~< ~P A /\ ~P A ~<_ T ) -> A ~< T )
7	1 5 6	syl2an2	|- ( ( T e. Tarski /\ A e. T ) -> A ~< T )