Metamath Proof Explorer

Theorem nf1const

Description: A constant function from at least two elements is not one-to-one. (Contributed by AV, 30-Mar-2024)

Ref Expression
Assertion nf1const 
|- ( ( F : A --> { B } /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> -. F : A -1-1-> C )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( X e. A /\ Y e. A /\ X =/= Y ) -> X e. A )
2 simp2 
 |-  ( ( X e. A /\ Y e. A /\ X =/= Y ) -> Y e. A )
3 fvconst 
 |-  ( ( F : A --> { B } /\ X e. A ) -> ( F ` X ) = B )
4 1 3 sylan2 
 |-  ( ( F : A --> { B } /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> ( F ` X ) = B )
5 fvconst 
 |-  ( ( F : A --> { B } /\ Y e. A ) -> ( F ` Y ) = B )
6 2 5 sylan2 
 |-  ( ( F : A --> { B } /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> ( F ` Y ) = B )
7 4 6 eqtr4d 
 |-  ( ( F : A --> { B } /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> ( F ` X ) = ( F ` Y ) )
8 neneq 
 |-  ( X =/= Y -> -. X = Y )
9 8 3ad2ant3 
 |-  ( ( X e. A /\ Y e. A /\ X =/= Y ) -> -. X = Y )
10 9 adantl 
 |-  ( ( F : A --> { B } /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> -. X = Y )
11 7 10 jcnd 
 |-  ( ( F : A --> { B } /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> -. ( ( F ` X ) = ( F ` Y ) -> X = Y ) )
12 fveqeq2 
 |-  ( x = X -> ( ( F ` x ) = ( F ` y ) <-> ( F ` X ) = ( F ` y ) ) )
13 eqeq1 
 |-  ( x = X -> ( x = y <-> X = y ) )
14 12 13 imbi12d 
 |-  ( x = X -> ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( ( F ` X ) = ( F ` y ) -> X = y ) ) )
15 14 notbid 
 |-  ( x = X -> ( -. ( ( F ` x ) = ( F ` y ) -> x = y ) <-> -. ( ( F ` X ) = ( F ` y ) -> X = y ) ) )
16 fveq2 
 |-  ( y = Y -> ( F ` y ) = ( F ` Y ) )
17 16 eqeq2d 
 |-  ( y = Y -> ( ( F ` X ) = ( F ` y ) <-> ( F ` X ) = ( F ` Y ) ) )
18 eqeq2 
 |-  ( y = Y -> ( X = y <-> X = Y ) )
19 17 18 imbi12d 
 |-  ( y = Y -> ( ( ( F ` X ) = ( F ` y ) -> X = y ) <-> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) )
20 19 notbid 
 |-  ( y = Y -> ( -. ( ( F ` X ) = ( F ` y ) -> X = y ) <-> -. ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) )
21 15 20 rspc2ev 
 |-  ( ( X e. A /\ Y e. A /\ -. ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) -> E. x e. A E. y e. A -. ( ( F ` x ) = ( F ` y ) -> x = y ) )
22 1 2 11 21 syl2an23an 
 |-  ( ( F : A --> { B } /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> E. x e. A E. y e. A -. ( ( F ` x ) = ( F ` y ) -> x = y ) )
23 rexnal2 
 |-  ( E. x e. A E. y e. A -. ( ( F ` x ) = ( F ` y ) -> x = y ) <-> -. A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) )
24 22 23 sylib 
 |-  ( ( F : A --> { B } /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> -. A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) )
25 24 olcd 
 |-  ( ( F : A --> { B } /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> ( -. F : A --> C \/ -. A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
26 ianor 
 |-  ( -. ( F : A --> C /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) <-> ( -. F : A --> C \/ -. A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
27 dff13 
 |-  ( F : A -1-1-> C <-> ( F : A --> C /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
28 26 27 xchnxbir 
 |-  ( -. F : A -1-1-> C <-> ( -. F : A --> C \/ -. A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
29 25 28 sylibr 
 |-  ( ( F : A --> { B } /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> -. F : A -1-1-> C )