Theorem f12dfv

Description: A one-to-one function with a domain with at least two different elements in terms of function values. (Contributed by Alexander van der Vekens, 2-Mar-2018)

	Ref	Expression
Hypothesis	f12dfv.a	$$⊢A=\left\{X,Y\right\}$$
Assertion	f12dfv	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to \left(F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge F\left(X\right)\ne F\left(Y\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		f12dfv.a	$$⊢A=\left\{X,Y\right\}$$
2		dff14b	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall x\in A\forall y\in \left(A\setminus \left\{x\right\}\right)F\left(x\right)\ne F\left(y\right)\right)$$
3	1	raleqi	$$⊢\forall x\in A\forall y\in \left(A\setminus \left\{x\right\}\right)F\left(x\right)\ne F\left(y\right)\leftrightarrow \forall x\in \left\{X,Y\right\}\forall y\in \left(A\setminus \left\{x\right\}\right)F\left(x\right)\ne F\left(y\right)$$
4		sneq	$$⊢x=X\to \left\{x\right\}=\left\{X\right\}$$
5	4	difeq2d	$$⊢x=X\to A\setminus \left\{x\right\}=A\setminus \left\{X\right\}$$
6		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
7	6	neeq1d	$$⊢x=X\to \left(F\left(x\right)\ne F\left(y\right)\leftrightarrow F\left(X\right)\ne F\left(y\right)\right)$$
8	5 7	raleqbidv	$$⊢x=X\to \left(\forall y\in \left(A\setminus \left\{x\right\}\right)F\left(x\right)\ne F\left(y\right)\leftrightarrow \forall y\in \left(A\setminus \left\{X\right\}\right)F\left(X\right)\ne F\left(y\right)\right)$$
9		sneq	$$⊢x=Y\to \left\{x\right\}=\left\{Y\right\}$$
10	9	difeq2d	$$⊢x=Y\to A\setminus \left\{x\right\}=A\setminus \left\{Y\right\}$$
11		fveq2	$$⊢x=Y\to F\left(x\right)=F\left(Y\right)$$
12	11	neeq1d	$$⊢x=Y\to \left(F\left(x\right)\ne F\left(y\right)\leftrightarrow F\left(Y\right)\ne F\left(y\right)\right)$$
13	10 12	raleqbidv	$$⊢x=Y\to \left(\forall y\in \left(A\setminus \left\{x\right\}\right)F\left(x\right)\ne F\left(y\right)\leftrightarrow \forall y\in \left(A\setminus \left\{Y\right\}\right)F\left(Y\right)\ne F\left(y\right)\right)$$
14	8 13	ralprg	$$⊢\left(X\in U\wedge Y\in V\right)\to \left(\forall x\in \left\{X,Y\right\}\forall y\in \left(A\setminus \left\{x\right\}\right)F\left(x\right)\ne F\left(y\right)\leftrightarrow \left(\forall y\in \left(A\setminus \left\{X\right\}\right)F\left(X\right)\ne F\left(y\right)\wedge \forall y\in \left(A\setminus \left\{Y\right\}\right)F\left(Y\right)\ne F\left(y\right)\right)\right)$$
15	14	adantr	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to \left(\forall x\in \left\{X,Y\right\}\forall y\in \left(A\setminus \left\{x\right\}\right)F\left(x\right)\ne F\left(y\right)\leftrightarrow \left(\forall y\in \left(A\setminus \left\{X\right\}\right)F\left(X\right)\ne F\left(y\right)\wedge \forall y\in \left(A\setminus \left\{Y\right\}\right)F\left(Y\right)\ne F\left(y\right)\right)\right)$$
16	1	difeq1i	$$⊢A\setminus \left\{X\right\}=\left\{X,Y\right\}\setminus \left\{X\right\}$$
17		difprsn1	$$⊢X\ne Y\to \left\{X,Y\right\}\setminus \left\{X\right\}=\left\{Y\right\}$$
18	16 17	syl5eq	$$⊢X\ne Y\to A\setminus \left\{X\right\}=\left\{Y\right\}$$
19	18	adantl	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to A\setminus \left\{X\right\}=\left\{Y\right\}$$
20	19	raleqdv	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to \left(\forall y\in \left(A\setminus \left\{X\right\}\right)F\left(X\right)\ne F\left(y\right)\leftrightarrow \forall y\in \left\{Y\right\}F\left(X\right)\ne F\left(y\right)\right)$$
21		fveq2	$$⊢y=Y\to F\left(y\right)=F\left(Y\right)$$
22	21	neeq2d	$$⊢y=Y\to \left(F\left(X\right)\ne F\left(y\right)\leftrightarrow F\left(X\right)\ne F\left(Y\right)\right)$$
23	22	ralsng	$$⊢Y\in V\to \left(\forall y\in \left\{Y\right\}F\left(X\right)\ne F\left(y\right)\leftrightarrow F\left(X\right)\ne F\left(Y\right)\right)$$
24	23	adantl	$$⊢\left(X\in U\wedge Y\in V\right)\to \left(\forall y\in \left\{Y\right\}F\left(X\right)\ne F\left(y\right)\leftrightarrow F\left(X\right)\ne F\left(Y\right)\right)$$
25	24	adantr	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to \left(\forall y\in \left\{Y\right\}F\left(X\right)\ne F\left(y\right)\leftrightarrow F\left(X\right)\ne F\left(Y\right)\right)$$
26	20 25	bitrd	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to \left(\forall y\in \left(A\setminus \left\{X\right\}\right)F\left(X\right)\ne F\left(y\right)\leftrightarrow F\left(X\right)\ne F\left(Y\right)\right)$$
27	1	difeq1i	$$⊢A\setminus \left\{Y\right\}=\left\{X,Y\right\}\setminus \left\{Y\right\}$$
28		difprsn2	$$⊢X\ne Y\to \left\{X,Y\right\}\setminus \left\{Y\right\}=\left\{X\right\}$$
29	27 28	syl5eq	$$⊢X\ne Y\to A\setminus \left\{Y\right\}=\left\{X\right\}$$
30	29	adantl	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to A\setminus \left\{Y\right\}=\left\{X\right\}$$
31	30	raleqdv	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to \left(\forall y\in \left(A\setminus \left\{Y\right\}\right)F\left(Y\right)\ne F\left(y\right)\leftrightarrow \forall y\in \left\{X\right\}F\left(Y\right)\ne F\left(y\right)\right)$$
32		fveq2	$$⊢y=X\to F\left(y\right)=F\left(X\right)$$
33	32	neeq2d	$$⊢y=X\to \left(F\left(Y\right)\ne F\left(y\right)\leftrightarrow F\left(Y\right)\ne F\left(X\right)\right)$$
34	33	ralsng	$$⊢X\in U\to \left(\forall y\in \left\{X\right\}F\left(Y\right)\ne F\left(y\right)\leftrightarrow F\left(Y\right)\ne F\left(X\right)\right)$$
35	34	adantr	$$⊢\left(X\in U\wedge Y\in V\right)\to \left(\forall y\in \left\{X\right\}F\left(Y\right)\ne F\left(y\right)\leftrightarrow F\left(Y\right)\ne F\left(X\right)\right)$$
36	35	adantr	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to \left(\forall y\in \left\{X\right\}F\left(Y\right)\ne F\left(y\right)\leftrightarrow F\left(Y\right)\ne F\left(X\right)\right)$$
37	31 36	bitrd	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to \left(\forall y\in \left(A\setminus \left\{Y\right\}\right)F\left(Y\right)\ne F\left(y\right)\leftrightarrow F\left(Y\right)\ne F\left(X\right)\right)$$
38	26 37	anbi12d	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to \left(\left(\forall y\in \left(A\setminus \left\{X\right\}\right)F\left(X\right)\ne F\left(y\right)\wedge \forall y\in \left(A\setminus \left\{Y\right\}\right)F\left(Y\right)\ne F\left(y\right)\right)\leftrightarrow \left(F\left(X\right)\ne F\left(Y\right)\wedge F\left(Y\right)\ne F\left(X\right)\right)\right)$$
39		necom	$$⊢F\left(X\right)\ne F\left(Y\right)\leftrightarrow F\left(Y\right)\ne F\left(X\right)$$
40	39	biimpi	$$⊢F\left(X\right)\ne F\left(Y\right)\to F\left(Y\right)\ne F\left(X\right)$$
41	40	pm4.71i	$$⊢F\left(X\right)\ne F\left(Y\right)\leftrightarrow \left(F\left(X\right)\ne F\left(Y\right)\wedge F\left(Y\right)\ne F\left(X\right)\right)$$
42	38 41	bitr4di	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to \left(\left(\forall y\in \left(A\setminus \left\{X\right\}\right)F\left(X\right)\ne F\left(y\right)\wedge \forall y\in \left(A\setminus \left\{Y\right\}\right)F\left(Y\right)\ne F\left(y\right)\right)\leftrightarrow F\left(X\right)\ne F\left(Y\right)\right)$$
43	15 42	bitrd	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to \left(\forall x\in \left\{X,Y\right\}\forall y\in \left(A\setminus \left\{x\right\}\right)F\left(x\right)\ne F\left(y\right)\leftrightarrow F\left(X\right)\ne F\left(Y\right)\right)$$
44	3 43	syl5bb	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to \left(\forall x\in A\forall y\in \left(A\setminus \left\{x\right\}\right)F\left(x\right)\ne F\left(y\right)\leftrightarrow F\left(X\right)\ne F\left(Y\right)\right)$$
45	44	anbi2d	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to \left(\left(F:A⟶B\wedge \forall x\in A\forall y\in \left(A\setminus \left\{x\right\}\right)F\left(x\right)\ne F\left(y\right)\right)\leftrightarrow \left(F:A⟶B\wedge F\left(X\right)\ne F\left(Y\right)\right)\right)$$
46	2 45	syl5bb	$$⊢\left(\left(X\in U\wedge Y\in V\right)\wedge X\ne Y\right)\to \left(F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge F\left(X\right)\ne F\left(Y\right)\right)\right)$$