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	$$⊢\left(T\in \mathrm{Tarski}\wedge A\in T\right)\to A\prec T$$

Proof

Step	Hyp	Ref	Expression
1		canth2g	$$⊢A\in T\to A\prec 𝒫A$$
2		simpl	$$⊢\left(T\in \mathrm{Tarski}\wedge A\in T\right)\to T\in \mathrm{Tarski}$$
3		tskpwss	$$⊢\left(T\in \mathrm{Tarski}\wedge A\in T\right)\to 𝒫A\subseteq T$$
4		ssdomg	$$⊢T\in \mathrm{Tarski}\to \left(𝒫A\subseteq T\to 𝒫A\preccurlyeq T\right)$$
5	2 3 4	sylc	$$⊢\left(T\in \mathrm{Tarski}\wedge A\in T\right)\to 𝒫A\preccurlyeq T$$
6		sdomdomtr	$$⊢\left(A\prec 𝒫A\wedge 𝒫A\preccurlyeq T\right)\to A\prec T$$
7	1 5 6	syl2an2	$$⊢\left(T\in \mathrm{Tarski}\wedge A\in T\right)\to A\prec T$$