tskwe2

Description: A Tarski class is well-orderable. (Contributed by Mario Carneiro, 20-Jun-2013)

		Ref	Expression
	Assertion	tskwe2	$⊢ T \in Tarski \to T \in dom card$

Step	Hyp	Ref	Expression
1		elpwi	$⊢ y \in 𝒫 T \to y \subseteq T$
2		tskssel	$⊢ (T \in Tarski \land y \subseteq T \land y ≺ T) \to y \in T$
3	2	3exp	$⊢ T \in Tarski \to (y \subseteq T \to (y ≺ T \to y \in T))$
4	1 3	syl5	$⊢ T \in Tarski \to (y \in 𝒫 T \to (y ≺ T \to y \in T))$
5	4	ralrimiv	$⊢ T \in Tarski \to \forall y \in 𝒫 T (y ≺ T \to y \in T)$
6		rabss	$⊢ \{y \in 𝒫 T \| y ≺ T\} \subseteq T \leftrightarrow \forall y \in 𝒫 T (y ≺ T \to y \in T)$
7	5 6	sylibr	$⊢ T \in Tarski \to \{y \in 𝒫 T \| y ≺ T\} \subseteq T$
8		tskwe	$⊢ (T \in Tarski \land \{y \in 𝒫 T \| y ≺ T\} \subseteq T) \to T \in dom card$
9	7 8	mpdan	$⊢ T \in Tarski \to T \in dom card$

Metamath Proof Explorer