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 7294

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 7291	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦)))
2		f13dfv.a	. . . . 5 ⊢ 𝐴 = {𝑋, 𝑌, 𝑍}
3	2	raleqi 3324	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦))
4		sneq 4636	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋})
5	4	difeq2d 4126	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑋}))
6		fveq2 6906	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋))
7	6	neeq1d 3000	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑦)))
8	5, 7	raleqbidv 3346	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦)))
9		sneq 4636	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → {𝑥} = {𝑌})
10	9	difeq2d 4126	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑌}))
11		fveq2 6906	. . . . . . . . 9 ⊢ (𝑥 = 𝑌 → (𝐹‘𝑥) = (𝐹‘𝑌))
12	11	neeq1d 3000	. . . . . . . 8 ⊢ (𝑥 = 𝑌 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑦)))
13	10, 12	raleqbidv 3346	. . . . . . 7 ⊢ (𝑥 = 𝑌 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦)))
14		sneq 4636	. . . . . . . . 9 ⊢ (𝑥 = 𝑍 → {𝑥} = {𝑍})
15	14	difeq2d 4126	. . . . . . . 8 ⊢ (𝑥 = 𝑍 → (𝐴 ∖ {𝑥}) = (𝐴 ∖ {𝑍}))
16		fveq2 6906	. . . . . . . . 9 ⊢ (𝑥 = 𝑍 → (𝐹‘𝑥) = (𝐹‘𝑍))
17	16	neeq1d 3000	. . . . . . . 8 ⊢ (𝑥 = 𝑍 → ((𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑦)))
18	15, 17	raleqbidv 3346	. . . . . . 7 ⊢ (𝑥 = 𝑍 → (∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦)))
19	8, 13, 18	raltpg 4698	. . . . . 6 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦))))
20	19	adantr 480	. . . . 5 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑥 ∈ {𝑋, 𝑌, 𝑍}∀𝑦 ∈ (𝐴 ∖ {𝑥})(𝐹‘𝑥) ≠ (𝐹‘𝑦) ↔ (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦))))
21	2	difeq1i 4122	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑋}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑋})
22		tprot 4749	. . . . . . . . . . . . 13 ⊢ {𝑋, 𝑌, 𝑍} = {𝑌, 𝑍, 𝑋}
23	22	difeq1i 4122	. . . . . . . . . . . 12 ⊢ ({𝑋, 𝑌, 𝑍} ∖ {𝑋}) = ({𝑌, 𝑍, 𝑋} ∖ {𝑋})
24		necom 2994	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ≠ 𝑌 ↔ 𝑌 ≠ 𝑋)
25		necom 2994	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ≠ 𝑍 ↔ 𝑍 ≠ 𝑋)
26	24, 25	anbi12i 628	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍) ↔ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋))
27	26	biimpi 216	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍) → (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋))
28	27	3adant3 1133	. . . . . . . . . . . . 13 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋))
29		diftpsn3 4802	. . . . . . . . . . . . 13 ⊢ ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → ({𝑌, 𝑍, 𝑋} ∖ {𝑋}) = {𝑌, 𝑍})
30	28, 29	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑌, 𝑍, 𝑋} ∖ {𝑋}) = {𝑌, 𝑍})
31	23, 30	eqtrid 2789	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑋}) = {𝑌, 𝑍})
32	21, 31	eqtrid 2789	. . . . . . . . . 10 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑋}) = {𝑌, 𝑍})
33	32	adantl 481	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑋}) = {𝑌, 𝑍})
34	33	raleqdv 3326	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦)))
35		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌))
36	35	neeq2d 3001	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌)))
37		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑍 → (𝐹‘𝑦) = (𝐹‘𝑍))
38	37	neeq2d 3001	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑍 → ((𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑍)))
39	36, 38	ralprg 4696	. . . . . . . . . 10 ⊢ ((𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
40	39	3adant1 1131	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
41	40	adantr 480	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ {𝑌, 𝑍} (𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
42	34, 41	bitrd 279	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑋})(𝐹‘𝑋) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍))))
43	2	difeq1i 4122	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑌}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑌})
44		tpcomb 4751	. . . . . . . . . . . . 13 ⊢ {𝑋, 𝑌, 𝑍} = {𝑋, 𝑍, 𝑌}
45	44	difeq1i 4122	. . . . . . . . . . . 12 ⊢ ({𝑋, 𝑌, 𝑍} ∖ {𝑌}) = ({𝑋, 𝑍, 𝑌} ∖ {𝑌})
46		necom 2994	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ≠ 𝑍 ↔ 𝑍 ≠ 𝑌)
47	46	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ≠ 𝑍 → 𝑍 ≠ 𝑌)
48	47	anim2i 617	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑌 ≠ 𝑍) → (𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌))
49	48	3adant2 1132	. . . . . . . . . . . . 13 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌))
50		diftpsn3 4802	. . . . . . . . . . . . 13 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑍 ≠ 𝑌) → ({𝑋, 𝑍, 𝑌} ∖ {𝑌}) = {𝑋, 𝑍})
51	49, 50	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑍, 𝑌} ∖ {𝑌}) = {𝑋, 𝑍})
52	45, 51	eqtrid 2789	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑌}) = {𝑋, 𝑍})
53	43, 52	eqtrid 2789	. . . . . . . . . 10 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑌}) = {𝑋, 𝑍})
54	53	adantl 481	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑌}) = {𝑋, 𝑍})
55	54	raleqdv 3326	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦)))
56		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑋 → (𝐹‘𝑦) = (𝐹‘𝑋))
57	56	neeq2d 3001	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑋)))
58	37	neeq2d 3001	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑍 → ((𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
59	57, 58	ralprg 4696	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
60	59	3adant2 1132	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
61	60	adantr 480	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ {𝑋, 𝑍} (𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
62	55, 61	bitrd 279	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑌})(𝐹‘𝑌) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
63	2	difeq1i 4122	. . . . . . . . . . 11 ⊢ (𝐴 ∖ {𝑍}) = ({𝑋, 𝑌, 𝑍} ∖ {𝑍})
64		diftpsn3 4802	. . . . . . . . . . . 12 ⊢ ((𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑍}) = {𝑋, 𝑌})
65	64	3adant1 1131	. . . . . . . . . . 11 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌, 𝑍} ∖ {𝑍}) = {𝑋, 𝑌})
66	63, 65	eqtrid 2789	. . . . . . . . . 10 ⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → (𝐴 ∖ {𝑍}) = {𝑋, 𝑌})
67	66	adantl 481	. . . . . . . . 9 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐴 ∖ {𝑍}) = {𝑋, 𝑌})
68	67	raleqdv 3326	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (∀𝑦 ∈ (𝐴 ∖ {𝑍})(𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦)))
69	56	neeq2d 3001	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑋 → ((𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑋)))
70	35	neeq2d 3001	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑌 → ((𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑌)))
71	69, 70	ralprg 4696	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) → (∀𝑦 ∈ {𝑋, 𝑌} (𝐹‘𝑍) ≠ (𝐹‘𝑦) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
72	71	3adant3 1133	. . . . . . . . 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 1159	. . . . . . 7 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
78		3an6 1448	. . . . . . 7 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))))
79		3anrot 1100	. . . . . . . . . 10 ⊢ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)))
80	79	bicomi 224	. . . . . . . . 9 ⊢ (((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
81		necom 2994	. . . . . . . . . 10 ⊢ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ↔ (𝐹‘𝑍) ≠ (𝐹‘𝑋))
82		necom 2994	. . . . . . . . . 10 ⊢ ((𝐹‘𝑌) ≠ (𝐹‘𝑋) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑌))
83		necom 2994	. . . . . . . . . 10 ⊢ ((𝐹‘𝑍) ≠ (𝐹‘𝑌) ↔ (𝐹‘𝑌) ≠ (𝐹‘𝑍))
84	81, 82, 83	3anbi123i 1156	. . . . . . . . 9 ⊢ (((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌)) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
85	80, 84	anbi12i 628	. . . . . . . 8 ⊢ ((((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋)) ∧ ((𝐹‘𝑋) ≠ (𝐹‘𝑍) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑌))) ↔ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))))
86		anidm 564	. . . . . . . 8 ⊢ ((((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ∧ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍))) ↔ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
87		3ancoma 1098	. . . . . . . . 9 ⊢ (((𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)) ↔ ((𝐹‘𝑋) ≠ (𝐹‘𝑌) ∧ (𝐹‘𝑍) ≠ (𝐹‘𝑋) ∧ (𝐹‘𝑌) ≠ (𝐹‘𝑍)))
88		necom 2994	. . . . . . . . . 10 ⊢ ((𝐹‘𝑍) ≠ (𝐹‘𝑋) ↔ (𝐹‘𝑋) ≠ (𝐹‘𝑍))
89	88	3anbi2i 1159	. . . . . . . . 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 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∖ cdif 3948 {csn 4626 {cpr 4628 {ctp 4630 ⟶wf 6557 –1-1→wf1 6558 ‘cfv 6561

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fv 6569

This theorem is referenced by: f13idfv 14041 cyc3evpm 33170

W3C validator