Metamath Proof Explorer

Theorem tskmcl

Description: A Tarski class that contains A is a Tarski class. (Contributed by FL, 17-Apr-2011) (Proof shortened by Mario Carneiro, 21-Sep-2014)

Ref Expression
Assertion tskmcl ⊢ tarskiMap ⁡ A ∈ Tarski

Proof

Step Hyp Ref Expression
1 tskmval ⊢ A ∈ V → tarskiMap ⁡ A = ⋂ x ∈ Tarski | A ∈ x
2 ssrab2 ⊢ x ∈ Tarski | A ∈ x ⊆ Tarski
3 id ⊢ A ∈ V → A ∈ V
4 grothtsk ⊢ ⋃ Tarski = V
5 3 4 eleqtrrdi ⊢ A ∈ V → A ∈ ⋃ Tarski
6 eluni2 ⊢ A ∈ ⋃ Tarski ↔ ∃ x ∈ Tarski A ∈ x
7 5 6 sylib ⊢ A ∈ V → ∃ x ∈ Tarski A ∈ x
8 rabn0 ⊢ x ∈ Tarski | A ∈ x ≠ ∅ ↔ ∃ x ∈ Tarski A ∈ x
9 7 8 sylibr ⊢ A ∈ V → x ∈ Tarski | A ∈ x ≠ ∅
10 inttsk ⊢ x ∈ Tarski | A ∈ x ⊆ Tarski ∧ x ∈ Tarski | A ∈ x ≠ ∅ → ⋂ x ∈ Tarski | A ∈ x ∈ Tarski
11 2 9 10 sylancr ⊢ A ∈ V → ⋂ x ∈ Tarski | A ∈ x ∈ Tarski
12 1 11 eqeltrd ⊢ A ∈ V → tarskiMap ⁡ A ∈ Tarski
13 fvprc ⊢ ¬ A ∈ V → tarskiMap ⁡ A = ∅
14 0tsk ⊢ ∅ ∈ Tarski
15 13 14 eqeltrdi ⊢ ¬ A ∈ V → tarskiMap ⁡ A ∈ Tarski
16 12 15 pm2.61i ⊢ tarskiMap ⁡ A ∈ Tarski