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 \in Tarski \land A \in T) \to A ≺ T$

Proof

Step	Hyp	Ref	Expression
1		canth2g	$⊢ A \in T \to A ≺ 𝒫 A$
2		simpl	$⊢ (T \in Tarski \land A \in T) \to T \in Tarski$
3		tskpwss	$⊢ (T \in Tarski \land A \in T) \to 𝒫 A \subseteq T$
4		ssdomg	$⊢ T \in Tarski \to (𝒫 A \subseteq T \to 𝒫 A ≼ T)$
5	2 3 4	sylc	$⊢ (T \in Tarski \land A \in T) \to 𝒫 A ≼ T$
6		sdomdomtr	$⊢ (A ≺ 𝒫 A \land 𝒫 A ≼ T) \to A ≺ T$
7	1 5 6	syl2an2	$⊢ (T \in Tarski \land A \in T) \to A ≺ T$

Metamath Proof Explorer

Theorem tsksdom

Proof