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	⊢ ( 𝐴 ∈ 𝑉 → ( tarskiMap ‘ 𝐴 ) = ∩ { 𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2		grothtsk	⊢ ∪ Tarski = V
3	1 2	eleqtrrdi	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ ∪ Tarski )
4		eluni2	⊢ ( 𝐴 ∈ ∪ Tarski ↔ ∃ 𝑥 ∈ Tarski 𝐴 ∈ 𝑥 )
5	3 4	sylib	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ∈ Tarski 𝐴 ∈ 𝑥 )
6		intexrab	⊢ ( ∃ 𝑥 ∈ Tarski 𝐴 ∈ 𝑥 ↔ ∩ { 𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥 } ∈ V )
7	5 6	sylib	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥 } ∈ V )
8		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 ) )
9	8	rabbidv	⊢ ( 𝑦 = 𝐴 → { 𝑥 ∈ Tarski ∣ 𝑦 ∈ 𝑥 } = { 𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥 } )
10	9	inteqd	⊢ ( 𝑦 = 𝐴 → ∩ { 𝑥 ∈ Tarski ∣ 𝑦 ∈ 𝑥 } = ∩ { 𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥 } )
11		df-tskm	⊢ tarskiMap = ( 𝑦 ∈ V ↦ ∩ { 𝑥 ∈ Tarski ∣ 𝑦 ∈ 𝑥 } )
12	10 11	fvmptg	⊢ ( ( 𝐴 ∈ V ∧ ∩ { 𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥 } ∈ V ) → ( tarskiMap ‘ 𝐴 ) = ∩ { 𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥 } )
13	1 7 12	syl2anc	⊢ ( 𝐴 ∈ 𝑉 → ( tarskiMap ‘ 𝐴 ) = ∩ { 𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥 } )