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 ) ) ) )