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