This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∀ 𝑥 ∈ ∅ ( 𝒫 𝑥 ⊆ ∅ ∧ 𝒫 𝑥 ∈ ∅ )
2 elsni ⊢ ( 𝑥 ∈ { ∅ } → 𝑥 = ∅ )
3 0ex ⊢ ∅ ∈ V
4 3 enref ⊢ ∅ ≈ ∅
5 breq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ≈ ∅ ↔ ∅ ≈ ∅ ) )
6 4 5 mpbiri ⊢ ( 𝑥 = ∅ → 𝑥 ≈ ∅ )
7 6 orcd ⊢ ( 𝑥 = ∅ → ( 𝑥 ≈ ∅ ∨ 𝑥 ∈ ∅ ) )
8 2 7 syl ⊢ ( 𝑥 ∈ { ∅ } → ( 𝑥 ≈ ∅ ∨ 𝑥 ∈ ∅ ) )
9 pw0 ⊢ 𝒫 ∅ = { ∅ }
10 8 9 eleq2s ⊢ ( 𝑥 ∈ 𝒫 ∅ → ( 𝑥 ≈ ∅ ∨ 𝑥 ∈ ∅ ) )
11 10 rgen ⊢ ∀ 𝑥 ∈ 𝒫 ∅ ( 𝑥 ≈ ∅ ∨ 𝑥 ∈ ∅ )
12 eltsk2g ⊢ ( ∅ ∈ V → ( ∅ ∈ Tarski ↔ ( ∀ 𝑥 ∈ ∅ ( 𝒫 𝑥 ⊆ ∅ ∧ 𝒫 𝑥 ∈ ∅ ) ∧ ∀ 𝑥 ∈ 𝒫 ∅ ( 𝑥 ≈ ∅ ∨ 𝑥 ∈ ∅ ) ) ) )
13 3 12 ax-mp ⊢ ( ∅ ∈ Tarski ↔ ( ∀ 𝑥 ∈ ∅ ( 𝒫 𝑥 ⊆ ∅ ∧ 𝒫 𝑥 ∈ ∅ ) ∧ ∀ 𝑥 ∈ 𝒫 ∅ ( 𝑥 ≈ ∅ ∨ 𝑥 ∈ ∅ ) ) )
14 1 11 13 mpbir2an ⊢ ∅ ∈ Tarski