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 ∅