Theorem tskssel

Description: A part of a Tarski class strictly dominated by the class is an element of the class. JFM CLASSES2 th. 2. (Contributed by FL, 22-Feb-2011) (Proof shortened by Mario Carneiro, 20-Sep-2014)

	Ref	Expression
Assertion	tskssel	$$⊢\left(T\in \mathrm{Tarski}\wedge A\subseteq T\wedge A\prec T\right)\to A\in T$$

Proof

Step	Hyp	Ref	Expression
1		sdomnen	$$⊢A\prec T\to \neg A\approx T$$
2	1	3ad2ant3	$$⊢\left(T\in \mathrm{Tarski}\wedge A\subseteq T\wedge A\prec T\right)\to \neg A\approx T$$
3		tsken	$$⊢\left(T\in \mathrm{Tarski}\wedge A\subseteq T\right)\to \left(A\approx T\vee A\in T\right)$$
4	3	3adant3	$$⊢\left(T\in \mathrm{Tarski}\wedge A\subseteq T\wedge A\prec T\right)\to \left(A\approx T\vee A\in T\right)$$
5	4	ord	$$⊢\left(T\in \mathrm{Tarski}\wedge A\subseteq T\wedge A\prec T\right)\to \left(\neg A\approx T\to A\in T\right)$$
6	2 5	mpd	$$⊢\left(T\in \mathrm{Tarski}\wedge A\subseteq T\wedge A\prec T\right)\to A\in T$$