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 |