Metamath Proof Explorer

Theorem 0tsk

Description: The empty set is a (transitive) Tarski class. (Contributed by FL, 30-Dec-2010)

Ref Expression
Assertion 0tsk 
|- (/) e. Tarski

Proof

Step Hyp Ref Expression
1 ral0 
 |-  A. x e. (/) ( ~P x C_ (/) /\ ~P x e. (/) )
2 elsni 
 |-  ( x e. { (/) } -> x = (/) )
3 0ex 
 |-  (/) e. _V
4 3 enref 
 |-  (/) ~~ (/)
5 breq1 
 |-  ( x = (/) -> ( x ~~ (/) <-> (/) ~~ (/) ) )
6 4 5 mpbiri 
 |-  ( x = (/) -> x ~~ (/) )
7 6 orcd 
 |-  ( x = (/) -> ( x ~~ (/) \/ x e. (/) ) )
8 2 7 syl 
 |-  ( x e. { (/) } -> ( x ~~ (/) \/ x e. (/) ) )
9 pw0 
 |-  ~P (/) = { (/) }
10 8 9 eleq2s 
 |-  ( x e. ~P (/) -> ( x ~~ (/) \/ x e. (/) ) )
11 10 rgen 
 |-  A. x e. ~P (/) ( x ~~ (/) \/ x e. (/) )
12 eltsk2g 
 |-  ( (/) e. _V -> ( (/) e. Tarski <-> ( A. x e. (/) ( ~P x C_ (/) /\ ~P x e. (/) ) /\ A. x e. ~P (/) ( x ~~ (/) \/ x e. (/) ) ) ) )
13 3 12 ax-mp 
 |-  ( (/) e. Tarski <-> ( A. x e. (/) ( ~P x C_ (/) /\ ~P x e. (/) ) /\ A. x e. ~P (/) ( x ~~ (/) \/ x e. (/) ) ) )
14 1 11 13 mpbir2an 
 |-  (/) e. Tarski