Metamath Proof Explorer

Theorem tskmcl

Description: A Tarski class that contains A is a Tarski class. (Contributed by FL, 17-Apr-2011) (Proof shortened by Mario Carneiro, 21-Sep-2014)

Ref Expression
Assertion tskmcl 
|- ( tarskiMap ` A ) e. Tarski

Proof

Step Hyp Ref Expression
1 tskmval 
 |-  ( A e. _V -> ( tarskiMap ` A ) = |^| { x e. Tarski | A e. x } )
2 ssrab2 
 |-  { x e. Tarski | A e. x } C_ Tarski
3 id 
 |-  ( A e. _V -> A e. _V )
4 grothtsk 
 |-  U. Tarski = _V
5 3 4 eleqtrrdi 
 |-  ( A e. _V -> A e. U. Tarski )
6 eluni2 
 |-  ( A e. U. Tarski <-> E. x e. Tarski A e. x )
7 5 6 sylib 
 |-  ( A e. _V -> E. x e. Tarski A e. x )
8 rabn0 
 |-  ( { x e. Tarski | A e. x } =/= (/) <-> E. x e. Tarski A e. x )
9 7 8 sylibr 
 |-  ( A e. _V -> { x e. Tarski | A e. x } =/= (/) )
10 inttsk 
 |-  ( ( { x e. Tarski | A e. x } C_ Tarski /\ { x e. Tarski | A e. x } =/= (/) ) -> |^| { x e. Tarski | A e. x } e. Tarski )
11 2 9 10 sylancr 
 |-  ( A e. _V -> |^| { x e. Tarski | A e. x } e. Tarski )
12 1 11 eqeltrd 
 |-  ( A e. _V -> ( tarskiMap ` A ) e. Tarski )
13 fvprc 
 |-  ( -. A e. _V -> ( tarskiMap ` A ) = (/) )
14 0tsk 
 |-  (/) e. Tarski
15 13 14 eqeltrdi 
 |-  ( -. A e. _V -> ( tarskiMap ` A ) e. Tarski )
16 12 15 pm2.61i 
 |-  ( tarskiMap ` A ) e. Tarski