Theorem dff13 6152

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 5778	. 2 |- ( F : A -1-1-> B <-> ( F : A --> B /\ A. z E* x x F z ) )
2		ffn 5729	. . . 4 |- ( F : A --> B -> F Fn A )
3		vex 3116	. . . . . . . . . . . . . . 15 |- x e. _V
4		vex 3116	. . . . . . . . . . . . . . 15 |- z e. _V
5	3, 4	breldm 5205	. . . . . . . . . . . . . 14 |- ( x F z -> x e. dom F )
6		fndm 5678	. . . . . . . . . . . . . . 15 |- ( F Fn A -> dom F = A )
7	6	eleq2d 2537	. . . . . . . . . . . . . 14 |- ( F Fn A -> ( x e. dom F <-> x e. A ) )
8	5, 7	syl5ib 219	. . . . . . . . . . . . 13 |- ( F Fn A -> ( x F z -> x e. A ) )
9		vex 3116	. . . . . . . . . . . . . . 15 |- y e. _V
10	9, 4	breldm 5205	. . . . . . . . . . . . . 14 |- ( y F z -> y e. dom F )
11	6	eleq2d 2537	. . . . . . . . . . . . . 14 |- ( F Fn A -> ( y e. dom F <-> y e. A ) )
12	10, 11	syl5ib 219	. . . . . . . . . . . . 13 |- ( F Fn A -> ( y F z -> y e. A ) )
13	8, 12	anim12d 563	. . . . . . . . . . . 12 |- ( F Fn A -> ( ( x F z /\ y F z ) -> ( x e. A /\ y e. A ) ) )
14	13	pm4.71rd 635	. . . . . . . . . . 11 |- ( F Fn A -> ( ( x F z /\ y F z ) <-> ( ( x e. A /\ y e. A ) /\ ( x F z /\ y F z ) ) ) )
15		eqcom 2476	. . . . . . . . . . . . . . 15 |- ( z = ( F ` x ) <-> ( F ` x ) = z )
16		fnbrfvb 5906	. . . . . . . . . . . . . . 15 |- ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = z <-> x F z ) )
17	15, 16	syl5bb 257	. . . . . . . . . . . . . 14 |- ( ( F Fn A /\ x e. A ) -> ( z = ( F ` x ) <-> x F z ) )
18		eqcom 2476	. . . . . . . . . . . . . . 15 |- ( z = ( F ` y ) <-> ( F ` y ) = z )
19		fnbrfvb 5906	. . . . . . . . . . . . . . 15 |- ( ( F Fn A /\ y e. A ) -> ( ( F ` y ) = z <-> y F z ) )
20	18, 19	syl5bb 257	. . . . . . . . . . . . . 14 |- ( ( F Fn A /\ y e. A ) -> ( z = ( F ` y ) <-> y F z ) )
21	17, 20	bi2anan9 871	. . . . . . . . . . . . 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 828	. . . . . . . . . . . 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 641	. . . . . . . . . . 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 256	. . . . . . . . . 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 317	. . . . . . . . 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 446	. . . . . . . . 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 261	. . . . . . . 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 1689	. . . . . . 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 1930	. . . . . . . 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 1932	. . . . . . . . . 10 |- ( A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) <-> ( E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) )
31		fvex 5874	. . . . . . . . . . . 12 |- ( F ` x ) e. _V
32	31	eqvinc 3230	. . . . . . . . . . 11 |- ( ( F ` x ) = ( F ` y ) <-> E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) )
33	32	imbi1i 325	. . . . . . . . . 10 |- ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) )
34	30, 33	bitr4i 252	. . . . . . . . 9 |- ( A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) <-> ( ( F ` x ) = ( F ` y ) -> x = y ) )
35	34	imbi2i 312	. . . . . . . 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 249	. . . . . . 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 261	. . . . . 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 1691	. . . . 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 4450	. . . . . . . 8 |- ( x = y -> ( x F z <-> y F z ) )
40	39	mo4 2339	. . . . . . 7 |- ( E* x x F z <-> A. x A. y ( ( x F z /\ y F z ) -> x = y ) )
41	40	albii 1620	. . . . . 6 |- ( A. z E* x x F z <-> A. z A. x A. y ( ( x F z /\ y F z ) -> x = y ) )
42		alrot3 1795	. . . . . 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 249	. . . . 5 |- ( A. z E* x x F z <-> A. x A. y A. z ( ( x F z /\ y F z ) -> x = y ) )
44		r2al 2842	. . . . 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 288	. . . 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 16	. . 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 637	. 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 249	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 184   /\ wa 369   A.wal 1377   = wceq 1379   E.wex 1596   e. wcel 1767   E*wmo 2276   A.wral 2814   class class class wbr 4447   dom cdm 4999   Fn wfn 5581   -->wf 5582   -1-1->wf1 5583   ` cfv 5586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fv 5594

This theorem is referenced by:  dff13f  6153  f1veqaeq  6154  dff14a  6163  dff1o6  6167  fcof1  6176  soisoi  6210  f1o2ndf1  6888  fnwelem  6895  smo11  7032  tz7.48lem  7103  omsmo  7300  unxpdomlem3  7723  unfilem2  7781  fofinf1o  7797  inf3lem6  8046  r111  8189  fseqenlem1  8401  fodomacn  8433  alephf1  8462  alephiso  8475  ackbij1lem17  8612  infpssrlem5  8683  fin23lem28  8716  fin1a2lem2  8777  fin1a2lem4  8779  axcc2lem  8812  domtriomlem  8818  cnref1o  11211  injresinj  11890  om2uzf1oi  12028  wwlktovf1  12854  reeff1  13712  bitsf1  13951  crt  14163  eulerthlem2  14167  1arith  14300  vdwlem12  14365  xpsff1o  14819  setcmon  15268  yoniso  15408  ghmf1  16090  orbsta  16146  symgextf1  16241  symgfixf1  16258  odf1  16380  kerf1hrm  17175  mvrf1  17852  ply1sclf1  18101  znf1o  18357  cygznlem3  18375  uvcf1  18590  lindff1  18622  scmatf1  18800  mdetunilem8  18888  mat2pmatf1  18997  pm2mpf1  19067  ist0-4  19965  ovolicc2lem4  21666  recosf1o  22655  efif1olem4  22665  basellem4  23085  dvdsmulf1o  23198  lgsqrlem2  23345  lgseisenlem2  23353  axlowdimlem15  23935  wlkntrllem3  24239  wlkdvspthlem  24285  fargshiftf1  24313  constr3trllem2  24327  wlknwwlkninj  24387  wlkiswwlkinj  24394  wwlkextinj  24406  clwwlkf1  24472  clwlkf1clwwlk  24526  frgrancvvdeqlemB  24715  numclwlk1lem2f1  24771  pjmf1  26310  unopf1o  26511  erdszelem9  28283  ghomf1olem  28509  f1opr  29818  grpokerinj  29950  dnnumch3  30597  sumnnodd  31172  fourierdlem34  31441  fourierdlem51  31458  cdleme50f1  35339  dihf11  36064