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

Metamath Proof Explorer

Theorem tsken

Description: Third axiom of a Tarski class. A subset of a Tarski class is either equipotent to the class or an element of the class. (Contributed by FL, 30-Dec-2010) (Revised by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion tsken 
|- ( ( T e. Tarski /\ A C_ T ) -> ( A ~~ T \/ A e. T ) )

Proof

Step Hyp Ref Expression
1 eltskg 
 |-  ( T e. Tarski -> ( T e. Tarski <-> ( A. x e. T ( ~P x C_ T /\ E. y e. T ~P x C_ y ) /\ A. x e. ~P T ( x ~~ T \/ x e. T ) ) ) )
2 1 ibi 
 |-  ( T e. Tarski -> ( A. x e. T ( ~P x C_ T /\ E. y e. T ~P x C_ y ) /\ A. x e. ~P T ( x ~~ T \/ x e. T ) ) )
3 2 simprd 
 |-  ( T e. Tarski -> A. x e. ~P T ( x ~~ T \/ x e. T ) )
4 elpw2g 
 |-  ( T e. Tarski -> ( A e. ~P T <-> A C_ T ) )
5 4 biimpar 
 |-  ( ( T e. Tarski /\ A C_ T ) -> A e. ~P T )
6 breq1 
 |-  ( x = A -> ( x ~~ T <-> A ~~ T ) )
7 eleq1 
 |-  ( x = A -> ( x e. T <-> A e. T ) )
8 6 7 orbi12d 
 |-  ( x = A -> ( ( x ~~ T \/ x e. T ) <-> ( A ~~ T \/ A e. T ) ) )
9 8 rspccva 
 |-  ( ( A. x e. ~P T ( x ~~ T \/ x e. T ) /\ A e. ~P T ) -> ( A ~~ T \/ A e. T ) )
10 3 5 9 syl2an2r 
 |-  ( ( T e. Tarski /\ A C_ T ) -> ( A ~~ T \/ A e. T ) )