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 ) |
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 ) |