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 7220

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 7218	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦)))
2		f13dfv.a	. . . . 5 ⊢ 𝐴 = {𝑋, 𝑌, 𝑍}
3	2	raleqi 3311	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦))
4		sneq 4596	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋})
5	4	difeq2d 4082	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑋}))
6		fveq2 6842	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋))
7	6	neeq1d 3003	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑦)))
8	5, 7	raleqbidv 3319	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦)))
9		sneq 4596	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → {𝑥} = {𝑌})
10	9	difeq2d 4082	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑌}))
11		fveq2 6842	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → (𝐹‘𝑥) = (𝐹‘𝑌))
12	11	neeq1d 3003	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑦)))
13	10, 12	raleqbidv 3319	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦)))
14		sneq 4596	. . . . . . . . 9 ⊢ (𝑥 = 𝑍 → {𝑥} = {𝑍})
15	14	difeq2d 4082	. . . . . . . 8 ⊢ (𝑥 = 𝑍 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑍}))
16		fveq2 6842	. . . . . . . . 9 ⊢ (𝑥 = 𝑍 → (𝐹‘𝑥) = (𝐹‘𝑍))
17	16	neeq1d 3003	. . . . . . . 8 ⊢ (𝑥 = 𝑍 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑦)))
18	15, 17	raleqbidv 3319	. . . . . . 7 ⊢ (𝑥 = 𝑍 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦)))
19	8, 13, 18	raltpg 4659	. . . . . 6 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦))))
20	19	adantr 481	. . . . 5 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦))))
21	2	difeq1i 4078	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑋}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑋})
22		tprot 4710	. . . . . . . . . . . . 13 ⊢ {𝑋, 𝑌, 𝑍} = {𝑌, 𝑍, 𝑋}
23	22	difeq1i 4078	. . . . . . . . . . . 12 ⊢ ({𝑋, 𝑌, 𝑍} ∖ {𝑋}) = ({𝑌, 𝑍, 𝑋} ∖ {𝑋})
24		necom 2997	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ≠ 𝑌 ↔ 𝑌 ≠ 𝑋)
25		necom 2997	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ≠ 𝑍 ↔ 𝑍 ≠ 𝑋)
26	24, 25	anbi12i 627	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍) ↔ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋))
27	26	biimpi 215	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍) → (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋))
28	27	3adant3 1132	. . . . . . . . . . . . 13 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋))
29		diftpsn3 4762	. . . . . . . . . . . . 13 ⊢ ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → ({𝑌, 𝑍, 𝑋} ∖ {𝑋}) = {𝑌, 𝑍})
30	28, 29	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑌, 𝑍, 𝑋} ∖ {𝑋}) = {𝑌, 𝑍})
31	23, 30	eqtrid 2788	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑋}) = {𝑌, 𝑍})
32	21, 31	eqtrid 2788	. . . . . . . . . 10 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑋}) = {𝑌, 𝑍})
33	32	adantl 482	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑋}) = {𝑌, 𝑍})
34	33	raleqdv 3313	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦)))
35		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌))
36	35	neeq2d 3004	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌)))
37		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑍 → (𝐹‘𝑦) = (𝐹‘𝑍))
38	37	neeq2d 3004	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑍 → ((𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑍)))
39	36, 38	ralprg 4655	. . . . . . . . . 10 ⊢ ((𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
40	39	3adant1 1130	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
41	40	adantr 481	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
42	34, 41	bitrd 278	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
43	2	difeq1i 4078	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑌}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑌})
44		tpcomb 4712	. . . . . . . . . . . . 13 ⊢ {𝑋, 𝑌, 𝑍} = {𝑋, 𝑍, 𝑌}
45	44	difeq1i 4078	. . . . . . . . . . . 12 ⊢ ({𝑋, 𝑌, 𝑍} ∖ {𝑌}) = ({𝑋, 𝑍, 𝑌} ∖ {𝑌})
46		necom 2997	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ≠ 𝑍 ↔ 𝑍 ≠ 𝑌)
47	46	biimpi 215	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ≠ 𝑍 → 𝑍 ≠ 𝑌)
48	47	anim2i 617	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑌 ≠ 𝑍) → (𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌))
49	48	3adant2 1131	. . . . . . . . . . . . 13 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌))
50		diftpsn3 4762	. . . . . . . . . . . . 13 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌) → ({𝑋, 𝑍, 𝑌} ∖ {𝑌}) = {𝑋, 𝑍})
51	49, 50	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑍, 𝑌} ∖ {𝑌}) = {𝑋, 𝑍})
52	45, 51	eqtrid 2788	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑌}) = {𝑋, 𝑍})
53	43, 52	eqtrid 2788	. . . . . . . . . 10 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑌}) = {𝑋, 𝑍})
54	53	adantl 482	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑌}) = {𝑋, 𝑍})
55	54	raleqdv 3313	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦)))
56		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (𝐹‘𝑦) = (𝐹‘𝑋))
57	56	neeq2d 3004	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑋)))
58	37	neeq2d 3004	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑍 → ((𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
59	57, 58	ralprg 4655	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
60	59	3adant2 1131	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
61	60	adantr 481	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
62	55, 61	bitrd 278	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
63	2	difeq1i 4078	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑍}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑍})
64		diftpsn3 4762	. . . . . . . . . . . 12 ⊢ ((𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑍}) = {𝑋, 𝑌})
65	64	3adant1 1130	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑍}) = {𝑋, 𝑌})
66	63, 65	eqtrid 2788	. . . . . . . . . 10 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑍}) = {𝑋, 𝑌})
67	66	adantl 482	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑍}) = {𝑋, 𝑌})
68	67	raleqdv 3313	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦)))
69	56	neeq2d 3004	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑋)))
70	35	neeq2d 3004	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑌)))
71	69, 70	ralprg 4655	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → (∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
72	71	3adant3 1132	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
73	72	adantr 481	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
74	68, 73	bitrd 278	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
75	42, 62, 74	3anbi123d 1436	. . . . . 6 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦)) ↔ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌)))))
76		ancom 461	. . . . . . . 8 ⊢ (((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋)))
77	76	3anbi2i 1158	. . . . . . 7 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
78		3an6 1446	. . . . . . 7 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
79		3anrot 1100	. . . . . . . . . 10 ⊢ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)))
80	79	bicomi 223	. . . . . . . . 9 ⊢ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
81		necom 2997	. . . . . . . . . 10 ⊢ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑋))
82		necom 2997	. . . . . . . . . 10 ⊢ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌))
83		necom 2997	. . . . . . . . . 10 ⊢ ((𝐹‘𝑍) ≠ (𝐹‘𝑌) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑍))
84	81, 82, 83	3anbi123i 1155	. . . . . . . . 9 ⊢ (((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌)) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
85	80, 84	anbi12i 627	. . . . . . . 8 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
86		anidm 565	. . . . . . . 8 ⊢ ((((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
87		3ancoma 1098	. . . . . . . . 9 ⊢ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
88		necom 2997	. . . . . . . . . 10 ⊢ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑍))
89	88	3anbi2i 1158	. . . . . . . . 9 ⊢ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
90	87, 89	bitri 274	. . . . . . . 8 ⊢ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
91	85, 86, 90	3bitri 296	. . . . . . 7 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
92	77, 78, 91	3bitri 296	. . . . . 6 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
93	75, 92	bitrdi 286	. . . . 5 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
94	20, 93	bitrd 278	. . . 4 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
95	3, 94	bitrid 282	. . 3 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
96	95	anbi2d 629	. 2 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦)) ↔ (𝐹:𝐴⟶𝐵 ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))))
97	1, 96	bitrid 282	1 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∖ cdif 3907 {csn 4586 {cpr 4588 {ctp 4590 ⟶wf 6492 –1-1→wf1 6493 ‘cfv 6496

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-tp 4591 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fv 6504

This theorem is referenced by: f13idfv 13905 cyc3evpm 31999

W3C validator