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

Metamath Proof Explorer

Theorem f102g

Description: A function that maps the empty set to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Assertion f102g 
|- ( ( A = (/) /\ F : A --> B ) -> F : A -1-1-> B )

Proof

Step Hyp Ref Expression
1 feq2 
 |-  ( A = (/) -> ( F : A --> B <-> F : (/) --> B ) )
2 1 biimpa 
 |-  ( ( A = (/) /\ F : A --> B ) -> F : (/) --> B )
3 f0bi 
 |-  ( F : (/) --> B <-> F = (/) )
4 f10 
 |-  (/) : (/) -1-1-> B
5 f1eq1 
 |-  ( F = (/) -> ( F : (/) -1-1-> B <-> (/) : (/) -1-1-> B ) )
6 4 5 mpbiri 
 |-  ( F = (/) -> F : (/) -1-1-> B )
7 3 6 sylbi 
 |-  ( F : (/) --> B -> F : (/) -1-1-> B )
8 2 7 syl 
 |-  ( ( A = (/) /\ F : A --> B ) -> F : (/) -1-1-> B )
9 f1eq2 
 |-  ( A = (/) -> ( F : A -1-1-> B <-> F : (/) -1-1-> B ) )
10 9 adantr 
 |-  ( ( A = (/) /\ F : A --> B ) -> ( F : A -1-1-> B <-> F : (/) -1-1-> B ) )
11 8 10 mpbird 
 |-  ( ( A = (/) /\ F : A --> B ) -> F : A -1-1-> B )