Metamath Proof Explorer

Theorem eltsk2g

Description: Properties of a Tarski class. (Contributed by FL, 30-Dec-2010) (Revised by Mario Carneiro, 20-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 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 ) ) ) )
2 nfra1 
 |-  F/ z A. z e. T ~P z C_ T
3 pweq 
 |-  ( z = w -> ~P z = ~P w )
4 3 sseq1d 
 |-  ( z = w -> ( ~P z C_ T <-> ~P w C_ T ) )
5 4 rspccva 
 |-  ( ( A. z e. T ~P z C_ T /\ w e. T ) -> ~P w C_ T )
6 5 adantlr 
 |-  ( ( ( A. z e. T ~P z C_ T /\ z e. T ) /\ w e. T ) -> ~P w C_ T )
7 vpwex 
 |-  ~P z e. _V
8 7 elpw 
 |-  ( ~P z e. ~P w <-> ~P z C_ w )
9 ssel 
 |-  ( ~P w C_ T -> ( ~P z e. ~P w -> ~P z e. T ) )
10 8 9 syl5bir 
 |-  ( ~P w C_ T -> ( ~P z C_ w -> ~P z e. T ) )
11 6 10 syl 
 |-  ( ( ( A. z e. T ~P z C_ T /\ z e. T ) /\ w e. T ) -> ( ~P z C_ w -> ~P z e. T ) )
12 11 rexlimdva 
 |-  ( ( A. z e. T ~P z C_ T /\ z e. T ) -> ( E. w e. T ~P z C_ w -> ~P z e. T ) )
13 2 12 ralimdaa 
 |-  ( A. z e. T ~P z C_ T -> ( A. z e. T E. w e. T ~P z C_ w -> A. z e. T ~P z e. T ) )
14 13 imdistani 
 |-  ( ( A. z e. T ~P z C_ T /\ A. z e. T E. w e. T ~P z C_ w ) -> ( A. z e. T ~P z C_ T /\ A. z e. T ~P z e. T ) )
15 r19.26 
 |-  ( A. z e. T ( ~P z C_ T /\ E. w e. T ~P z C_ w ) <-> ( A. z e. T ~P z C_ T /\ A. z e. T E. w e. T ~P z C_ w ) )
16 r19.26 
 |-  ( A. z e. T ( ~P z C_ T /\ ~P z e. T ) <-> ( A. z e. T ~P z C_ T /\ A. z e. T ~P z e. T ) )
17 14 15 16 3imtr4i 
 |-  ( A. z e. T ( ~P z C_ T /\ E. w e. T ~P z C_ w ) -> A. z e. T ( ~P z C_ T /\ ~P z e. T ) )
18 ssid 
 |-  ~P z C_ ~P z
19 sseq2 
 |-  ( w = ~P z -> ( ~P z C_ w <-> ~P z C_ ~P z ) )
20 19 rspcev 
 |-  ( ( ~P z e. T /\ ~P z C_ ~P z ) -> E. w e. T ~P z C_ w )
21 18 20 mpan2 
 |-  ( ~P z e. T -> E. w e. T ~P z C_ w )
22 21 anim2i 
 |-  ( ( ~P z C_ T /\ ~P z e. T ) -> ( ~P z C_ T /\ E. w e. T ~P z C_ w ) )
23 22 ralimi 
 |-  ( A. z e. T ( ~P z C_ T /\ ~P z e. T ) -> A. z e. T ( ~P z C_ T /\ E. w e. T ~P z C_ w ) )
24 17 23 impbii 
 |-  ( A. z e. T ( ~P z C_ T /\ E. w e. T ~P z C_ w ) <-> A. z e. T ( ~P z C_ T /\ ~P z e. T ) )
25 24 anbi1i 
 |-  ( ( 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 ) ) <-> ( A. z e. T ( ~P z C_ T /\ ~P z e. T ) /\ A. z e. ~P T ( z ~~ T \/ z e. T ) ) )
26 1 25 bitrdi 
 |-  ( T e. V -> ( T e. Tarski <-> ( A. z e. T ( ~P z C_ T /\ ~P z e. T ) /\ A. z e. ~P T ( z ~~ T \/ z e. T ) ) ) )