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\} \land (X \in A \land Y \in A \land X \neq Y)) \to \neg F : A \underset{1-1 onto}{⟶} C$

Step	Hyp	Ref	Expression
1		nf1const	$⊢ (F : A ⟶ \{B\} \land (X \in A \land Y \in A \land X \neq Y)) \to \neg F : A \underset{1-1}{⟶} C$
2	1	orcd	$⊢ (F : A ⟶ \{B\} \land (X \in A \land Y \in A \land X \neq Y)) \to (\neg F : A \underset{1-1}{⟶} C \lor \neg F : A \underset{onto}{⟶} C)$
3		ianor	$⊢ \neg (F : A \underset{1-1}{⟶} C \land F : A \underset{onto}{⟶} C) \leftrightarrow (\neg F : A \underset{1-1}{⟶} C \lor \neg F : A \underset{onto}{⟶} C)$
4		df-f1o	$⊢ F : A \underset{1-1 onto}{⟶} C \leftrightarrow (F : A \underset{1-1}{⟶} C \land F : A \underset{onto}{⟶} C)$
5	3 4	xchnxbir	$⊢ \neg F : A \underset{1-1 onto}{⟶} C \leftrightarrow (\neg F : A \underset{1-1}{⟶} C \lor \neg F : A \underset{onto}{⟶} C)$
6	2 5	sylibr	$⊢ (F : A ⟶ \{B\} \land (X \in A \land Y \in A \land X \neq Y)) \to \neg F : A \underset{1-1 onto}{⟶} C$

Metamath Proof Explorer