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