Theorem f1fv 3874

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 3664	. 2 |- (F:A-1-1->B <-> (F:A-->B /\ A.zE*x xFz))
2		ffn 3627	. . . 4 |- (F:A-->B -> F Fn A)
3		fndm 3587	. . . . . . . . . . . . . . 15 |- (F Fn A -> dom F = A)
4	3	eleq2d 1541	. . . . . . . . . . . . . 14 |- (F Fn A -> (x e. dom F <-> x e. A))
5		visset 1813	. . . . . . . . . . . . . . 15 |- x e. V
6	5	breldm 3315	. . . . . . . . . . . . . 14 |- (xFz -> x e. dom F)
7	4, 6	syl5bi 208	. . . . . . . . . . . . 13 |- (F Fn A -> (xFz -> x e. A))
8	3	eleq2d 1541	. . . . . . . . . . . . . 14 |- (F Fn A -> (y e. dom F <-> y e. A))
9		visset 1813	. . . . . . . . . . . . . . 15 |- y e. V
10	9	breldm 3315	. . . . . . . . . . . . . 14 |- (yFz -> y e. dom F)
11	8, 10	syl5bi 208	. . . . . . . . . . . . 13 |- (F Fn A -> (yFz -> y e. A))
12	7, 11	anim12d 558	. . . . . . . . . . . 12 |- (F Fn A -> ((xFz /\ yFz) -> (x e. A /\ y e. A)))
13	12	pm4.71rd 639	. . . . . . . . . . 11 |- (F Fn A -> ((xFz /\ yFz) <-> ((x e. A /\ y e. A) /\ (xFz /\ yFz))))
14		visset 1813	. . . . . . . . . . . . . . . 16 |- z e. V
15	14	fnbrfvb 3753	. . . . . . . . . . . . . . 15 |- ((F Fn A /\ x e. A) -> ((F` x) = z <-> xFz))
16		eqcom 1477	. . . . . . . . . . . . . . 15 |- (z = (F` x) <-> (F` x) = z)
17	15, 16	syl5bb 532	. . . . . . . . . . . . . 14 |- ((F Fn A /\ x e. A) -> (z = (F` x) <-> xFz))
18	14	fnbrfvb 3753	. . . . . . . . . . . . . . 15 |- ((F Fn A /\ y e. A) -> ((F` y) = z <-> yFz))
19		eqcom 1477	. . . . . . . . . . . . . . 15 |- (z = (F` y) <-> (F` y) = z)
20	18, 19	syl5bb 532	. . . . . . . . . . . . . 14 |- ((F Fn A /\ y e. A) -> (z = (F` y) <-> yFz))
21	17, 20	bi2anan9 632	. . . . . . . . . . . . 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 649	. . . . . . . . . . 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 531	. . . . . . . . . 10 |- (F Fn A -> ((xFz /\ yFz) <-> ((x e. A /\ y e. A) /\ (z = (F` x) /\ z = (F` y)))))
25	24	imbi1d 613	. . . . . . . . 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 536	. . . . . . . 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 3732	. . . . . . . . . . . 12 |- (F` x) e. V
32	31	eqvinc 1883	. . . . . . . . . . 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 536	. . . . . 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 2622	. . . . . . . 8 |- (x = y -> (xFz <-> yFz))
40	39	mo4 1403	. . . . . . 7 |- (E*x xFz <-> A.xA.y((xFz /\ yFz) -> x = y))
41	40	albii 999	. . . . . 6 |- (A.zE*x xFz <-> A.zA.xA.y((xFz /\ yFz) -> x = y))
42		alcom 1032	. . . . . 6 |- (A.zA.xA.y((xFz /\ yFz) -> x = y) <-> A.xA.zA.y((xFz /\ yFz) -> x = y))
43		alcom 1032	. . . . . . 7 |- (A.zA.y((xFz /\ yFz) -> x = y) <-> A.yA.z((xFz /\ yFz) -> x = y))
44	43	albii 999	. . . . . 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 1676	. . . . 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 555	. . . 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 645	. 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 954   = wceq 956   e. wcel 958  E.wex 980  E*wmo 1381  A.wral 1645   class class class wbr 2619  dom cdm 3170   Fn wfn 3177  -->wf 3178  -1-1->wf1 3179  ` cfv 3182

This theorem is referenced by:  f1fvf 3875  f1fveq 3876  f1ofv 3877  tz7.48lem 3955  omsmo 4257  mapenlem2 4490  unfilem2 4549  inf3lem6 4618  alephiso 4892  om2uzf1o 6301  icoshftf1oi 6409  reeff1 7410  grplactf1o 8098  efif1 8737  eff1i 8744  pjmf1 9661  unopf1ot 9840  ghomf1olem 10396  homcard 10539  trnij 10637

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab