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

Metamath Proof Explorer

Theorem eltskg

Description: Properties of a Tarski class. (Contributed by FL, 30-Dec-2010)

Ref Expression
Assertion eltskg 
|- ( T e. V -> ( T e. Tarski <-> ( A. z e. T ( ~P z C_ T /\ E. w e. T ~P z C_ w ) /\ A. z e. ~P T ( z ~~ T \/ z e. T ) ) ) )

Proof

Step Hyp Ref Expression
1 sseq2 
 |-  ( y = T -> ( ~P z C_ y <-> ~P z C_ T ) )
2 rexeq 
 |-  ( y = T -> ( E. w e. y ~P z C_ w <-> E. w e. T ~P z C_ w ) )
3 1 2 anbi12d 
 |-  ( y = T -> ( ( ~P z C_ y /\ E. w e. y ~P z C_ w ) <-> ( ~P z C_ T /\ E. w e. T ~P z C_ w ) ) )
4 3 raleqbi1dv 
 |-  ( y = T -> ( A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) <-> A. z e. T ( ~P z C_ T /\ E. w e. T ~P z C_ w ) ) )
5 pweq 
 |-  ( y = T -> ~P y = ~P T )
6 breq2 
 |-  ( y = T -> ( z ~~ y <-> z ~~ T ) )
7 eleq2 
 |-  ( y = T -> ( z e. y <-> z e. T ) )
8 6 7 orbi12d 
 |-  ( y = T -> ( ( z ~~ y \/ z e. y ) <-> ( z ~~ T \/ z e. T ) ) )
9 5 8 raleqbidv 
 |-  ( y = T -> ( A. z e. ~P y ( z ~~ y \/ z e. y ) <-> A. z e. ~P T ( z ~~ T \/ z e. T ) ) )
10 4 9 anbi12d 
 |-  ( y = T -> ( ( A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) /\ A. z e. ~P y ( z ~~ y \/ z e. y ) ) <-> ( A. z e. T ( ~P z C_ T /\ E. w e. T ~P z C_ w ) /\ A. z e. ~P T ( z ~~ T \/ z e. T ) ) ) )
11 df-tsk 
 |-  Tarski = { y | ( A. z e. y ( ~P z C_ y /\ E. w e. y ~P z C_ w ) /\ A. z e. ~P y ( z ~~ y \/ z e. y ) ) }
12 10 11 elab2g 
 |-  ( T e. V -> ( T e. Tarski <-> ( A. z e. T ( ~P z C_ T /\ E. w e. T ~P z C_ w ) /\ A. z e. ~P T ( z ~~ T \/ z e. T ) ) ) )