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