This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ◡ ∅ = ∅
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 { ∅ } )