Theorem 0cnf

Description: The empty set is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	0cnf	|- (/) e. ( { (/) } Cn { (/) } )

Proof

Step	Hyp	Ref	Expression
1		f0	|- (/) : (/) --> (/)
2		cnv0	|- `' (/) = (/)
3	2	imaeq1i	|- ( `' (/) " x ) = ( (/) " x )
4		0ima	|- ( (/) " x ) = (/)
5	3 4	eqtri	|- ( `' (/) " x ) = (/)
6		0ex	|- (/) e. _V
7	6	snid	|- (/) e. { (/) }
8	5 7	eqeltri	|- ( `' (/) " x ) e. { (/) }
9	8	rgenw	|- A. x e. { (/) } ( `' (/) " x ) e. { (/) }
10		sn0topon	|- { (/) } e. ( TopOn ` (/) )
11		iscn	|- ( ( { (/) } e. ( TopOn ` (/) ) /\ { (/) } e. ( TopOn ` (/) ) ) -> ( (/) e. ( { (/) } Cn { (/) } ) <-> ( (/) : (/) --> (/) /\ A. x e. { (/) } ( `' (/) " x ) e. { (/) } ) ) )
12	10 10 11	mp2an	|- ( (/) e. ( { (/) } Cn { (/) } ) <-> ( (/) : (/) --> (/) /\ A. x e. { (/) } ( `' (/) " x ) e. { (/) } ) )
13	1 9 12	mpbir2an	|- (/) e. ( { (/) } Cn { (/) } )