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 ⊢∅-1x=∅x
4 0ima ⊢∅x=∅
5 3 4 eqtri ⊢∅-1x=∅
6 0ex ⊢∅∈V
7 6 snid ⊢∅∈∅
8 5 7 eqeltri ⊢∅-1x∈∅
9 8 rgenw ⊢∀x∈∅∅-1x∈∅
10 sn0topon ⊢∅∈TopOn⁡∅
11 iscn ⊢∅∈TopOn⁡∅∧∅∈TopOn⁡∅→∅∈∅Cn∅↔∅:∅⟶∅∧∀x∈∅∅-1x∈∅
12 10 10 11 mp2an ⊢∅∈∅Cn∅↔∅:∅⟶∅∧∀x∈∅∅-1x∈∅
13 1 9 12 mpbir2an ⊢∅∈∅Cn∅