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

Proof

Step	Hyp	Ref	Expression
1		sdomnen	$⊢ A ≺ T \to \neg A \approx T$
2	1	3ad2ant3	$⊢ (T \in Tarski \land A \subseteq T \land A ≺ T) \to \neg A \approx T$
3		tsken	$⊢ (T \in Tarski \land A \subseteq T) \to (A \approx T \lor A \in T)$
4	3	3adant3	$⊢ (T \in Tarski \land A \subseteq T \land A ≺ T) \to (A \approx T \lor A \in T)$
5	4	ord	$⊢ (T \in Tarski \land A \subseteq T \land A ≺ T) \to (\neg A \approx T \to A \in T)$
6	2 5	mpd	$⊢ (T \in Tarski \land A \subseteq T \land A ≺ T) \to A \in T$

Metamath Proof Explorer

Theorem tskssel

Proof