Theorem f1dom3el3dif

Description: The range of a 1-1 function from a set with three different elements has (at least) three different elements. (Contributed by AV, 20-Mar-2019)

	Ref	Expression
Hypotheses	f1dom3fv3dif.v	$$⊢\phi \to \left(A\in X\wedge B\in Y\wedge C\in Z\right)$$
	f1dom3fv3dif.n	$$⊢\phi \to \left(A\ne B\wedge A\ne C\wedge B\ne C\right)$$
	f1dom3fv3dif.f	$$⊢\phi \to F:\left\{A,B,C\right\}\underset{1-1}{⟶}R$$
Assertion	f1dom3el3dif	$$⊢\phi \to \exists x\in R\exists y\in R\exists z\in R\left(x\ne y\wedge x\ne z\wedge y\ne z\right)$$

Proof

Step	Hyp	Ref	Expression
1		f1dom3fv3dif.v	$$⊢\phi \to \left(A\in X\wedge B\in Y\wedge C\in Z\right)$$
2		f1dom3fv3dif.n	$$⊢\phi \to \left(A\ne B\wedge A\ne C\wedge B\ne C\right)$$
3		f1dom3fv3dif.f	$$⊢\phi \to F:\left\{A,B,C\right\}\underset{1-1}{⟶}R$$
4		f1f	$$⊢F:\left\{A,B,C\right\}\underset{1-1}{⟶}R\to F:\left\{A,B,C\right\}⟶R$$
5		simpr	$$⊢\left(\phi \wedge F:\left\{A,B,C\right\}⟶R\right)\to F:\left\{A,B,C\right\}⟶R$$
6		eqidd	$$⊢\phi \to A=A$$
7	6	3mix1d	$$⊢\phi \to \left(A=A\vee A=B\vee A=C\right)$$
8	1	simp1d	$$⊢\phi \to A\in X$$
9		eltpg	$$⊢A\in X\to \left(A\in \left\{A,B,C\right\}\leftrightarrow \left(A=A\vee A=B\vee A=C\right)\right)$$
10	8 9	syl	$$⊢\phi \to \left(A\in \left\{A,B,C\right\}\leftrightarrow \left(A=A\vee A=B\vee A=C\right)\right)$$
11	7 10	mpbird	$$⊢\phi \to A\in \left\{A,B,C\right\}$$
12	11	adantr	$$⊢\left(\phi \wedge F:\left\{A,B,C\right\}⟶R\right)\to A\in \left\{A,B,C\right\}$$
13	5 12	ffvelrnd	$$⊢\left(\phi \wedge F:\left\{A,B,C\right\}⟶R\right)\to F\left(A\right)\in R$$
14		eqidd	$$⊢\phi \to B=B$$
15	14	3mix2d	$$⊢\phi \to \left(B=A\vee B=B\vee B=C\right)$$
16	1	simp2d	$$⊢\phi \to B\in Y$$
17		eltpg	$$⊢B\in Y\to \left(B\in \left\{A,B,C\right\}\leftrightarrow \left(B=A\vee B=B\vee B=C\right)\right)$$
18	16 17	syl	$$⊢\phi \to \left(B\in \left\{A,B,C\right\}\leftrightarrow \left(B=A\vee B=B\vee B=C\right)\right)$$
19	15 18	mpbird	$$⊢\phi \to B\in \left\{A,B,C\right\}$$
20	19	adantr	$$⊢\left(\phi \wedge F:\left\{A,B,C\right\}⟶R\right)\to B\in \left\{A,B,C\right\}$$
21	5 20	ffvelrnd	$$⊢\left(\phi \wedge F:\left\{A,B,C\right\}⟶R\right)\to F\left(B\right)\in R$$
22	1	simp3d	$$⊢\phi \to C\in Z$$
23		tpid3g	$$⊢C\in Z\to C\in \left\{A,B,C\right\}$$
24	22 23	syl	$$⊢\phi \to C\in \left\{A,B,C\right\}$$
25	24	adantr	$$⊢\left(\phi \wedge F:\left\{A,B,C\right\}⟶R\right)\to C\in \left\{A,B,C\right\}$$
26	5 25	ffvelrnd	$$⊢\left(\phi \wedge F:\left\{A,B,C\right\}⟶R\right)\to F\left(C\right)\in R$$
27	13 21 26	3jca	$$⊢\left(\phi \wedge F:\left\{A,B,C\right\}⟶R\right)\to \left(F\left(A\right)\in R\wedge F\left(B\right)\in R\wedge F\left(C\right)\in R\right)$$
28	27	expcom	$$⊢F:\left\{A,B,C\right\}⟶R\to \left(\phi \to \left(F\left(A\right)\in R\wedge F\left(B\right)\in R\wedge F\left(C\right)\in R\right)\right)$$
29	4 28	syl	$$⊢F:\left\{A,B,C\right\}\underset{1-1}{⟶}R\to \left(\phi \to \left(F\left(A\right)\in R\wedge F\left(B\right)\in R\wedge F\left(C\right)\in R\right)\right)$$
30	3 29	mpcom	$$⊢\phi \to \left(F\left(A\right)\in R\wedge F\left(B\right)\in R\wedge F\left(C\right)\in R\right)$$
31	1 2 3	f1dom3fv3dif	$$⊢\phi \to \left(F\left(A\right)\ne F\left(B\right)\wedge F\left(A\right)\ne F\left(C\right)\wedge F\left(B\right)\ne F\left(C\right)\right)$$
32		neeq1	$$⊢x=F\left(A\right)\to \left(x\ne y\leftrightarrow F\left(A\right)\ne y\right)$$
33		neeq1	$$⊢x=F\left(A\right)\to \left(x\ne z\leftrightarrow F\left(A\right)\ne z\right)$$
34	32 33	3anbi12d	$$⊢x=F\left(A\right)\to \left(\left(x\ne y\wedge x\ne z\wedge y\ne z\right)\leftrightarrow \left(F\left(A\right)\ne y\wedge F\left(A\right)\ne z\wedge y\ne z\right)\right)$$
35		neeq2	$$⊢y=F\left(B\right)\to \left(F\left(A\right)\ne y\leftrightarrow F\left(A\right)\ne F\left(B\right)\right)$$
36		neeq1	$$⊢y=F\left(B\right)\to \left(y\ne z\leftrightarrow F\left(B\right)\ne z\right)$$
37	35 36	3anbi13d	$$⊢y=F\left(B\right)\to \left(\left(F\left(A\right)\ne y\wedge F\left(A\right)\ne z\wedge y\ne z\right)\leftrightarrow \left(F\left(A\right)\ne F\left(B\right)\wedge F\left(A\right)\ne z\wedge F\left(B\right)\ne z\right)\right)$$
38		neeq2	$$⊢z=F\left(C\right)\to \left(F\left(A\right)\ne z\leftrightarrow F\left(A\right)\ne F\left(C\right)\right)$$
39		neeq2	$$⊢z=F\left(C\right)\to \left(F\left(B\right)\ne z\leftrightarrow F\left(B\right)\ne F\left(C\right)\right)$$
40	38 39	3anbi23d	$$⊢z=F\left(C\right)\to \left(\left(F\left(A\right)\ne F\left(B\right)\wedge F\left(A\right)\ne z\wedge F\left(B\right)\ne z\right)\leftrightarrow \left(F\left(A\right)\ne F\left(B\right)\wedge F\left(A\right)\ne F\left(C\right)\wedge F\left(B\right)\ne F\left(C\right)\right)\right)$$
41	34 37 40	rspc3ev	$$⊢\left(\left(F\left(A\right)\in R\wedge F\left(B\right)\in R\wedge F\left(C\right)\in R\right)\wedge \left(F\left(A\right)\ne F\left(B\right)\wedge F\left(A\right)\ne F\left(C\right)\wedge F\left(B\right)\ne F\left(C\right)\right)\right)\to \exists x\in R\exists y\in R\exists z\in R\left(x\ne y\wedge x\ne z\wedge y\ne z\right)$$
42	30 31 41	syl2anc	$$⊢\phi \to \exists x\in R\exists y\in R\exists z\in R\left(x\ne y\wedge x\ne z\wedge y\ne z\right)$$