Theorem tskwe2

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

	Ref	Expression
Assertion	tskwe2	|- ( T e. Tarski -> T e. dom card )

Proof

Step	Hyp	Ref	Expression
1		elpwi	|- ( y e. ~P T -> y C_ T )
2		tskssel	|- ( ( T e. Tarski /\ y C_ T /\ y ~< T ) -> y e. T )
3	2	3exp	|- ( T e. Tarski -> ( y C_ T -> ( y ~< T -> y e. T ) ) )
4	1 3	syl5	|- ( T e. Tarski -> ( y e. ~P T -> ( y ~< T -> y e. T ) ) )
5	4	ralrimiv	|- ( T e. Tarski -> A. y e. ~P T ( y ~< T -> y e. T ) )
6		rabss	|- ( { y e. ~P T | y ~< T } C_ T <-> A. y e. ~P T ( y ~< T -> y e. T ) )
7	5 6	sylibr	|- ( T e. Tarski -> { y e. ~P T | y ~< T } C_ T )
8		tskwe	|- ( ( T e. Tarski /\ { y e. ~P T | y ~< T } C_ T ) -> T e. dom card )
9	7 8	mpdan	|- ( T e. Tarski -> T e. dom card )