Metamath Proof Explorer

Theorem nf1oconst

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

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

Proof

Step Hyp Ref Expression
1 nf1const 
 |-  ( ( F : A --> { B } /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> -. F : A -1-1-> C )
2 1 orcd 
 |-  ( ( F : A --> { B } /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> ( -. F : A -1-1-> C \/ -. F : A -onto-> C ) )
3 ianor 
 |-  ( -. ( F : A -1-1-> C /\ F : A -onto-> C ) <-> ( -. F : A -1-1-> C \/ -. F : A -onto-> C ) )
4 df-f1o 
 |-  ( F : A -1-1-onto-> C <-> ( F : A -1-1-> C /\ F : A -onto-> C ) )
5 3 4 xchnxbir 
 |-  ( -. F : A -1-1-onto-> C <-> ( -. F : A -1-1-> C \/ -. F : A -onto-> C ) )
6 2 5 sylibr 
 |-  ( ( F : A --> { B } /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> -. F : A -1-1-onto-> C )