f13dfv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > f13dfv		Structured version Visualization version GIF version

Theorem f13dfv 7208

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.)

**Hypothesis**
Ref	Expression
f13dfv.a	⊢ 𝐴 = {𝑋, 𝑌, 𝑍}

**Assertion**
Ref	Expression
f13dfv	⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))))

Proof of Theorem f13dfv Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dff14b 7205	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦)))
2		f13dfv.a	. . . . 5 ⊢ 𝐴 = {𝑋, 𝑌, 𝑍}
3	2	raleqi 3290	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦))
4		sneq 4586	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋})
5	4	difeq2d 4076	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑋}))
6		fveq2 6822	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋))
7	6	neeq1d 2987	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑦)))
8	5, 7	raleqbidv 3312	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦)))
9		sneq 4586	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → {𝑥} = {𝑌})
10	9	difeq2d 4076	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑌}))
11		fveq2 6822	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → (𝐹‘𝑥) = (𝐹‘𝑌))
12	11	neeq1d 2987	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑦)))
13	10, 12	raleqbidv 3312	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦)))
14		sneq 4586	. . . . . . . . 9 ⊢ (𝑥 = 𝑍 → {𝑥} = {𝑍})
15	14	difeq2d 4076	. . . . . . . 8 ⊢ (𝑥 = 𝑍 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑍}))
16		fveq2 6822	. . . . . . . . 9 ⊢ (𝑥 = 𝑍 → (𝐹‘𝑥) = (𝐹‘𝑍))
17	16	neeq1d 2987	. . . . . . . 8 ⊢ (𝑥 = 𝑍 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑦)))
18	15, 17	raleqbidv 3312	. . . . . . 7 ⊢ (𝑥 = 𝑍 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦)))
19	8, 13, 18	raltpg 4651	. . . . . 6 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦))))
20	19	adantr 480	. . . . 5 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦))))
21	2	difeq1i 4072	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑋}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑋})
22		tprot 4702	. . . . . . . . . . . . 13 ⊢ {𝑋, 𝑌, 𝑍} = {𝑌, 𝑍, 𝑋}
23	22	difeq1i 4072	. . . . . . . . . . . 12 ⊢ ({𝑋, 𝑌, 𝑍} ∖ {𝑋}) = ({𝑌, 𝑍, 𝑋} ∖ {𝑋})
24		necom 2981	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ≠ 𝑌 ↔ 𝑌 ≠ 𝑋)
25		necom 2981	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ≠ 𝑍 ↔ 𝑍 ≠ 𝑋)
26	24, 25	anbi12i 628	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍) ↔ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋))
27	26	biimpi 216	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍) → (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋))
28	27	3adant3 1132	. . . . . . . . . . . . 13 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋))
29		diftpsn3 4754	. . . . . . . . . . . . 13 ⊢ ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → ({𝑌, 𝑍, 𝑋} ∖ {𝑋}) = {𝑌, 𝑍})
30	28, 29	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑌, 𝑍, 𝑋} ∖ {𝑋}) = {𝑌, 𝑍})
31	23, 30	eqtrid 2778	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑋}) = {𝑌, 𝑍})
32	21, 31	eqtrid 2778	. . . . . . . . . 10 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑋}) = {𝑌, 𝑍})
33	32	adantl 481	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑋}) = {𝑌, 𝑍})
34	33	raleqdv 3292	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦)))
35		fveq2 6822	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌))
36	35	neeq2d 2988	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌)))
37		fveq2 6822	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑍 → (𝐹‘𝑦) = (𝐹‘𝑍))
38	37	neeq2d 2988	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑍 → ((𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑍)))
39	36, 38	ralprg 4649	. . . . . . . . . 10 ⊢ ((𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
40	39	3adant1 1130	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
41	40	adantr 480	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
42	34, 41	bitrd 279	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
43	2	difeq1i 4072	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑌}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑌})
44		tpcomb 4704	. . . . . . . . . . . . 13 ⊢ {𝑋, 𝑌, 𝑍} = {𝑋, 𝑍, 𝑌}
45	44	difeq1i 4072	. . . . . . . . . . . 12 ⊢ ({𝑋, 𝑌, 𝑍} ∖ {𝑌}) = ({𝑋, 𝑍, 𝑌} ∖ {𝑌})
46		necom 2981	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ≠ 𝑍 ↔ 𝑍 ≠ 𝑌)
47	46	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ≠ 𝑍 → 𝑍 ≠ 𝑌)
48	47	anim2i 617	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑌 ≠ 𝑍) → (𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌))
49	48	3adant2 1131	. . . . . . . . . . . . 13 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌))
50		diftpsn3 4754	. . . . . . . . . . . . 13 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌) → ({𝑋, 𝑍, 𝑌} ∖ {𝑌}) = {𝑋, 𝑍})
51	49, 50	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑍, 𝑌} ∖ {𝑌}) = {𝑋, 𝑍})
52	45, 51	eqtrid 2778	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑌}) = {𝑋, 𝑍})
53	43, 52	eqtrid 2778	. . . . . . . . . 10 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑌}) = {𝑋, 𝑍})
54	53	adantl 481	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑌}) = {𝑋, 𝑍})
55	54	raleqdv 3292	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦)))
56		fveq2 6822	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (𝐹‘𝑦) = (𝐹‘𝑋))
57	56	neeq2d 2988	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑋)))
58	37	neeq2d 2988	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑍 → ((𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
59	57, 58	ralprg 4649	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
60	59	3adant2 1131	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
61	60	adantr 480	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
62	55, 61	bitrd 279	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
63	2	difeq1i 4072	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑍}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑍})
64		diftpsn3 4754	. . . . . . . . . . . 12 ⊢ ((𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑍}) = {𝑋, 𝑌})
65	64	3adant1 1130	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑍}) = {𝑋, 𝑌})
66	63, 65	eqtrid 2778	. . . . . . . . . 10 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑍}) = {𝑋, 𝑌})
67	66	adantl 481	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑍}) = {𝑋, 𝑌})
68	67	raleqdv 3292	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦)))
69	56	neeq2d 2988	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑋)))
70	35	neeq2d 2988	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑌)))
71	69, 70	ralprg 4649	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → (∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
72	71	3adant3 1132	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
73	72	adantr 480	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
74	68, 73	bitrd 279	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
75	42, 62, 74	3anbi123d 1438	. . . . . 6 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦)) ↔ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌)))))
76		ancom 460	. . . . . . . 8 ⊢ (((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋)))
77	76	3anbi2i 1158	. . . . . . 7 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
78		3an6 1448	. . . . . . 7 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
79		3anrot 1099	. . . . . . . . . 10 ⊢ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)))
80	79	bicomi 224	. . . . . . . . 9 ⊢ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
81		necom 2981	. . . . . . . . . 10 ⊢ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑋))
82		necom 2981	. . . . . . . . . 10 ⊢ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌))
83		necom 2981	. . . . . . . . . 10 ⊢ ((𝐹‘𝑍) ≠ (𝐹‘𝑌) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑍))
84	81, 82, 83	3anbi123i 1155	. . . . . . . . 9 ⊢ (((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌)) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
85	80, 84	anbi12i 628	. . . . . . . 8 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
86		anidm 564	. . . . . . . 8 ⊢ ((((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
87		3ancoma 1097	. . . . . . . . 9 ⊢ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
88		necom 2981	. . . . . . . . . 10 ⊢ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑍))
89	88	3anbi2i 1158	. . . . . . . . 9 ⊢ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
90	87, 89	bitri 275	. . . . . . . 8 ⊢ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
91	85, 86, 90	3bitri 297	. . . . . . 7 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
92	77, 78, 91	3bitri 297	. . . . . 6 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
93	75, 92	bitrdi 287	. . . . 5 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
94	20, 93	bitrd 279	. . . 4 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
95	3, 94	bitrid 283	. . 3 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
96	95	anbi2d 630	. 2 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦)) ↔ (𝐹:𝐴⟶𝐵 ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))))
97	1, 96	bitrid 283	1 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∖ cdif 3899 {csn 4576 {cpr 4578 {ctp 4580 ⟶wf 6477 –1-1→wf1 6478 ‘cfv 6481

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5234 ax-nul 5244 ax-pr 5370

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4284 df-if 4476 df-sn 4577 df-pr 4579 df-tp 4581 df-op 4583 df-uni 4860 df-br 5092 df-opab 5154 df-id 5511 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fv 6489

This theorem is referenced by: f13idfv 13907 cyc3evpm 33117

W3C validator