Metamath Proof Explorer

Theorem tskmval

Description: Value of our tarski map. (Contributed by FL, 30-Dec-2010) (Revised by Mario Carneiro, 20-Sep-2014)

Ref Expression
Assertion tskmval 
|- ( A e. V -> ( tarskiMap ` A ) = |^| { x e. Tarski | A e. x } )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 grothtsk 
 |-  U. Tarski = _V
3 1 2 eleqtrrdi 
 |-  ( A e. V -> A e. U. Tarski )
4 eluni2 
 |-  ( A e. U. Tarski <-> E. x e. Tarski A e. x )
5 3 4 sylib 
 |-  ( A e. V -> E. x e. Tarski A e. x )
6 intexrab 
 |-  ( E. x e. Tarski A e. x <-> |^| { x e. Tarski | A e. x } e. _V )
7 5 6 sylib 
 |-  ( A e. V -> |^| { x e. Tarski | A e. x } e. _V )
8 eleq1 
 |-  ( y = A -> ( y e. x <-> A e. x ) )
9 8 rabbidv 
 |-  ( y = A -> { x e. Tarski | y e. x } = { x e. Tarski | A e. x } )
10 9 inteqd 
 |-  ( y = A -> |^| { x e. Tarski | y e. x } = |^| { x e. Tarski | A e. x } )
11 df-tskm 
 |-  tarskiMap = ( y e. _V |-> |^| { x e. Tarski | y e. x } )
12 10 11 fvmptg 
 |-  ( ( A e. _V /\ |^| { x e. Tarski | A e. x } e. _V ) -> ( tarskiMap ` A ) = |^| { x e. Tarski | A e. x } )
13 1 7 12 syl2anc 
 |-  ( A e. V -> ( tarskiMap ` A ) = |^| { x e. Tarski | A e. x } )