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

Metamath Proof Explorer

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 ) )