Metamath Proof Explorer


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 )