Theorem dff13 6171

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 5792	. 2 |- ( F : A -1-1-> B <-> ( F : A --> B /\ A. z E* x x F z ) )
2		ffn 5743	. . . 4 |- ( F : A --> B -> F Fn A )
3		vex 3084	. . . . . . . . . . . . . . 15 |- x e. _V
4		vex 3084	. . . . . . . . . . . . . . 15 |- z e. _V
5	3, 4	breldm 5055	. . . . . . . . . . . . . 14 |- ( x F z -> x e. dom F )
6		fndm 5690	. . . . . . . . . . . . . . 15 |- ( F Fn A -> dom F = A )
7	6	eleq2d 2492	. . . . . . . . . . . . . 14 |- ( F Fn A -> ( x e. dom F <-> x e. A ) )
8	5, 7	syl5ib 222	. . . . . . . . . . . . 13 |- ( F Fn A -> ( x F z -> x e. A ) )
9		vex 3084	. . . . . . . . . . . . . . 15 |- y e. _V
10	9, 4	breldm 5055	. . . . . . . . . . . . . 14 |- ( y F z -> y e. dom F )
11	6	eleq2d 2492	. . . . . . . . . . . . . 14 |- ( F Fn A -> ( y e. dom F <-> y e. A ) )
12	10, 11	syl5ib 222	. . . . . . . . . . . . 13 |- ( F Fn A -> ( y F z -> y e. A ) )
13	8, 12	anim12d 565	. . . . . . . . . . . 12 |- ( F Fn A -> ( ( x F z /\ y F z ) -> ( x e. A /\ y e. A ) ) )
14	13	pm4.71rd 639	. . . . . . . . . . 11 |- ( F Fn A -> ( ( x F z /\ y F z ) <-> ( ( x e. A /\ y e. A ) /\ ( x F z /\ y F z ) ) ) )
15		eqcom 2431	. . . . . . . . . . . . . . 15 |- ( z = ( F ` x ) <-> ( F ` x ) = z )
16		fnbrfvb 5918	. . . . . . . . . . . . . . 15 |- ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = z <-> x F z ) )
17	15, 16	syl5bb 260	. . . . . . . . . . . . . 14 |- ( ( F Fn A /\ x e. A ) -> ( z = ( F ` x ) <-> x F z ) )
18		eqcom 2431	. . . . . . . . . . . . . . 15 |- ( z = ( F ` y ) <-> ( F ` y ) = z )
19		fnbrfvb 5918	. . . . . . . . . . . . . . 15 |- ( ( F Fn A /\ y e. A ) -> ( ( F ` y ) = z <-> y F z ) )
20	18, 19	syl5bb 260	. . . . . . . . . . . . . 14 |- ( ( F Fn A /\ y e. A ) -> ( z = ( F ` y ) <-> y F z ) )
21	17, 20	bi2anan9 881	. . . . . . . . . . . . 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 837	. . . . . . . . . . . 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 645	. . . . . . . . . . 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 259	. . . . . . . . . 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 318	. . . . . . . . 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 447	. . . . . . . . 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 264	. . . . . . . 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 1757	. . . . . . 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 1775	. . . . . . . 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 1807	. . . . . . . . . 10 |- ( A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) <-> ( E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) )
31		fvex 5888	. . . . . . . . . . . 12 |- ( F ` x ) e. _V
32	31	eqvinc 3198	. . . . . . . . . . 11 |- ( ( F ` x ) = ( F ` y ) <-> E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) )
33	32	imbi1i 326	. . . . . . . . . 10 |- ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) )
34	30, 33	bitr4i 255	. . . . . . . . 9 |- ( A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) <-> ( ( F ` x ) = ( F ` y ) -> x = y ) )
35	34	imbi2i 313	. . . . . . . 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 252	. . . . . . 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 264	. . . . . 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 1759	. . . . 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 4423	. . . . . . . 8 |- ( x = y -> ( x F z <-> y F z ) )
40	39	mo4 2313	. . . . . . 7 |- ( E* x x F z <-> A. x A. y ( ( x F z /\ y F z ) -> x = y ) )
41	40	albii 1687	. . . . . 6 |- ( A. z E* x x F z <-> A. z A. x A. y ( ( x F z /\ y F z ) -> x = y ) )
42		alrot3 1896	. . . . . 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 252	. . . . 5 |- ( A. z E* x x F z <-> A. x A. y A. z ( ( x F z /\ y F z ) -> x = y ) )
44		r2al 2803	. . . . 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 291	. . . 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 641	. 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 252	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 187   /\ wa 370   A.wal 1435   = wceq 1437   E.wex 1659   e. wcel 1868   E*wmo 2266   A.wral 2775   class class class wbr 4420   dom cdm 4850   Fn wfn 5593   -->wf 5594   -1-1->wf1 5595   ` cfv 5598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fv 5606

This theorem is referenced by:  dff13f  6172  f1veqaeq  6173  dff14a  6182  dff1o6  6186  fcof1  6197  soisoi  6231  f1o2ndf1  6912  fnwelem  6919  smo11  7088  tz7.48lem  7163  omsmo  7360  unxpdomlem3  7781  unfilem2  7839  fofinf1o  7855  inf3lem6  8141  r111  8248  fseqenlem1  8456  fodomacn  8488  alephf1  8517  alephiso  8530  ackbij1lem17  8667  infpssrlem5  8738  fin23lem28  8771  fin1a2lem2  8832  fin1a2lem4  8834  axcc2lem  8867  domtriomlem  8873  cnref1o  11298  injresinj  12025  om2uzf1oi  12167  wwlktovf1  13021  reeff1  14162  bitsf1  14408  crt  14714  eulerthlem2  14718  1arith  14859  vdwlem12  14930  xpsff1o  15462  setcmon  15970  fthestrcsetc  16023  embedsetcestrclem  16030  fthsetcestrc  16038  yoniso  16158  ghmf1  16899  orbsta  16955  symgextf1  17050  symgfixf1  17066  odf1  17201  kerf1hrm  17959  mvrf1  18637  ply1sclf1  18870  znf1o  19109  cygznlem3  19127  uvcf1  19337  lindff1  19365  scmatf1  19543  mdetunilem8  19631  mat2pmatf1  19740  pm2mpf1  19810  ist0-4  20731  ovolicc2lem4OLD  22460  ovolicc2lem4  22461  recosf1o  23471  efif1olem4  23481  basellem4  23997  dvdsmulf1o  24110  lgsqrlem2  24257  lgseisenlem2  24265  axlowdimlem15  24973  wlkntrllem3  25277  wlkdvspthlem  25323  fargshiftf1  25351  constr3trllem2  25365  wlknwwlkninj  25425  wlkiswwlkinj  25432  wwlkextinj  25444  clwwlkf1  25510  clwlkf1clwwlk  25564  frgrancvvdeqlemB  25752  numclwlk1lem2f1  25808  pjmf1  27355  unopf1o  27555  erdszelem9  29918  mrsubff1  30148  msubff1  30190  mvhf1  30193  ghomf1olem  30308  f1omptsnlem  31679  poimirlem26  31880  poimirlem27  31881  f1opr  31965  grpokerinj  32097  cdleme50f1  34029  dihf11  34754  dnnumch3  35825  wessf1ornlem  37309  projf1o  37324  sumnnodd  37530  dvnprodlem1  37641  fourierdlem34  37824  fourierdlem51  37841