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 ‘ 𝐴 ) ∈ Tarski

Proof

Step Hyp Ref Expression
1 tskmval ( 𝐴 ∈ V → ( tarskiMap ‘ 𝐴 ) = { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } )
2 ssrab2 { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } ⊆ Tarski
3 id ( 𝐴 ∈ V → 𝐴 ∈ V )
4 grothtsk Tarski = V
5 3 4 eleqtrrdi ( 𝐴 ∈ V → 𝐴 Tarski )
6 eluni2 ( 𝐴 Tarski ↔ ∃ 𝑥 ∈ Tarski 𝐴𝑥 )
7 5 6 sylib ( 𝐴 ∈ V → ∃ 𝑥 ∈ Tarski 𝐴𝑥 )
8 rabn0 ( { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } ≠ ∅ ↔ ∃ 𝑥 ∈ Tarski 𝐴𝑥 )
9 7 8 sylibr ( 𝐴 ∈ V → { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } ≠ ∅ )
10 inttsk ( ( { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } ⊆ Tarski ∧ { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } ≠ ∅ ) → { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } ∈ Tarski )
11 2 9 10 sylancr ( 𝐴 ∈ V → { 𝑥 ∈ Tarski ∣ 𝐴𝑥 } ∈ Tarski )
12 1 11 eqeltrd ( 𝐴 ∈ V → ( tarskiMap ‘ 𝐴 ) ∈ Tarski )
13 fvprc ( ¬ 𝐴 ∈ V → ( tarskiMap ‘ 𝐴 ) = ∅ )
14 0tsk ∅ ∈ Tarski
15 13 14 eqeltrdi ( ¬ 𝐴 ∈ V → ( tarskiMap ‘ 𝐴 ) ∈ Tarski )
16 12 15 pm2.61i ( tarskiMap ‘ 𝐴 ) ∈ Tarski