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

Metamath Proof Explorer

Theorem f1mo

Description: A function that maps a set with at most one element to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Assertion f1mo 
|- ( ( E* x x e. A /\ F : A --> B ) -> F : A -1-1-> B )

Proof

Step Hyp Ref Expression
1 mo0sn 
 |-  ( E* x x e. A <-> ( A = (/) \/ E. y A = { y } ) )
2 f102g 
 |-  ( ( A = (/) /\ F : A --> B ) -> F : A -1-1-> B )
3 vex 
 |-  y e. _V
4 f1sn2g 
 |-  ( ( y e. _V /\ F : { y } --> B ) -> F : { y } -1-1-> B )
5 3 4 mpan 
 |-  ( F : { y } --> B -> F : { y } -1-1-> B )
6 feq2 
 |-  ( A = { y } -> ( F : A --> B <-> F : { y } --> B ) )
7 f1eq2 
 |-  ( A = { y } -> ( F : A -1-1-> B <-> F : { y } -1-1-> B ) )
8 6 7 imbi12d 
 |-  ( A = { y } -> ( ( F : A --> B -> F : A -1-1-> B ) <-> ( F : { y } --> B -> F : { y } -1-1-> B ) ) )
9 5 8 mpbiri 
 |-  ( A = { y } -> ( F : A --> B -> F : A -1-1-> B ) )
10 9 exlimiv 
 |-  ( E. y A = { y } -> ( F : A --> B -> F : A -1-1-> B ) )
11 10 imp 
 |-  ( ( E. y A = { y } /\ F : A --> B ) -> F : A -1-1-> B )
12 2 11 jaoian 
 |-  ( ( ( A = (/) \/ E. y A = { y } ) /\ F : A --> B ) -> F : A -1-1-> B )
13 1 12 sylanb 
 |-  ( ( E* x x e. A /\ F : A --> B ) -> F : A -1-1-> B )