Theorem f1fv 3871

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 groups:   x,y,A   x,F,y

Proof of Theorem f1fv

Step	Hyp	Ref	Expression
1		f11 3661	. 2 |- (F:A-1-1->B <-> (F:A-->B /\ A.zE*x xFz))
2		ffn 3624	. . . 4 |- (F:A-->B -> F Fn A)
3		fndm 3584	. . . . . . . . . . . . . . 15 |- (F Fn A -> dom F = A)
4	3	eleq2d 1540	. . . . . . . . . . . . . 14 |- (F Fn A -> (x e. dom F <-> x e. A))
5		visset 1811	. . . . . . . . . . . . . . 15 |- x e. V
6	5	breldm 3312	. . . . . . . . . . . . . 14 |- (xFz -> x e. dom F)
7	4, 6	syl5bi 208	. . . . . . . . . . . . 13 |- (F Fn A -> (xFz -> x e. A))
8	3	eleq2d 1540	. . . . . . . . . . . . . 14 |- (F Fn A -> (y e. dom F <-> y e. A))
9		visset 1811	. . . . . . . . . . . . . . 15 |- y e. V
10	9	breldm 3312	. . . . . . . . . . . . . 14 |- (yFz -> y e. dom F)
11	8, 10	syl5bi 208	. . . . . . . . . . . . 13 |- (F Fn A -> (yFz -> y e. A))
12	7, 11	anim12d 557	. . . . . . . . . . . 12 |- (F Fn A -> ((xFz /\ yFz) -> (x e. A /\ y e. A)))
13	12	pm4.71rd 638	. . . . . . . . . . 11 |- (F Fn A -> ((xFz /\ yFz) <-> ((x e. A /\ y e. A) /\ (xFz /\ yFz))))
14		visset 1811	. . . . . . . . . . . . . . . 16 |- z e. V
15	14	fnbrfvb 3750	. . . . . . . . . . . . . . 15 |- ((F Fn A /\ x e. A) -> ((F` x) = z <-> xFz))
16		eqcom 1476	. . . . . . . . . . . . . . 15 |- (z = (F` x) <-> (F` x) = z)
17	15, 16	syl5bb 531	. . . . . . . . . . . . . 14 |- ((F Fn A /\ x e. A) -> (z = (F` x) <-> xFz))
18	14	fnbrfvb 3750	. . . . . . . . . . . . . . 15 |- ((F Fn A /\ y e. A) -> ((F` y) = z <-> yFz))
19		eqcom 1476	. . . . . . . . . . . . . . 15 |- (z = (F` y) <-> (F` y) = z)
20	18, 19	syl5bb 531	. . . . . . . . . . . . . 14 |- ((F Fn A /\ y e. A) -> (z = (F` y) <-> yFz))
21	17, 20	bi2anan9 631	. . . . . . . . . . . . 13 |- (((F Fn A /\ x e. A) /\ (F Fn A /\ y e. A)) -> ((z = (F` x) /\ z = (F` y)) <-> (xFz /\ yFz)))
22	21	anandis 512	. . . . . . . . . . . 12 |- ((F Fn A /\ (x e. A /\ y e. A)) -> ((z = (F` x) /\ z = (F` y)) <-> (xFz /\ yFz)))
23	22	pm5.32da 648	. . . . . . . . . . 11 |- (F Fn A -> (((x e. A /\ y e. A) /\ (z = (F` x) /\ z = (F` y))) <-> ((x e. A /\ y e. A) /\ (xFz /\ yFz))))
24	13, 23	bitr4d 530	. . . . . . . . . 10 |- (F Fn A -> ((xFz /\ yFz) <-> ((x e. A /\ y e. A) /\ (z = (F` x) /\ z = (F` y)))))
25	24	imbi1d 612	. . . . . . . . 9 |- (F Fn A -> (((xFz /\ yFz) -> x = y) <-> (((x e. A /\ y e. A) /\ (z = (F` x) /\ z = (F` y))) -> x = y)))
26		impexp 347	. . . . . . . . 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)))
27	25, 26	syl6bb 535	. . . . . . . 8 |- (F Fn A -> (((xFz /\ yFz) -> x = y) <-> ((x e. A /\ y e. A) -> ((z = (F` x) /\ z = (F` y)) -> x = y))))
28	27	albidv 1278	. . . . . . 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))))
29		19.21v 1285	. . . . . . . 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)))
30		19.23v 1293	. . . . . . . . . 10 |- (A.z((z = (F` x) /\ z = (F` y)) -> x = y) <-> (E.z(z = (F` x) /\ z = (F` y)) -> x = y))
31		fvex 3729	. . . . . . . . . . . 12 |- (F` x) e. V
32	31	eqvinc 1881	. . . . . . . . . . 11 |- ((F` x) = (F` y) <-> E.z(z = (F` x) /\ z = (F` y)))
33	32	imbi1i 186	. . . . . . . . . 10 |- (((F` x) = (F` y) -> x = y) <-> (E.z(z = (F` x) /\ z = (F` y)) -> x = y))
34	30, 33	bitr4 176	. . . . . . . . 9 |- (A.z((z = (F` x) /\ z = (F` y)) -> x = y) <-> ((F` x) = (F` y) -> x = y))
35	34	imbi2i 185	. . . . . . . 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)))
36	29, 35	bitr 173	. . . . . . 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)))
37	28, 36	syl6bb 535	. . . . . 6 |- (F Fn A -> (A.z((xFz /\ yFz) -> x = y) <-> ((x e. A /\ y e. A) -> ((F` x) = (F` y) -> x = y))))
38	37	2albidv 1280	. . . . 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))))
39		breq1 2619	. . . . . . . 8 |- (x = y -> (xFz <-> yFz))
40	39	mo4 1403	. . . . . . 7 |- (E*x xFz <-> A.xA.y((xFz /\ yFz) -> x = y))
41	40	albii 998	. . . . . 6 |- (A.zE*x xFz <-> A.zA.xA.y((xFz /\ yFz) -> x = y))
42		alcom 1031	. . . . . 6 |- (A.zA.xA.y((xFz /\ yFz) -> x = y) <-> A.xA.zA.y((xFz /\ yFz) -> x = y))
43		alcom 1031	. . . . . . 7 |- (A.zA.y((xFz /\ yFz) -> x = y) <-> A.yA.z((xFz /\ yFz) -> x = y))
44	43	albii 998	. . . . . 6 |- (A.xA.zA.y((xFz /\ yFz) -> x = y) <-> A.xA.yA.z((xFz /\ yFz) -> x = y))
45	41, 42, 44	3bitr 177	. . . . 5 |- (A.zE*x xFz <-> A.xA.yA.z((xFz /\ yFz) -> x = y))
46		r2al 1675	. . . . 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)))
47	38, 45, 46	3bitr4g 554	. . . 4 |- (F Fn A -> (A.zE*x xFz <-> A.x e. A A.y e. A ((F` x) = (F` y) -> x = y)))
48	2, 47	syl 10	. . 3 |- (F:A-->B -> (A.zE*x xFz <-> A.x e. A A.y e. A ((F` x) = (F` y) -> x = y)))
49	48	pm5.32i 644	. 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)))
50	1, 49	bitr 173	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 3   <-> wb 146   /\ wa 223  A.wal 953   = wceq 955   e. wcel 957  E.wex 979  E*wmo 1381  A.wral 1644   class class class wbr 2616  dom cdm 3167   Fn wfn 3174  -->wf 3175  -1-1->wf1 3176  ` cfv 3179

This theorem is referenced by:  f1fvf 3872  f1fveq 3873  f1ofv 3874  tz7.48lem 3952  omsmo 4254  mapenlem2 4483  unfilem2 4538  inf3lem6 4605  alephiso 4879  om2uzf1o 6256  icoshftf1oi 6360  reeff1 7386  grplactf1o 8082  efif1 8716  eff1i 8728  pjmf1 9652  unopf1ot 9831  ghomf1olem 10387  homcard 10520  trnij 10588

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2700  ax-pow 2739  ax-pr 2776  ax-un 2863

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-ral 1648  df-rex 1649  df-v 1810  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-nul 2279  df-pw 2400  df-sn 2410  df-pr 2411  df-op 2414  df-uni 2501  df-br 2617  df-opab 2664  df-id