Theorem map0cor

Description: A function exists iff an empty codomain is accompanied with an empty domain. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypotheses	map0cor.1	|- ( ph -> A e. V )
	map0cor.2	|- ( ph -> B e. W )
Assertion	map0cor	|- ( ph -> ( ( B = (/) -> A = (/) ) <-> E. f f : A --> B ) )

Proof

Step	Hyp	Ref	Expression
1		map0cor.1	|- ( ph -> A e. V )
2		map0cor.2	|- ( ph -> B e. W )
3		biid	|- ( A =/= (/) <-> A =/= (/) )
4	3	necon2bbii	|- ( A = (/) <-> -. A =/= (/) )
5	4	imbi2i	|- ( ( B = (/) -> A = (/) ) <-> ( B = (/) -> -. A =/= (/) ) )
6		imnan	|- ( ( B = (/) -> -. A =/= (/) ) <-> -. ( B = (/) /\ A =/= (/) ) )
7	5 6	bitri	|- ( ( B = (/) -> A = (/) ) <-> -. ( B = (/) /\ A =/= (/) ) )
8		map0g	|- ( ( B e. W /\ A e. V ) -> ( ( B ^m A ) = (/) <-> ( B = (/) /\ A =/= (/) ) ) )
9	8	notbid	|- ( ( B e. W /\ A e. V ) -> ( -. ( B ^m A ) = (/) <-> -. ( B = (/) /\ A =/= (/) ) ) )
10	7 9	bitr4id	|- ( ( B e. W /\ A e. V ) -> ( ( B = (/) -> A = (/) ) <-> -. ( B ^m A ) = (/) ) )
11		neq0	|- ( -. ( B ^m A ) = (/) <-> E. f f e. ( B ^m A ) )
12	11	a1i	|- ( ( B e. W /\ A e. V ) -> ( -. ( B ^m A ) = (/) <-> E. f f e. ( B ^m A ) ) )
13		elmapg	|- ( ( B e. W /\ A e. V ) -> ( f e. ( B ^m A ) <-> f : A --> B ) )
14	13	exbidv	|- ( ( B e. W /\ A e. V ) -> ( E. f f e. ( B ^m A ) <-> E. f f : A --> B ) )
15	10 12 14	3bitrd	|- ( ( B e. W /\ A e. V ) -> ( ( B = (/) -> A = (/) ) <-> E. f f : A --> B ) )
16	2 1 15	syl2anc	|- ( ph -> ( ( B = (/) -> A = (/) ) <-> E. f f : A --> B ) )