This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )