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 Tarski A T A T

Proof

Step Hyp Ref Expression
1 canth2g A T A 𝒫 A
2 simpl T Tarski A T T Tarski
3 tskpwss T Tarski A T 𝒫 A T
4 ssdomg T Tarski 𝒫 A T 𝒫 A T
5 2 3 4 sylc T Tarski A T 𝒫 A T
6 sdomdomtr A 𝒫 A 𝒫 A T A T
7 1 5 6 syl2an2 T Tarski A T A T