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

Metamath Proof Explorer

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