Theorem f1cdmsn

Description: If a one-to-one function with a nonempty domain has a singleton as its codomain, its domain must also be a singleton. (Contributed by BTernaryTau, 1-Dec-2024)

	Ref	Expression
Assertion	f1cdmsn	|- ( ( F : A -1-1-> { B } /\ A =/= (/) ) -> E. x A = { x } )

Proof

Step	Hyp	Ref	Expression
1		f1f	|- ( F : A -1-1-> { B } -> F : A --> { B } )
2		fvconst	|- ( ( F : A --> { B } /\ y e. A ) -> ( F ` y ) = B )
3	2	3adant3	|- ( ( F : A --> { B } /\ y e. A /\ z e. A ) -> ( F ` y ) = B )
4		fvconst	|- ( ( F : A --> { B } /\ z e. A ) -> ( F ` z ) = B )
5	4	3adant2	|- ( ( F : A --> { B } /\ y e. A /\ z e. A ) -> ( F ` z ) = B )
6	3 5	eqtr4d	|- ( ( F : A --> { B } /\ y e. A /\ z e. A ) -> ( F ` y ) = ( F ` z ) )
7	1 6	syl3an1	|- ( ( F : A -1-1-> { B } /\ y e. A /\ z e. A ) -> ( F ` y ) = ( F ` z ) )
8		f1veqaeq	|- ( ( F : A -1-1-> { B } /\ ( y e. A /\ z e. A ) ) -> ( ( F ` y ) = ( F ` z ) -> y = z ) )
9	8	3impb	|- ( ( F : A -1-1-> { B } /\ y e. A /\ z e. A ) -> ( ( F ` y ) = ( F ` z ) -> y = z ) )
10	7 9	mpd	|- ( ( F : A -1-1-> { B } /\ y e. A /\ z e. A ) -> y = z )
11	10	3expia	|- ( ( F : A -1-1-> { B } /\ y e. A ) -> ( z e. A -> y = z ) )
12	11	ralrimiv	|- ( ( F : A -1-1-> { B } /\ y e. A ) -> A. z e. A y = z )
13	12	reximdva0	|- ( ( F : A -1-1-> { B } /\ A =/= (/) ) -> E. y e. A A. z e. A y = z )
14		issn	|- ( E. y e. A A. z e. A y = z -> E. x A = { x } )
15	13 14	syl	|- ( ( F : A -1-1-> { B } /\ A =/= (/) ) -> E. x A = { x } )