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 7025

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 7023	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦)))
2		f13dfv.a	. . . . 5 ⊢ 𝐴 = {𝑋, 𝑌, 𝑍}
3	2	raleqi 3413	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦))
4		sneq 4570	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋})
5	4	difeq2d 4098	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑋}))
6		fveq2 6664	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋))
7	6	neeq1d 3075	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑦)))
8	5, 7	raleqbidv 3401	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦)))
9		sneq 4570	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → {𝑥} = {𝑌})
10	9	difeq2d 4098	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑌}))
11		fveq2 6664	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → (𝐹‘𝑥) = (𝐹‘𝑌))
12	11	neeq1d 3075	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑦)))
13	10, 12	raleqbidv 3401	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦)))
14		sneq 4570	. . . . . . . . 9 ⊢ (𝑥 = 𝑍 → {𝑥} = {𝑍})
15	14	difeq2d 4098	. . . . . . . 8 ⊢ (𝑥 = 𝑍 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑍}))
16		fveq2 6664	. . . . . . . . 9 ⊢ (𝑥 = 𝑍 → (𝐹‘𝑥) = (𝐹‘𝑍))
17	16	neeq1d 3075	. . . . . . . 8 ⊢ (𝑥 = 𝑍 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑦)))
18	15, 17	raleqbidv 3401	. . . . . . 7 ⊢ (𝑥 = 𝑍 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦)))
19	8, 13, 18	raltpg 4627	. . . . . 6 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦))))
20	19	adantr 483	. . . . 5 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦))))
21	2	difeq1i 4094	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑋}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑋})
22		tprot 4678	. . . . . . . . . . . . 13 ⊢ {𝑋, 𝑌, 𝑍} = {𝑌, 𝑍, 𝑋}
23	22	difeq1i 4094	. . . . . . . . . . . 12 ⊢ ({𝑋, 𝑌, 𝑍} ∖ {𝑋}) = ({𝑌, 𝑍, 𝑋} ∖ {𝑋})
24		necom 3069	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ≠ 𝑌 ↔ 𝑌 ≠ 𝑋)
25		necom 3069	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ≠ 𝑍 ↔ 𝑍 ≠ 𝑋)
26	24, 25	anbi12i 628	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍) ↔ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋))
27	26	biimpi 218	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍) → (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋))
28	27	3adant3 1128	. . . . . . . . . . . . 13 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋))
29		diftpsn3 4728	. . . . . . . . . . . . 13 ⊢ ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → ({𝑌, 𝑍, 𝑋} ∖ {𝑋}) = {𝑌, 𝑍})
30	28, 29	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑌, 𝑍, 𝑋} ∖ {𝑋}) = {𝑌, 𝑍})
31	23, 30	syl5eq 2868	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑋}) = {𝑌, 𝑍})
32	21, 31	syl5eq 2868	. . . . . . . . . 10 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑋}) = {𝑌, 𝑍})
33	32	adantl 484	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑋}) = {𝑌, 𝑍})
34	33	raleqdv 3415	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦)))
35		fveq2 6664	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌))
36	35	neeq2d 3076	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌)))
37		fveq2 6664	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑍 → (𝐹‘𝑦) = (𝐹‘𝑍))
38	37	neeq2d 3076	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑍 → ((𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑍)))
39	36, 38	ralprg 4625	. . . . . . . . . 10 ⊢ ((𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
40	39	3adant1 1126	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
41	40	adantr 483	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
42	34, 41	bitrd 281	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
43	2	difeq1i 4094	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑌}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑌})
44		tpcomb 4680	. . . . . . . . . . . . 13 ⊢ {𝑋, 𝑌, 𝑍} = {𝑋, 𝑍, 𝑌}
45	44	difeq1i 4094	. . . . . . . . . . . 12 ⊢ ({𝑋, 𝑌, 𝑍} ∖ {𝑌}) = ({𝑋, 𝑍, 𝑌} ∖ {𝑌})
46		necom 3069	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ≠ 𝑍 ↔ 𝑍 ≠ 𝑌)
47	46	biimpi 218	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ≠ 𝑍 → 𝑍 ≠ 𝑌)
48	47	anim2i 618	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑌 ≠ 𝑍) → (𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌))
49	48	3adant2 1127	. . . . . . . . . . . . 13 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌))
50		diftpsn3 4728	. . . . . . . . . . . . 13 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌) → ({𝑋, 𝑍, 𝑌} ∖ {𝑌}) = {𝑋, 𝑍})
51	49, 50	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑍, 𝑌} ∖ {𝑌}) = {𝑋, 𝑍})
52	45, 51	syl5eq 2868	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑌}) = {𝑋, 𝑍})
53	43, 52	syl5eq 2868	. . . . . . . . . 10 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑌}) = {𝑋, 𝑍})
54	53	adantl 484	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑌}) = {𝑋, 𝑍})
55	54	raleqdv 3415	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦)))
56		fveq2 6664	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (𝐹‘𝑦) = (𝐹‘𝑋))
57	56	neeq2d 3076	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑋)))
58	37	neeq2d 3076	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑍 → ((𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
59	57, 58	ralprg 4625	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
60	59	3adant2 1127	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
61	60	adantr 483	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
62	55, 61	bitrd 281	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
63	2	difeq1i 4094	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑍}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑍})
64		diftpsn3 4728	. . . . . . . . . . . 12 ⊢ ((𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑍}) = {𝑋, 𝑌})
65	64	3adant1 1126	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑍}) = {𝑋, 𝑌})
66	63, 65	syl5eq 2868	. . . . . . . . . 10 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑍}) = {𝑋, 𝑌})
67	66	adantl 484	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑍}) = {𝑋, 𝑌})
68	67	raleqdv 3415	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦)))
69	56	neeq2d 3076	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑋)))
70	35	neeq2d 3076	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑌)))
71	69, 70	ralprg 4625	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → (∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
72	71	3adant3 1128	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
73	72	adantr 483	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
74	68, 73	bitrd 281	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
75	42, 62, 74	3anbi123d 1432	. . . . . 6 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦)) ↔ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌)))))
76		ancom 463	. . . . . . . 8 ⊢ (((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋)))
77	76	3anbi2i 1154	. . . . . . 7 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
78		3an6 1442	. . . . . . 7 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
79		3anrot 1096	. . . . . . . . . 10 ⊢ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)))
80	79	bicomi 226	. . . . . . . . 9 ⊢ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
81		necom 3069	. . . . . . . . . 10 ⊢ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑋))
82		necom 3069	. . . . . . . . . 10 ⊢ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌))
83		necom 3069	. . . . . . . . . 10 ⊢ ((𝐹‘𝑍) ≠ (𝐹‘𝑌) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑍))
84	81, 82, 83	3anbi123i 1151	. . . . . . . . 9 ⊢ (((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌)) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
85	80, 84	anbi12i 628	. . . . . . . 8 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
86		anidm 567	. . . . . . . 8 ⊢ ((((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
87		3ancoma 1094	. . . . . . . . 9 ⊢ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
88		necom 3069	. . . . . . . . . 10 ⊢ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑍))
89	88	3anbi2i 1154	. . . . . . . . 9 ⊢ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
90	87, 89	bitri 277	. . . . . . . 8 ⊢ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
91	85, 86, 90	3bitri 299	. . . . . . 7 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
92	77, 78, 91	3bitri 299	. . . . . 6 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
93	75, 92	syl6bb 289	. . . . 5 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
94	20, 93	bitrd 281	. . . 4 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
95	3, 94	syl5bb 285	. . 3 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
96	95	anbi2d 630	. 2 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦)) ↔ (𝐹:𝐴⟶𝐵 ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))))
97	1, 96	syl5bb 285	1 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ≠ wne 3016 ∀wral 3138 ∖ cdif 3932 {csn 4560 {cpr 4562 {ctp 4564 ⟶wf 6345 –1-1→wf1 6346 ‘cfv 6349

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-br 5059 df-opab 5121 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fv 6357

This theorem is referenced by: f13idfv 13362 cyc3evpm 30787

W3C validator