Theorem dff13 5350

Description: A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43. (Contributed by NM, 29-Oct-1996.)

Assertion

Ref	Expression
dff13	|- ( 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

Allowed substitution hints:   B(x,y)

Proof of Theorem dff13

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dff12 5034	. 2 |- ( F :A -1-1->B <-> ( F :A -->B /\ A.zE*x x Fz))
2		ffn 4989	. . . 4 |- ( F :A -->B -> F Fn A)
3		vex 2554	. . . . . . . . . . . . . . 15 |- x e. _V
4		vex 2554	. . . . . . . . . . . . . . 15 |- z e. _V
5	3, 4	breldm 4482	. . . . . . . . . . . . . 14 |- (x Fz -> x e. dom F)
6		fndm 4941	. . . . . . . . . . . . . . 15 |- ( F Fn A -> dom F = A)
7	6	eleq2d 2104	. . . . . . . . . . . . . 14 |- ( F Fn A -> (x e. dom F <-> x e. A))
8	5, 7	syl5ib 143	. . . . . . . . . . . . 13 |- ( F Fn A -> (x Fz -> x e. A))
9		vex 2554	. . . . . . . . . . . . . . 15 |- y e. _V
10	9, 4	breldm 4482	. . . . . . . . . . . . . 14 |- (y Fz -> y e. dom F)
11	6	eleq2d 2104	. . . . . . . . . . . . . 14 |- ( F Fn A -> (y e. dom F <-> y e. A))
12	10, 11	syl5ib 143	. . . . . . . . . . . . 13 |- ( F Fn A -> (y Fz -> y e. A))
13	8, 12	anim12d 318	. . . . . . . . . . . 12 |- ( F Fn A -> ((x Fz /\ y Fz) -> (x e. A /\ y e. A)))
14	13	pm4.71rd 374	. . . . . . . . . . 11 |- ( F Fn A -> ((x Fz /\ y Fz) <-> ((x e. A /\ y e. A) /\ (x Fz /\ y Fz))))
15		eqcom 2039	. . . . . . . . . . . . . . 15 |- (z = ( F ` x) <-> ( F ` x) = z)
16		fnbrfvb 5157	. . . . . . . . . . . . . . 15 |- (( F Fn A /\ x e. A) -> (( F ` x) = z <-> x Fz))
17	15, 16	syl5bb 181	. . . . . . . . . . . . . 14 |- (( F Fn A /\ x e. A) -> (z = ( F ` x) <-> x Fz))
18		eqcom 2039	. . . . . . . . . . . . . . 15 |- (z = ( F ` y) <-> ( F ` y) = z)
19		fnbrfvb 5157	. . . . . . . . . . . . . . 15 |- (( F Fn A /\ y e. A) -> (( F ` y) = z <-> y Fz))
20	18, 19	syl5bb 181	. . . . . . . . . . . . . 14 |- (( F Fn A /\ y e. A) -> (z = ( F ` y) <-> y Fz))
21	17, 20	bi2anan9 538	. . . . . . . . . . . . 13 |- ((( F Fn A /\ x e. A) /\ ( F Fn A /\ y e. A)) -> ((z = ( F ` x) /\ z = ( F ` y)) <-> (x Fz /\ y Fz)))
22	21	anandis 526	. . . . . . . . . . . 12 |- (( F Fn A /\ (x e. A /\ y e. A)) -> ((z = ( F ` x) /\ z = ( F ` y)) <-> (x Fz /\ y Fz)))
23	22	pm5.32da 425	. . . . . . . . . . 11 |- ( F Fn A -> (((x e. A /\ y e. A) /\ (z = ( F ` x) /\ z = ( F ` y))) <-> ((x e. A /\ y e. A) /\ (x Fz /\ y Fz))))
24	14, 23	bitr4d 180	. . . . . . . . . 10 |- ( F Fn A -> ((x Fz /\ y Fz) <-> ((x e. A /\ y e. A) /\ (z = ( F ` x) /\ z = ( F ` y)))))
25	24	imbi1d 220	. . . . . . . . 9 |- ( F Fn A -> (((x Fz /\ y Fz) -> x = y) <-> (((x e. A /\ y e. A) /\ (z = ( F ` x) /\ z = ( F ` y))) -> x = y)))
26		impexp 250	. . . . . . . . 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 185	. . . . . . . 8 |- ( F Fn A -> (((x Fz /\ y Fz) -> x = y) <-> ((x e. A /\ y e. A) -> ((z = ( F ` x) /\ z = ( F ` y)) -> x = y))))
28	27	albidv 1702	. . . . . . 7 |- ( F Fn A -> (A.z((x Fz /\ y Fz) -> x = y) <-> A.z((x e. A /\ y e. A) -> ((z = ( F ` x) /\ z = ( F ` y)) -> x = y))))
29		19.21v 1750	. . . . . . . 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		funfvex 5135	. . . . . . . . . . . . . 14 |- (( Fun F /\ x e. dom F) -> ( F ` x) e. _V)
31	30	funfni 4942	. . . . . . . . . . . . 13 |- (( F Fn A /\ x e. A) -> ( F ` x) e. _V)
32		eqvincg 2662	. . . . . . . . . . . . 13 |- (( F ` x) e. _V -> (( F ` x) = ( F ` y) <-> E.z(z = ( F ` x) /\ z = ( F ` y))))
33	31, 32	syl 14	. . . . . . . . . . . 12 |- (( F Fn A /\ x e. A) -> (( F ` x) = ( F ` y) <-> E.z(z = ( F ` x) /\ z = ( F ` y))))
34	33	imbi1d 220	. . . . . . . . . . 11 |- (( F Fn A /\ x e. A) -> ((( F ` x) = ( F ` y) -> x = y) <-> (E.z(z = ( F ` x) /\ z = ( F ` y)) -> x = y)))
35		19.23v 1760	. . . . . . . . . . 11 |- (A.z((z = ( F ` x) /\ z = ( F ` y)) -> x = y) <-> (E.z(z = ( F ` x) /\ z = ( F ` y)) -> x = y))
36	34, 35	syl6rbbr 188	. . . . . . . . . 10 |- (( F Fn A /\ x e. A) -> (A.z((z = ( F ` x) /\ z = ( F ` y)) -> x = y) <-> (( F ` x) = ( F ` y) -> x = y)))
37	36	adantrr 448	. . . . . . . . 9 |- (( F Fn A /\ (x e. A /\ y e. A)) -> (A.z((z = ( F ` x) /\ z = ( F ` y)) -> x = y) <-> (( F ` x) = ( F ` y) -> x = y)))
38	37	pm5.74da 417	. . . . . . . 8 |- ( F Fn A -> (((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))))
39	29, 38	syl5bb 181	. . . . . . 7 |- ( F Fn A -> (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))))
40	28, 39	bitrd 177	. . . . . 6 |- ( F Fn A -> (A.z((x Fz /\ y Fz) -> x = y) <-> ((x e. A /\ y e. A) -> (( F ` x) = ( F ` y) -> x = y))))
41	40	2albidv 1744	. . . . 5 |- ( F Fn A -> (A.xA.yA.z((x Fz /\ y Fz) -> x = y) <-> A.xA.y((x e. A /\ y e. A) -> (( F ` x) = ( F ` y) -> x = y))))
42		breq1 3758	. . . . . . . 8 |- (x = y -> (x Fz <-> y Fz))
43	42	mo4 1958	. . . . . . 7 |- (E*x x Fz <-> A.xA.y((x Fz /\ y Fz) -> x = y))
44	43	albii 1356	. . . . . 6 |- (A.zE*x x Fz <-> A.zA.xA.y((x Fz /\ y Fz) -> x = y))
45		alrot3 1371	. . . . . 6 |- (A.zA.xA.y((x Fz /\ y Fz) -> x = y) <-> A.xA.yA.z((x Fz /\ y Fz) -> x = y))
46	44, 45	bitri 173	. . . . 5 |- (A.zE*x x Fz <-> A.xA.yA.z((x Fz /\ y Fz) -> x = y))
47		r2al 2337	. . . . 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)))
48	41, 46, 47	3bitr4g 212	. . . 4 |- ( F Fn A -> (A.zE*x x Fz <-> A.x e. A A.y e. A (( F ` x) = ( F ` y) -> x = y)))
49	2, 48	syl 14	. . 3 |- ( F :A -->B -> (A.zE*x x Fz <-> A.x e. A A.y e. A (( F ` x) = ( F ` y) -> x = y)))
50	49	pm5.32i 427	. 2 |- (( F :A -->B /\ A.zE*x x Fz) <-> ( F :A -->B /\ A.x e. A A.y e. A (( F ` x) = ( F ` y) -> x = y)))
51	1, 50	bitri 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 4   /\ wa 97   <-> wb 98  A.wal 1240   = wceq 1242  E.wex 1378   e. wcel 1390  E*wmo 1898  A.wral 2300   _Vcvv 2551   class class class wbr 3755   dom cdm 4288   Fn wfn 4840   -->wf 4841   -1-1->wf1 4842   ` cfv 4845

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fv 4853

This theorem is referenced by:  f1veqaeq  5351  dff13f  5352  dff1o6  5359  fcof1  5366  f1o2ndf1  5791  cnref1o  8357  frec2uzf1od  8873