Theorem tskwe2

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

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

Proof

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