f13dfv

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

		Ref	Expression
	Hypothesis	f13dfv.a	$⊢ A = \{X, Y, Z\}$
	Assertion	f13dfv	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land (F (X) \neq F (Y) \land F (X) \neq F (Z) \land F (Y) \neq F (Z))))$

Proof

Step	Hyp	Ref	Expression
1		f13dfv.a	$⊢ A = \{X, Y, Z\}$
2		dff14b	$⊢ F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land \forall x \in A \forall y \in (A ∖ \{x\}) F (x) \neq F (y))$
3	1	raleqi	$⊢ \forall x \in A \forall y \in (A ∖ \{x\}) F (x) \neq F (y) \leftrightarrow \forall x \in \{X, Y, Z\} \forall y \in (A ∖ \{x\}) F (x) \neq F (y)$
4		sneq	$⊢ x = X \to \{x\} = \{X\}$
5	4	difeq2d	$⊢ x = X \to A ∖ \{x\} = A ∖ \{X\}$
6		fveq2	$⊢ x = X \to F (x) = F (X)$
7	6	neeq1d	$⊢ x = X \to (F (x) \neq F (y) \leftrightarrow F (X) \neq F (y))$
8	5 7	raleqbidv	$⊢ x = X \to (\forall y \in (A ∖ \{x\}) F (x) \neq F (y) \leftrightarrow \forall y \in (A ∖ \{X\}) F (X) \neq F (y))$
9		sneq	$⊢ x = Y \to \{x\} = \{Y\}$
10	9	difeq2d	$⊢ x = Y \to A ∖ \{x\} = A ∖ \{Y\}$
11		fveq2	$⊢ x = Y \to F (x) = F (Y)$
12	11	neeq1d	$⊢ x = Y \to (F (x) \neq F (y) \leftrightarrow F (Y) \neq F (y))$
13	10 12	raleqbidv	$⊢ x = Y \to (\forall y \in (A ∖ \{x\}) F (x) \neq F (y) \leftrightarrow \forall y \in (A ∖ \{Y\}) F (Y) \neq F (y))$
14		sneq	$⊢ x = Z \to \{x\} = \{Z\}$
15	14	difeq2d	$⊢ x = Z \to A ∖ \{x\} = A ∖ \{Z\}$
16		fveq2	$⊢ x = Z \to F (x) = F (Z)$
17	16	neeq1d	$⊢ x = Z \to (F (x) \neq F (y) \leftrightarrow F (Z) \neq F (y))$
18	15 17	raleqbidv	$⊢ x = Z \to (\forall y \in (A ∖ \{x\}) F (x) \neq F (y) \leftrightarrow \forall y \in (A ∖ \{Z\}) F (Z) \neq F (y))$
19	8 13 18	raltpg	$⊢ (X \in U \land Y \in V \land Z \in W) \to (\forall x \in \{X, Y, Z\} \forall y \in (A ∖ \{x\}) F (x) \neq F (y) \leftrightarrow (\forall y \in (A ∖ \{X\}) F (X) \neq F (y) \land \forall y \in (A ∖ \{Y\}) F (Y) \neq F (y) \land \forall y \in (A ∖ \{Z\}) F (Z) \neq F (y)))$
20	19	adantr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (\forall x \in \{X, Y, Z\} \forall y \in (A ∖ \{x\}) F (x) \neq F (y) \leftrightarrow (\forall y \in (A ∖ \{X\}) F (X) \neq F (y) \land \forall y \in (A ∖ \{Y\}) F (Y) \neq F (y) \land \forall y \in (A ∖ \{Z\}) F (Z) \neq F (y)))$
21	1	difeq1i	$⊢ A ∖ \{X\} = \{X, Y, Z\} ∖ \{X\}$
22		tprot	$⊢ \{X, Y, Z\} = \{Y, Z, X\}$
23	22	difeq1i	$⊢ \{X, Y, Z\} ∖ \{X\} = \{Y, Z, X\} ∖ \{X\}$
24		necom	$⊢ X \neq Y \leftrightarrow Y \neq X$
25		necom	$⊢ X \neq Z \leftrightarrow Z \neq X$
26	24 25	anbi12i	$⊢ (X \neq Y \land X \neq Z) \leftrightarrow (Y \neq X \land Z \neq X)$
27	26	biimpi	$⊢ (X \neq Y \land X \neq Z) \to (Y \neq X \land Z \neq X)$
28	27	3adant3	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to (Y \neq X \land Z \neq X)$
29		diftpsn3	$⊢ (Y \neq X \land Z \neq X) \to \{Y, Z, X\} ∖ \{X\} = \{Y, Z\}$
30	28 29	syl	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to \{Y, Z, X\} ∖ \{X\} = \{Y, Z\}$
31	23 30	syl5eq	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to \{X, Y, Z\} ∖ \{X\} = \{Y, Z\}$
32	21 31	syl5eq	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to A ∖ \{X\} = \{Y, Z\}$
33	32	adantl	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to A ∖ \{X\} = \{Y, Z\}$
34	33	raleqdv	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (\forall y \in (A ∖ \{X\}) F (X) \neq F (y) \leftrightarrow \forall y \in \{Y, Z\} F (X) \neq F (y))$
35		fveq2	$⊢ y = Y \to F (y) = F (Y)$
36	35	neeq2d	$⊢ y = Y \to (F (X) \neq F (y) \leftrightarrow F (X) \neq F (Y))$
37		fveq2	$⊢ y = Z \to F (y) = F (Z)$
38	37	neeq2d	$⊢ y = Z \to (F (X) \neq F (y) \leftrightarrow F (X) \neq F (Z))$
39	36 38	ralprg	$⊢ (Y \in V \land Z \in W) \to (\forall y \in \{Y, Z\} F (X) \neq F (y) \leftrightarrow (F (X) \neq F (Y) \land F (X) \neq F (Z)))$
40	39	3adant1	$⊢ (X \in U \land Y \in V \land Z \in W) \to (\forall y \in \{Y, Z\} F (X) \neq F (y) \leftrightarrow (F (X) \neq F (Y) \land F (X) \neq F (Z)))$
41	40	adantr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (\forall y \in \{Y, Z\} F (X) \neq F (y) \leftrightarrow (F (X) \neq F (Y) \land F (X) \neq F (Z)))$
42	34 41	bitrd	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (\forall y \in (A ∖ \{X\}) F (X) \neq F (y) \leftrightarrow (F (X) \neq F (Y) \land F (X) \neq F (Z)))$
43	1	difeq1i	$⊢ A ∖ \{Y\} = \{X, Y, Z\} ∖ \{Y\}$
44		tpcomb	$⊢ \{X, Y, Z\} = \{X, Z, Y\}$
45	44	difeq1i	$⊢ \{X, Y, Z\} ∖ \{Y\} = \{X, Z, Y\} ∖ \{Y\}$
46		necom	$⊢ Y \neq Z \leftrightarrow Z \neq Y$
47	46	biimpi	$⊢ Y \neq Z \to Z \neq Y$
48	47	anim2i	$⊢ (X \neq Y \land Y \neq Z) \to (X \neq Y \land Z \neq Y)$
49	48	3adant2	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to (X \neq Y \land Z \neq Y)$
50		diftpsn3	$⊢ (X \neq Y \land Z \neq Y) \to \{X, Z, Y\} ∖ \{Y\} = \{X, Z\}$
51	49 50	syl	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to \{X, Z, Y\} ∖ \{Y\} = \{X, Z\}$
52	45 51	syl5eq	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to \{X, Y, Z\} ∖ \{Y\} = \{X, Z\}$
53	43 52	syl5eq	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to A ∖ \{Y\} = \{X, Z\}$
54	53	adantl	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to A ∖ \{Y\} = \{X, Z\}$
55	54	raleqdv	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (\forall y \in (A ∖ \{Y\}) F (Y) \neq F (y) \leftrightarrow \forall y \in \{X, Z\} F (Y) \neq F (y))$
56		fveq2	$⊢ y = X \to F (y) = F (X)$
57	56	neeq2d	$⊢ y = X \to (F (Y) \neq F (y) \leftrightarrow F (Y) \neq F (X))$
58	37	neeq2d	$⊢ y = Z \to (F (Y) \neq F (y) \leftrightarrow F (Y) \neq F (Z))$
59	57 58	ralprg	$⊢ (X \in U \land Z \in W) \to (\forall y \in \{X, Z\} F (Y) \neq F (y) \leftrightarrow (F (Y) \neq F (X) \land F (Y) \neq F (Z)))$
60	59	3adant2	$⊢ (X \in U \land Y \in V \land Z \in W) \to (\forall y \in \{X, Z\} F (Y) \neq F (y) \leftrightarrow (F (Y) \neq F (X) \land F (Y) \neq F (Z)))$
61	60	adantr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (\forall y \in \{X, Z\} F (Y) \neq F (y) \leftrightarrow (F (Y) \neq F (X) \land F (Y) \neq F (Z)))$
62	55 61	bitrd	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (\forall y \in (A ∖ \{Y\}) F (Y) \neq F (y) \leftrightarrow (F (Y) \neq F (X) \land F (Y) \neq F (Z)))$
63	1	difeq1i	$⊢ A ∖ \{Z\} = \{X, Y, Z\} ∖ \{Z\}$
64		diftpsn3	$⊢ (X \neq Z \land Y \neq Z) \to \{X, Y, Z\} ∖ \{Z\} = \{X, Y\}$
65	64	3adant1	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to \{X, Y, Z\} ∖ \{Z\} = \{X, Y\}$
66	63 65	syl5eq	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to A ∖ \{Z\} = \{X, Y\}$
67	66	adantl	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to A ∖ \{Z\} = \{X, Y\}$
68	67	raleqdv	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (\forall y \in (A ∖ \{Z\}) F (Z) \neq F (y) \leftrightarrow \forall y \in \{X, Y\} F (Z) \neq F (y))$
69	56	neeq2d	$⊢ y = X \to (F (Z) \neq F (y) \leftrightarrow F (Z) \neq F (X))$
70	35	neeq2d	$⊢ y = Y \to (F (Z) \neq F (y) \leftrightarrow F (Z) \neq F (Y))$
71	69 70	ralprg	$⊢ (X \in U \land Y \in V) \to (\forall y \in \{X, Y\} F (Z) \neq F (y) \leftrightarrow (F (Z) \neq F (X) \land F (Z) \neq F (Y)))$
72	71	3adant3	$⊢ (X \in U \land Y \in V \land Z \in W) \to (\forall y \in \{X, Y\} F (Z) \neq F (y) \leftrightarrow (F (Z) \neq F (X) \land F (Z) \neq F (Y)))$
73	72	adantr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (\forall y \in \{X, Y\} F (Z) \neq F (y) \leftrightarrow (F (Z) \neq F (X) \land F (Z) \neq F (Y)))$
74	68 73	bitrd	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (\forall y \in (A ∖ \{Z\}) F (Z) \neq F (y) \leftrightarrow (F (Z) \neq F (X) \land F (Z) \neq F (Y)))$
75	42 62 74	3anbi123d	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to ((\forall y \in (A ∖ \{X\}) F (X) \neq F (y) \land \forall y \in (A ∖ \{Y\}) F (Y) \neq F (y) \land \forall y \in (A ∖ \{Z\}) F (Z) \neq F (y)) \leftrightarrow ((F (X) \neq F (Y) \land F (X) \neq F (Z)) \land (F (Y) \neq F (X) \land F (Y) \neq F (Z)) \land (F (Z) \neq F (X) \land F (Z) \neq F (Y))))$
76		ancom	$⊢ (F (Y) \neq F (X) \land F (Y) \neq F (Z)) \leftrightarrow (F (Y) \neq F (Z) \land F (Y) \neq F (X))$
77	76	3anbi2i	$⊢ ((F (X) \neq F (Y) \land F (X) \neq F (Z)) \land (F (Y) \neq F (X) \land F (Y) \neq F (Z)) \land (F (Z) \neq F (X) \land F (Z) \neq F (Y))) \leftrightarrow ((F (X) \neq F (Y) \land F (X) \neq F (Z)) \land (F (Y) \neq F (Z) \land F (Y) \neq F (X)) \land (F (Z) \neq F (X) \land F (Z) \neq F (Y)))$
78		3an6	$⊢ ((F (X) \neq F (Y) \land F (X) \neq F (Z)) \land (F (Y) \neq F (Z) \land F (Y) \neq F (X)) \land (F (Z) \neq F (X) \land F (Z) \neq F (Y))) \leftrightarrow ((F (X) \neq F (Y) \land F (Y) \neq F (Z) \land F (Z) \neq F (X)) \land (F (X) \neq F (Z) \land F (Y) \neq F (X) \land F (Z) \neq F (Y)))$
79		3anrot	$⊢ (F (Z) \neq F (X) \land F (X) \neq F (Y) \land F (Y) \neq F (Z)) \leftrightarrow (F (X) \neq F (Y) \land F (Y) \neq F (Z) \land F (Z) \neq F (X))$
80	79	bicomi	$⊢ (F (X) \neq F (Y) \land F (Y) \neq F (Z) \land F (Z) \neq F (X)) \leftrightarrow (F (Z) \neq F (X) \land F (X) \neq F (Y) \land F (Y) \neq F (Z))$
81		necom	$⊢ F (X) \neq F (Z) \leftrightarrow F (Z) \neq F (X)$
82		necom	$⊢ F (Y) \neq F (X) \leftrightarrow F (X) \neq F (Y)$
83		necom	$⊢ F (Z) \neq F (Y) \leftrightarrow F (Y) \neq F (Z)$
84	81 82 83	3anbi123i	$⊢ (F (X) \neq F (Z) \land F (Y) \neq F (X) \land F (Z) \neq F (Y)) \leftrightarrow (F (Z) \neq F (X) \land F (X) \neq F (Y) \land F (Y) \neq F (Z))$
85	80 84	anbi12i	$⊢ ((F (X) \neq F (Y) \land F (Y) \neq F (Z) \land F (Z) \neq F (X)) \land (F (X) \neq F (Z) \land F (Y) \neq F (X) \land F (Z) \neq F (Y))) \leftrightarrow ((F (Z) \neq F (X) \land F (X) \neq F (Y) \land F (Y) \neq F (Z)) \land (F (Z) \neq F (X) \land F (X) \neq F (Y) \land F (Y) \neq F (Z)))$
86		anidm	$⊢ ((F (Z) \neq F (X) \land F (X) \neq F (Y) \land F (Y) \neq F (Z)) \land (F (Z) \neq F (X) \land F (X) \neq F (Y) \land F (Y) \neq F (Z))) \leftrightarrow (F (Z) \neq F (X) \land F (X) \neq F (Y) \land F (Y) \neq F (Z))$
87		3ancoma	$⊢ (F (Z) \neq F (X) \land F (X) \neq F (Y) \land F (Y) \neq F (Z)) \leftrightarrow (F (X) \neq F (Y) \land F (Z) \neq F (X) \land F (Y) \neq F (Z))$
88		necom	$⊢ F (Z) \neq F (X) \leftrightarrow F (X) \neq F (Z)$
89	88	3anbi2i	$⊢ (F (X) \neq F (Y) \land F (Z) \neq F (X) \land F (Y) \neq F (Z)) \leftrightarrow (F (X) \neq F (Y) \land F (X) \neq F (Z) \land F (Y) \neq F (Z))$
90	87 89	bitri	$⊢ (F (Z) \neq F (X) \land F (X) \neq F (Y) \land F (Y) \neq F (Z)) \leftrightarrow (F (X) \neq F (Y) \land F (X) \neq F (Z) \land F (Y) \neq F (Z))$
91	85 86 90	3bitri	$⊢ ((F (X) \neq F (Y) \land F (Y) \neq F (Z) \land F (Z) \neq F (X)) \land (F (X) \neq F (Z) \land F (Y) \neq F (X) \land F (Z) \neq F (Y))) \leftrightarrow (F (X) \neq F (Y) \land F (X) \neq F (Z) \land F (Y) \neq F (Z))$
92	77 78 91	3bitri	$⊢ ((F (X) \neq F (Y) \land F (X) \neq F (Z)) \land (F (Y) \neq F (X) \land F (Y) \neq F (Z)) \land (F (Z) \neq F (X) \land F (Z) \neq F (Y))) \leftrightarrow (F (X) \neq F (Y) \land F (X) \neq F (Z) \land F (Y) \neq F (Z))$
93	75 92	bitrdi	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to ((\forall y \in (A ∖ \{X\}) F (X) \neq F (y) \land \forall y \in (A ∖ \{Y\}) F (Y) \neq F (y) \land \forall y \in (A ∖ \{Z\}) F (Z) \neq F (y)) \leftrightarrow (F (X) \neq F (Y) \land F (X) \neq F (Z) \land F (Y) \neq F (Z)))$
94	20 93	bitrd	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (\forall x \in \{X, Y, Z\} \forall y \in (A ∖ \{x\}) F (x) \neq F (y) \leftrightarrow (F (X) \neq F (Y) \land F (X) \neq F (Z) \land F (Y) \neq F (Z)))$
95	3 94	syl5bb	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (\forall x \in A \forall y \in (A ∖ \{x\}) F (x) \neq F (y) \leftrightarrow (F (X) \neq F (Y) \land F (X) \neq F (Z) \land F (Y) \neq F (Z)))$
96	95	anbi2d	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to ((F : A ⟶ B \land \forall x \in A \forall y \in (A ∖ \{x\}) F (x) \neq F (y)) \leftrightarrow (F : A ⟶ B \land (F (X) \neq F (Y) \land F (X) \neq F (Z) \land F (Y) \neq F (Z))))$
97	2 96	syl5bb	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to (F : A \underset{1-1}{⟶} B \leftrightarrow (F : A ⟶ B \land (F (X) \neq F (Y) \land F (X) \neq F (Z) \land F (Y) \neq F (Z))))$

Metamath Proof Explorer

Theorem f13dfv

Proof