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 V tarskiMap A = x Tarski | A x

Proof

Step Hyp Ref Expression
1 elex A V A V
2 grothtsk Tarski = V
3 1 2 eleqtrrdi A V A Tarski
4 eluni2 A Tarski x Tarski A x
5 3 4 sylib A V x Tarski A x
6 intexrab x Tarski A x x Tarski | A x V
7 5 6 sylib A V x Tarski | A x V
8 eleq1 y = A y x A x
9 8 rabbidv y = A x Tarski | y x = x Tarski | A x
10 9 inteqd y = A x Tarski | y x = x Tarski | A x
11 df-tskm tarskiMap = y V x Tarski | y x
12 10 11 fvmptg A V x Tarski | A x V tarskiMap A = x Tarski | A x
13 1 7 12 syl2anc A V tarskiMap A = x Tarski | A x