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 tarskiMapATarski

Proof

Step Hyp Ref Expression
1 tskmval AVtarskiMapA=xTarski|Ax
2 ssrab2 xTarski|AxTarski
3 id AVAV
4 grothtsk Tarski=V
5 3 4 eleqtrrdi AVATarski
6 eluni2 ATarskixTarskiAx
7 5 6 sylib AVxTarskiAx
8 rabn0 xTarski|AxxTarskiAx
9 7 8 sylibr AVxTarski|Ax
10 inttsk xTarski|AxTarskixTarski|AxxTarski|AxTarski
11 2 9 10 sylancr AVxTarski|AxTarski
12 1 11 eqeltrd AVtarskiMapATarski
13 fvprc ¬AVtarskiMapA=
14 0tsk Tarski
15 13 14 eqeltrdi ¬AVtarskiMapATarski
16 12 15 pm2.61i tarskiMapATarski