Metamath Proof Explorer

Theorem 0tsk

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

Ref Expression
Assertion 0tsk ⊢ ∅ ∈ Tarski

Proof

Step Hyp Ref Expression
1 ral0 ⊢ ∀ x ∈ ∅ 𝒫 x ⊆ ∅ ∧ 𝒫 x ∈ ∅
2 elsni ⊢ x ∈ ∅ → x = ∅
3 0ex ⊢ ∅ ∈ V
4 3 enref ⊢ ∅ ≈ ∅
5 breq1 ⊢ x = ∅ → x ≈ ∅ ↔ ∅ ≈ ∅
6 4 5 mpbiri ⊢ x = ∅ → x ≈ ∅
7 6 orcd ⊢ x = ∅ → x ≈ ∅ ∨ x ∈ ∅
8 2 7 syl ⊢ x ∈ ∅ → x ≈ ∅ ∨ x ∈ ∅
9 pw0 ⊢ 𝒫 ∅ = ∅
10 8 9 eleq2s ⊢ x ∈ 𝒫 ∅ → x ≈ ∅ ∨ x ∈ ∅
11 10 rgen ⊢ ∀ x ∈ 𝒫 ∅ x ≈ ∅ ∨ x ∈ ∅
12 eltsk2g ⊢ ∅ ∈ V → ∅ ∈ Tarski ↔ ∀ x ∈ ∅ 𝒫 x ⊆ ∅ ∧ 𝒫 x ∈ ∅ ∧ ∀ x ∈ 𝒫 ∅ x ≈ ∅ ∨ x ∈ ∅
13 3 12 ax-mp ⊢ ∅ ∈ Tarski ↔ ∀ x ∈ ∅ 𝒫 x ⊆ ∅ ∧ 𝒫 x ∈ ∅ ∧ ∀ x ∈ 𝒫 ∅ x ≈ ∅ ∨ x ∈ ∅
14 1 11 13 mpbir2an ⊢ ∅ ∈ Tarski