Theorem dff13 6512

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 6100	. 2 |- ( F : A -1-1-> B <-> ( F : A --> B /\ A. z E* x x F z ) )
2		ffn 6045	. . . 4 |- ( F : A --> B -> F Fn A )
3		vex 3203	. . . . . . . . . . . . . . 15 |- x e. _V
4		vex 3203	. . . . . . . . . . . . . . 15 |- z e. _V
5	3, 4	breldm 5329	. . . . . . . . . . . . . 14 |- ( x F z -> x e. dom F )
6		fndm 5990	. . . . . . . . . . . . . . 15 |- ( F Fn A -> dom F = A )
7	6	eleq2d 2687	. . . . . . . . . . . . . 14 |- ( F Fn A -> ( x e. dom F <-> x e. A ) )
8	5, 7	syl5ib 234	. . . . . . . . . . . . 13 |- ( F Fn A -> ( x F z -> x e. A ) )
9		vex 3203	. . . . . . . . . . . . . . 15 |- y e. _V
10	9, 4	breldm 5329	. . . . . . . . . . . . . 14 |- ( y F z -> y e. dom F )
11	6	eleq2d 2687	. . . . . . . . . . . . . 14 |- ( F Fn A -> ( y e. dom F <-> y e. A ) )
12	10, 11	syl5ib 234	. . . . . . . . . . . . 13 |- ( F Fn A -> ( y F z -> y e. A ) )
13	8, 12	anim12d 586	. . . . . . . . . . . 12 |- ( F Fn A -> ( ( x F z /\ y F z ) -> ( x e. A /\ y e. A ) ) )
14	13	pm4.71rd 667	. . . . . . . . . . 11 |- ( F Fn A -> ( ( x F z /\ y F z ) <-> ( ( x e. A /\ y e. A ) /\ ( x F z /\ y F z ) ) ) )
15		eqcom 2629	. . . . . . . . . . . . . . 15 |- ( z = ( F ` x ) <-> ( F ` x ) = z )
16		fnbrfvb 6236	. . . . . . . . . . . . . . 15 |- ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = z <-> x F z ) )
17	15, 16	syl5bb 272	. . . . . . . . . . . . . 14 |- ( ( F Fn A /\ x e. A ) -> ( z = ( F ` x ) <-> x F z ) )
18		eqcom 2629	. . . . . . . . . . . . . . 15 |- ( z = ( F ` y ) <-> ( F ` y ) = z )
19		fnbrfvb 6236	. . . . . . . . . . . . . . 15 |- ( ( F Fn A /\ y e. A ) -> ( ( F ` y ) = z <-> y F z ) )
20	18, 19	syl5bb 272	. . . . . . . . . . . . . 14 |- ( ( F Fn A /\ y e. A ) -> ( z = ( F ` y ) <-> y F z ) )
21	17, 20	bi2anan9 917	. . . . . . . . . . . . 13 |- ( ( ( F Fn A /\ x e. A ) /\ ( F Fn A /\ y e. A ) ) -> ( ( z = ( F ` x ) /\ z = ( F ` y ) ) <-> ( x F z /\ y F z ) ) )
22	21	anandis 873	. . . . . . . . . . . 12 |- ( ( F Fn A /\ ( x e. A /\ y e. A ) ) -> ( ( z = ( F ` x ) /\ z = ( F ` y ) ) <-> ( x F z /\ y F z ) ) )
23	22	pm5.32da 673	. . . . . . . . . . 11 |- ( F Fn A -> ( ( ( x e. A /\ y e. A ) /\ ( z = ( F ` x ) /\ z = ( F ` y ) ) ) <-> ( ( x e. A /\ y e. A ) /\ ( x F z /\ y F z ) ) ) )
24	14, 23	bitr4d 271	. . . . . . . . . 10 |- ( F Fn A -> ( ( x F z /\ y F z ) <-> ( ( x e. A /\ y e. A ) /\ ( z = ( F ` x ) /\ z = ( F ` y ) ) ) ) )
25	24	imbi1d 331	. . . . . . . . 9 |- ( F Fn A -> ( ( ( x F z /\ y F z ) -> x = y ) <-> ( ( ( x e. A /\ y e. A ) /\ ( z = ( F ` x ) /\ z = ( F ` y ) ) ) -> x = y ) ) )
26		impexp 462	. . . . . . . . 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 276	. . . . . . . 8 |- ( F Fn A -> ( ( ( x F z /\ y F z ) -> x = y ) <-> ( ( x e. A /\ y e. A ) -> ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) ) ) )
28	27	albidv 1849	. . . . . . 7 |- ( F Fn A -> ( A. z ( ( x F z /\ y F z ) -> x = y ) <-> A. z ( ( x e. A /\ y e. A ) -> ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) ) ) )
29		19.21v 1868	. . . . . . . 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 1902	. . . . . . . . . 10 |- ( A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) <-> ( E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) )
31		fvex 6201	. . . . . . . . . . . 12 |- ( F ` x ) e. _V
32	31	eqvinc 3330	. . . . . . . . . . 11 |- ( ( F ` x ) = ( F ` y ) <-> E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) )
33	32	imbi1i 339	. . . . . . . . . 10 |- ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) )
34	30, 33	bitr4i 267	. . . . . . . . 9 |- ( A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) <-> ( ( F ` x ) = ( F ` y ) -> x = y ) )
35	34	imbi2i 326	. . . . . . . 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	bitri 264	. . . . . . 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 276	. . . . . 6 |- ( F Fn A -> ( A. z ( ( x F z /\ y F z ) -> x = y ) <-> ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) )
38	37	2albidv 1851	. . . . 5 |- ( F Fn A -> ( A. x A. y A. z ( ( x F z /\ y F z ) -> x = y ) <-> A. x A. y ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) )
39		breq1 4656	. . . . . . . 8 |- ( x = y -> ( x F z <-> y F z ) )
40	39	mo4 2517	. . . . . . 7 |- ( E* x x F z <-> A. x A. y ( ( x F z /\ y F z ) -> x = y ) )
41	40	albii 1747	. . . . . 6 |- ( A. z E* x x F z <-> A. z A. x A. y ( ( x F z /\ y F z ) -> x = y ) )
42		alrot3 2038	. . . . . 6 |- ( A. z A. x A. y ( ( x F z /\ y F z ) -> x = y ) <-> A. x A. y A. z ( ( x F z /\ y F z ) -> x = y ) )
43	41, 42	bitri 264	. . . . 5 |- ( A. z E* x x F z <-> A. x A. y A. z ( ( x F z /\ y F z ) -> x = y ) )
44		r2al 2939	. . . . 5 |- ( A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. x A. y ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
45	38, 43, 44	3bitr4g 303	. . . 4 |- ( F Fn A -> ( A. z E* x x F z <-> A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
46	2, 45	syl 17	. . 3 |- ( F : A --> B -> ( A. z E* x x F z <-> A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
47	46	pm5.32i 669	. 2 |- ( ( F : A --> B /\ A. z E* x x F z ) <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
48	1, 47	bitri 264	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   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   E*wmo 2471   A.wral 2912   class class class wbr 4653   dom cdm 5114   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fv 5896

This theorem is referenced by:  dff13f  6513  f1veqaeq  6514  fpropnf1  6524  dff14a  6527  dff1o6  6531  fcof1  6542  soisoi  6578  f1o2ndf1  7285  fnwelem  7292  smo11  7461  tz7.48lem  7536  omsmo  7734  unxpdomlem3  8166  unfilem2  8225  fofinf1o  8241  inf3lem6  8530  r111  8638  fseqenlem1  8847  fodomacn  8879  alephf1  8908  alephiso  8921  ackbij1lem17  9058  infpssrlem5  9129  fin23lem28  9162  fin1a2lem2  9223  fin1a2lem4  9225  axcc2lem  9258  domtriomlem  9264  cnref1o  11827  injresinj  12589  om2uzf1oi  12752  cshf1  13556  wwlktovf1  13700  reeff1  14850  bitsf1  15168  crth  15483  eulerthlem2  15487  1arith  15631  vdwlem12  15696  xpsff1o  16228  setcmon  16737  fthestrcsetc  16790  embedsetcestrclem  16797  fthsetcestrc  16805  yoniso  16925  ghmf1  17689  orbsta  17746  symgextf1  17841  symgfixf1  17857  odf1  17979  kerf1hrm  18743  mvrf1  19425  ply1sclf1  19659  znf1o  19900  cygznlem3  19918  uvcf1  20131  lindff1  20159  scmatf1  20337  mdetunilem8  20425  mat2pmatf1  20534  pm2mpf1  20604  ist0-4  21532  ovolicc2lem4  23288  recosf1o  24281  efif1olem4  24291  basellem4  24810  dvdsmulf1o  24920  lgsqrlem2  25072  lgseisenlem2  25101  2lgslem1b  25117  axlowdimlem15  25836  upgrwlkdvdelem  26632  wlkpwwlkf1ouspgr  26765  wlknwwlksninj  26775  wlkwwlkinj  26782  wwlksnextinj  26794  clwwlksf1  26917  clwlksf1clwwlk  26969  frgrncvvdeqlem8  27170  numclwlk1lem2f1  27227  pjmf1  28575  unopf1o  28775  erdszelem9  31181  mrsubff1  31411  msubff1  31453  mvhf1  31456  f1omptsnlem  33183  poimirlem26  33435  poimirlem27  33436  f1opr  33519  grpokerinj  33692  cdleme50f1  35831  dihf11  36556  dnnumch3  37617  wessf1ornlem  39371  projf1o  39386  sumnnodd  39862  dvnprodlem1  40161  fourierdlem34  40358  fourierdlem51  40374  fargshiftf1  41377  fmtnof1  41447  prmdvdsfmtnof1  41499  sprsymrelf1  41746  uspgrsprf1  41755