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