Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Continuous Functions
0cnf
Next ⟩
fsumcncf
Metamath Proof Explorer
Ascii
Unicode
Theorem
0cnf
Description:
The empty set is a continuous function.
(Contributed by
Glauco Siliprandi
, 11-Dec-2019)
Ref
Expression
Assertion
0cnf
⊢
∅
∈
∅
Cn
∅
Proof
Step
Hyp
Ref
Expression
1
f0
⊢
∅
:
∅
⟶
∅
2
cnv0
⊢
∅
-1
=
∅
3
2
imaeq1i
⊢
∅
-1
x
=
∅
x
4
0ima
⊢
∅
x
=
∅
5
3
4
eqtri
⊢
∅
-1
x
=
∅
6
0ex
⊢
∅
∈
V
7
6
snid
⊢
∅
∈
∅
8
5
7
eqeltri
⊢
∅
-1
x
∈
∅
9
8
rgenw
⊢
∀
x
∈
∅
∅
-1
x
∈
∅
10
sn0topon
⊢
∅
∈
TopOn
⁡
∅
11
iscn
⊢
∅
∈
TopOn
⁡
∅
∧
∅
∈
TopOn
⁡
∅
→
∅
∈
∅
Cn
∅
↔
∅
:
∅
⟶
∅
∧
∀
x
∈
∅
∅
-1
x
∈
∅
12
10
10
11
mp2an
⊢
∅
∈
∅
Cn
∅
↔
∅
:
∅
⟶
∅
∧
∀
x
∈
∅
∅
-1
x
∈
∅
13
1
9
12
mpbir2an
⊢
∅
∈
∅
Cn
∅