Theorem f1fv 2916

Description: A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43.

Assertion

Ref	Expression
f1fv	|- (F:A-1-1->B <-> (F:A-->B /\ A.x e. A A.y e. A ((F` x) = (F` y) -> x = y)))

Distinct variable group(s):   x,y,A   x,B,y   x,F,y

Proof of Theorem f1fv

Step	Hyp	Ref	Expression
1		f11 2780	. 2 |- (F:A-1-1->B <-> (F:A-->B /\ A.zE*x xFz))
2		ffn 2752	. . . 4 |- (F:A-->B -> F Fn A)
3		fndm 2723	. . . . . . . . . . . . . . . 16 |- (F Fn A -> dom F = A)
4	3	eleq2d 1156	. . . . . . . . . . . . . . 15 |- (F Fn A -> (x e. dom F <-> x e. A))
5		visset 1350	. . . . . . . . . . . . . . . 16 |- x e. V
6	5	breldm 2535	. . . . . . . . . . . . . . 15 |- (xFz -> x e. dom F)
7	4, 6	syl5bi 183	. . . . . . . . . . . . . 14 |- (F Fn A -> (xFz -> x e. A))
8	3	eleq2d 1156	. . . . . . . . . . . . . . 15 |- (F Fn A -> (y e. dom F <-> y e. A))
9		visset 1350	. . . . . . . . . . . . . . . 16 |- y e. V
10	9	breldm 2535	. . . . . . . . . . . . . . 15 |- (yFz -> y e. dom F)
11	8, 10	syl5bi 183	. . . . . . . . . . . . . 14 |- (F Fn A -> (yFz -> y e. A))
12	7, 11	anim12d 431	. . . . . . . . . . . . 13 |- (F Fn A -> ((xFz /\ yFz) -> (x e. A /\ y e. A)))
13	12	ancrd 247	. . . . . . . . . . . 12 |- (F Fn A -> ((xFz /\ yFz) -> ((x e. A /\ y e. A) /\ (xFz /\ yFz))))
14		pm3.27 260	. . . . . . . . . . . . 13 |- (((x e. A /\ y e. A) /\ (xFz /\ yFz)) -> (xFz /\ yFz))
15	14	a1i 7	. . . . . . . . . . . 12 |- (F Fn A -> (((x e. A /\ y e. A) /\ (xFz /\ yFz)) -> (xFz /\ yFz)))
16	13, 15	impbid 397	. . . . . . . . . . 11 |- (F Fn A -> ((xFz /\ yFz) <-> ((x e. A /\ y e. A) /\ (xFz /\ yFz))))
17		visset 1350	. . . . . . . . . . . . . . . . 17 |- z e. V
18	17	fnfvbr 2855	. . . . . . . . . . . . . . . 16 |- ((F Fn A /\ x e. A) -> ((F` x) = z <-> xFz))
19		cleqcom 1103	. . . . . . . . . . . . . . . 16 |- (z = (F` x) <-> (F` x) = z)
20	18, 19	syl5bb 410	. . . . . . . . . . . . . . 15 |- ((F Fn A /\ x e. A) -> (z = (F` x) <-> xFz))
21	17	fnfvbr 2855	. . . . . . . . . . . . . . . 16 |- ((F Fn A /\ y e. A) -> ((F` y) = z <-> yFz))
22		cleqcom 1103	. . . . . . . . . . . . . . . 16 |- (z = (F` y) <-> (F` y) = z)
23	21, 22	syl5bb 410	. . . . . . . . . . . . . . 15 |- ((F Fn A /\ y e. A) -> (z = (F` y) <-> yFz))
24	20, 23	bi2anan9 478	. . . . . . . . . . . . . 14 |- (((F Fn A /\ x e. A) /\ (F Fn A /\ y e. A)) -> ((z = (F` x) /\ z = (F` y)) <-> (xFz /\ yFz)))
25	24	anandis 394	. . . . . . . . . . . . 13 |- ((F Fn A /\ (x e. A /\ y e. A)) -> ((z = (F` x) /\ z = (F` y)) <-> (xFz /\ yFz)))
26	25	exp 291	. . . . . . . . . . . 12 |- (F Fn A -> ((x e. A /\ y e. A) -> ((z = (F` x) /\ z = (F` y)) <-> (xFz /\ yFz))))
27	26	pm5.32d 491	. . . . . . . . . . 11 |- (F Fn A -> (((x e. A /\ y e. A) /\ (z = (F` x) /\ z = (F` y))) <-> ((x e. A /\ y e. A) /\ (xFz /\ yFz))))
28	16, 27	bitr4d 409	. . . . . . . . . 10 |- (F Fn A -> ((xFz /\ yFz) <-> ((x e. A /\ y e. A) /\ (z = (F` x) /\ z = (F` y)))))
29	28	imbi1d 465	. . . . . . . . 9 |- (F Fn A -> (((xFz /\ yFz) -> x = y) <-> (((x e. A /\ y e. A) /\ (z = (F` x) /\ z = (F` y))) -> x = y)))
30		impexp 276	. . . . . . . . 9 |- ((((x e. A /\ y e. A) /\ (z = (F` x) /\ z = (F` y))) -> x = y) <-> ((x e. A /\ y e. A) -> ((z = (F` x) /\ z = (F` y)) -> x = y)))
31	29, 30	syl6bb 414	. . . . . . . 8 |- (F Fn A -> (((xFz /\ yFz) -> x = y) <-> ((x e. A /\ y e. A) -> ((z = (F` x) /\ z = (F` y)) -> x = y))))
32	31	bialdv 935	. . . . . . 7 |- (F Fn A -> (A.z((xFz /\ yFz) -> x = y) <-> A.z((x e. A /\ y e. A) -> ((z = (F` x) /\ z = (F` y)) -> x = y))))
33		19.21v 942	. . . . . . . 8 |- (A.z((x e. A /\ y e. A) -> ((z = (F` x) /\ z = (F` y)) -> x = y)) <-> ((x e. A /\ y e. A) -> A.z((z = (F` x) /\ z = (F` y)) -> x = y)))
34		19.23v 950	. . . . . . . . . 10 |- (A.z((z = (F` x) /\ z = (F` y)) -> x = y) <-> (E.z(z = (F` x) /\ z = (F` y)) -> x = y))
35		fvex 2838	. . . . . . . . . . . 12 |- (F` x) e. V
36	35	eqvinc 1407	. . . . . . . . . . 11 |- ((F` x) = (F` y) <-> E.z(z = (F` x) /\ z = (F` y)))
37	36	imbi1i 161	. . . . . . . . . 10 |- (((F` x) = (F` y) -> x = y) <-> (E.z(z = (F` x) /\ z = (F` y)) -> x = y))
38	34, 37	bitr4 154	. . . . . . . . 9 |- (A.z((z = (F` x) /\ z = (F` y)) -> x = y) <-> ((F` x) = (F` y) -> x = y))
39	38	imbi2i 160	. . . . . . . 8 |- (((x e. A /\ y e. A) -> A.z((z = (F` x) /\ z = (F` y)) -> x = y)) <-> ((x e. A /\ y e. A) -> ((F` x) = (F` y) -> x = y)))
40	33, 39	bitr 151	. . . . . . 7 |- (A.z((x e. A /\ y e. A) -> ((z = (F` x) /\ z = (F` y)) -> x = y)) <-> ((x e. A /\ y e. A) -> ((F` x) = (F` y) -> x = y)))
41	32, 40	syl6bb 414	. . . . . 6 |- (F Fn A -> (A.z((xFz /\ yFz) -> x = y) <-> ((x e. A /\ y e. A) -> ((F` x) = (F` y) -> x = y))))
42	41	bi2aldv 937	. . . . 5 |- (F Fn A -> (A.xA.yA.z((xFz /\ yFz) -> x = y) <-> A.xA.y((x e. A /\ y e. A) -> ((F` x) = (F` y) -> x = y))))
43		breq1 2065	. . . . . . . 8 |- (x = y -> (xFz <-> yFz))
44	43	mo4 1029	. . . . . . 7 |- (E*x xFz <-> A.xA.y((xFz /\ yFz) -> x = y))
45	44	bial 695	. . . . . 6 |- (A.zE*x xFz <-> A.zA.xA.y((xFz /\ yFz) -> x = y))
46		alcom 715	. . . . . 6 |- (A.zA.xA.y((xFz /\ yFz) -> x = y) <-> A.xA.zA.y((xFz /\ yFz) -> x = y))
47		alcom 715	. . . . . . 7 |- (A.zA.y((xFz /\ yFz) -> x = y) <-> A.yA.z((xFz /\ yFz) -> x = y))
48	47	bial 695	. . . . . 6 |- (A.xA.zA.y((xFz /\ yFz) -> x = y) <-> A.xA.yA.z((xFz /\ yFz) -> x = y))
49	45, 46, 48	3bitr 155	. . . . 5 |- (A.zE*x xFz <-> A.xA.yA.z((xFz /\ yFz) -> x = y))
50		r2al 1231	. . . . 5 |- (A.x e. A A.y e. A ((F` x) = (F` y) -> x = y) <-> A.xA.y((x e. A /\ y e. A) -> ((F` x) = (F` y) -> x = y)))
51	42, 49, 50	3bitr4g 428	. . . 4 |- (F Fn A -> (A.zE*x xFz <-> A.x e. A A.y e. A ((F` x) = (F` y) -> x = y)))
52	2, 51	syl 12	. . 3 |- (F:A-->B -> (A.zE*x xFz <-> A.x e. A A.y e. A ((F` x) = (F` y) -> x = y)))
53	52	pm5.32i 489	. 2 |- ((F:A-->B /\ A.zE*x xFz) <-> (F:A-->B /\ A.x e. A A.y e. A ((F` x) = (F` y) -> x = y)))
54	1, 53	bitr 151	1 |- (F:A-1-1->B <-> (F:A-->B /\ A.x e. A A.y e. A ((F` x) = (F` y) -> x = y)))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196  A.wal 672  E.wex 678   = weq 797  E*wmo 1008   = wceq 1091   e. wcel 1092  A.wral 1201   class class class wbr 2054  dom cdm 2410   Fn wfn 2417  -->wf 2418  -1-1->wf1 2419  ` cfv</