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