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 )