Metamath Proof Explorer


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