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