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	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ≺ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		canth2g	⊢ ( 𝐴 ∈ 𝑇 → 𝐴 ≺ 𝒫 𝐴 )
2		simpl	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → 𝑇 ∈ Tarski )
3		tskpwss	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → 𝒫 𝐴 ⊆ 𝑇 )
4		ssdomg	⊢ ( 𝑇 ∈ Tarski → ( 𝒫 𝐴 ⊆ 𝑇 → 𝒫 𝐴 ≼ 𝑇 ) )
5	2 3 4	sylc	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → 𝒫 𝐴 ≼ 𝑇 )
6		sdomdomtr	⊢ ( ( 𝐴 ≺ 𝒫 𝐴 ∧ 𝒫 𝐴 ≼ 𝑇 ) → 𝐴 ≺ 𝑇 )
7	1 5 6	syl2an2	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ≺ 𝑇 )