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