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	$$⊢\left(F:A⟶\left\{B\right\}\wedge \left(X\in A\wedge Y\in A\wedge X\ne Y\right)\right)\to \neg F:A\underset{1-1}{⟶}C$$

Proof

Step	Hyp	Ref	Expression
1		simp1	$$⊢\left(X\in A\wedge Y\in A\wedge X\ne Y\right)\to X\in A$$
2		simp2	$$⊢\left(X\in A\wedge Y\in A\wedge X\ne Y\right)\to Y\in A$$
3		fvconst	$$⊢\left(F:A⟶\left\{B\right\}\wedge X\in A\right)\to F\left(X\right)=B$$
4	1 3	sylan2	$$⊢\left(F:A⟶\left\{B\right\}\wedge \left(X\in A\wedge Y\in A\wedge X\ne Y\right)\right)\to F\left(X\right)=B$$
5		fvconst	$$⊢\left(F:A⟶\left\{B\right\}\wedge Y\in A\right)\to F\left(Y\right)=B$$
6	2 5	sylan2	$$⊢\left(F:A⟶\left\{B\right\}\wedge \left(X\in A\wedge Y\in A\wedge X\ne Y\right)\right)\to F\left(Y\right)=B$$
7	4 6	eqtr4d	$$⊢\left(F:A⟶\left\{B\right\}\wedge \left(X\in A\wedge Y\in A\wedge X\ne Y\right)\right)\to F\left(X\right)=F\left(Y\right)$$
8		neneq	$$⊢X\ne Y\to \neg X=Y$$
9	8	3ad2ant3	$$⊢\left(X\in A\wedge Y\in A\wedge X\ne Y\right)\to \neg X=Y$$
10	9	adantl	$$⊢\left(F:A⟶\left\{B\right\}\wedge \left(X\in A\wedge Y\in A\wedge X\ne Y\right)\right)\to \neg X=Y$$
11	7 10	jcnd	$$⊢\left(F:A⟶\left\{B\right\}\wedge \left(X\in A\wedge Y\in A\wedge X\ne Y\right)\right)\to \neg \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)$$
12		fveqeq2	$$⊢x=X\to \left(F\left(x\right)=F\left(y\right)\leftrightarrow F\left(X\right)=F\left(y\right)\right)$$
13		eqeq1	$$⊢x=X\to \left(x=y\leftrightarrow X=y\right)$$
14	12 13	imbi12d	$$⊢x=X\to \left(\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \left(F\left(X\right)=F\left(y\right)\to X=y\right)\right)$$
15	14	notbid	$$⊢x=X\to \left(\neg \left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \neg \left(F\left(X\right)=F\left(y\right)\to X=y\right)\right)$$
16		fveq2	$$⊢y=Y\to F\left(y\right)=F\left(Y\right)$$
17	16	eqeq2d	$$⊢y=Y\to \left(F\left(X\right)=F\left(y\right)\leftrightarrow F\left(X\right)=F\left(Y\right)\right)$$
18		eqeq2	$$⊢y=Y\to \left(X=y\leftrightarrow X=Y\right)$$
19	17 18	imbi12d	$$⊢y=Y\to \left(\left(F\left(X\right)=F\left(y\right)\to X=y\right)\leftrightarrow \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)$$
20	19	notbid	$$⊢y=Y\to \left(\neg \left(F\left(X\right)=F\left(y\right)\to X=y\right)\leftrightarrow \neg \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)$$
21	15 20	rspc2ev	$$⊢\left(X\in A\wedge Y\in A\wedge \neg \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\to \exists x\in A\exists y\in A\neg \left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
22	1 2 11 21	syl2an23an	$$⊢\left(F:A⟶\left\{B\right\}\wedge \left(X\in A\wedge Y\in A\wedge X\ne Y\right)\right)\to \exists x\in A\exists y\in A\neg \left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
23		rexnal2	$$⊢\exists x\in A\exists y\in A\neg \left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \neg \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
24	22 23	sylib	$$⊢\left(F:A⟶\left\{B\right\}\wedge \left(X\in A\wedge Y\in A\wedge X\ne Y\right)\right)\to \neg \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)$$
25	24	olcd	$$⊢\left(F:A⟶\left\{B\right\}\wedge \left(X\in A\wedge Y\in A\wedge X\ne Y\right)\right)\to \left(\neg F:A⟶C\vee \neg \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
26		ianor	$$⊢\neg \left(F:A⟶C\wedge \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)\leftrightarrow \left(\neg F:A⟶C\vee \neg \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
27		dff13	$$⊢F:A\underset{1-1}{⟶}C\leftrightarrow \left(F:A⟶C\wedge \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
28	26 27	xchnxbir	$$⊢\neg F:A\underset{1-1}{⟶}C\leftrightarrow \left(\neg F:A⟶C\vee \neg \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
29	25 28	sylibr	$$⊢\left(F:A⟶\left\{B\right\}\wedge \left(X\in A\wedge Y\in A\wedge X\ne Y\right)\right)\to \neg F:A\underset{1-1}{⟶}C$$