Step |
Hyp |
Ref |
Expression |
1 |
|
f0 |
⊢ ∅ : ∅ ⟶ ∅ |
2 |
|
cnv0 |
⊢ ◡ ∅ = ∅ |
3 |
2
|
imaeq1i |
⊢ ( ◡ ∅ “ 𝑥 ) = ( ∅ “ 𝑥 ) |
4 |
|
0ima |
⊢ ( ∅ “ 𝑥 ) = ∅ |
5 |
3 4
|
eqtri |
⊢ ( ◡ ∅ “ 𝑥 ) = ∅ |
6 |
|
0ex |
⊢ ∅ ∈ V |
7 |
6
|
snid |
⊢ ∅ ∈ { ∅ } |
8 |
5 7
|
eqeltri |
⊢ ( ◡ ∅ “ 𝑥 ) ∈ { ∅ } |
9 |
8
|
rgenw |
⊢ ∀ 𝑥 ∈ { ∅ } ( ◡ ∅ “ 𝑥 ) ∈ { ∅ } |
10 |
|
sn0topon |
⊢ { ∅ } ∈ ( TopOn ‘ ∅ ) |
11 |
|
iscn |
⊢ ( ( { ∅ } ∈ ( TopOn ‘ ∅ ) ∧ { ∅ } ∈ ( TopOn ‘ ∅ ) ) → ( ∅ ∈ ( { ∅ } Cn { ∅ } ) ↔ ( ∅ : ∅ ⟶ ∅ ∧ ∀ 𝑥 ∈ { ∅ } ( ◡ ∅ “ 𝑥 ) ∈ { ∅ } ) ) ) |
12 |
10 10 11
|
mp2an |
⊢ ( ∅ ∈ ( { ∅ } Cn { ∅ } ) ↔ ( ∅ : ∅ ⟶ ∅ ∧ ∀ 𝑥 ∈ { ∅ } ( ◡ ∅ “ 𝑥 ) ∈ { ∅ } ) ) |
13 |
1 9 12
|
mpbir2an |
⊢ ∅ ∈ ( { ∅ } Cn { ∅ } ) |