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\in V\to \mathrm{tarskiMap}\left(A\right)=\bigcap \left\{x\in \mathrm{Tarski}|A\in x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in V\to A\in \mathrm{V}$$
2		grothtsk	$$⊢\bigcup \mathrm{Tarski}=\mathrm{V}$$
3	1 2	eleqtrrdi	$$⊢A\in V\to A\in \bigcup \mathrm{Tarski}$$
4		eluni2	$$⊢A\in \bigcup \mathrm{Tarski}\leftrightarrow \exists x\in \mathrm{Tarski}A\in x$$
5	3 4	sylib	$$⊢A\in V\to \exists x\in \mathrm{Tarski}A\in x$$
6		intexrab	$$⊢\exists x\in \mathrm{Tarski}A\in x\leftrightarrow \bigcap \left\{x\in \mathrm{Tarski}|A\in x\right\}\in \mathrm{V}$$
7	5 6	sylib	$$⊢A\in V\to \bigcap \left\{x\in \mathrm{Tarski}|A\in x\right\}\in \mathrm{V}$$
8		eleq1	$$⊢y=A\to \left(y\in x\leftrightarrow A\in x\right)$$
9	8	rabbidv	$$⊢y=A\to \left\{x\in \mathrm{Tarski}|y\in x\right\}=\left\{x\in \mathrm{Tarski}|A\in x\right\}$$
10	9	inteqd	$$⊢y=A\to \bigcap \left\{x\in \mathrm{Tarski}|y\in x\right\}=\bigcap \left\{x\in \mathrm{Tarski}|A\in x\right\}$$
11		df-tskm	$$⊢\mathrm{tarskiMap}=\left(y\in \mathrm{V}⟼\bigcap \left\{x\in \mathrm{Tarski}|y\in x\right\}\right)$$
12	10 11	fvmptg	$$⊢\left(A\in \mathrm{V}\wedge \bigcap \left\{x\in \mathrm{Tarski}|A\in x\right\}\in \mathrm{V}\right)\to \mathrm{tarskiMap}\left(A\right)=\bigcap \left\{x\in \mathrm{Tarski}|A\in x\right\}$$
13	1 7 12	syl2anc	$$⊢A\in V\to \mathrm{tarskiMap}\left(A\right)=\bigcap \left\{x\in \mathrm{Tarski}|A\in x\right\}$$