Theorem dff13 6183

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 5800	. 2 |- ( F : A -1-1-> B <-> ( F : A --> B /\ A. z E* x x F z ) )
2		ffn 5750	. . . 4 |- ( F : A --> B -> F Fn A )
3		vex 3059	. . . . . . . . . . . . . . 15 |- x e. _V
4		vex 3059	. . . . . . . . . . . . . . 15 |- z e. _V
5	3, 4	breldm 5057	. . . . . . . . . . . . . 14 |- ( x F z -> x e. dom F )
6		fndm 5696	. . . . . . . . . . . . . . 15 |- ( F Fn A -> dom F = A )
7	6	eleq2d 2524	. . . . . . . . . . . . . 14 |- ( F Fn A -> ( x e. dom F <-> x e. A ) )
8	5, 7	syl5ib 227	. . . . . . . . . . . . 13 |- ( F Fn A -> ( x F z -> x e. A ) )
9		vex 3059	. . . . . . . . . . . . . . 15 |- y e. _V
10	9, 4	breldm 5057	. . . . . . . . . . . . . 14 |- ( y F z -> y e. dom F )
11	6	eleq2d 2524	. . . . . . . . . . . . . 14 |- ( F Fn A -> ( y e. dom F <-> y e. A ) )
12	10, 11	syl5ib 227	. . . . . . . . . . . . 13 |- ( F Fn A -> ( y F z -> y e. A ) )
13	8, 12	anim12d 570	. . . . . . . . . . . 12 |- ( F Fn A -> ( ( x F z /\ y F z ) -> ( x e. A /\ y e. A ) ) )
14	13	pm4.71rd 645	. . . . . . . . . . 11 |- ( F Fn A -> ( ( x F z /\ y F z ) <-> ( ( x e. A /\ y e. A ) /\ ( x F z /\ y F z ) ) ) )
15		eqcom 2468	. . . . . . . . . . . . . . 15 |- ( z = ( F ` x ) <-> ( F ` x ) = z )
16		fnbrfvb 5927	. . . . . . . . . . . . . . 15 |- ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = z <-> x F z ) )
17	15, 16	syl5bb 265	. . . . . . . . . . . . . 14 |- ( ( F Fn A /\ x e. A ) -> ( z = ( F ` x ) <-> x F z ) )
18		eqcom 2468	. . . . . . . . . . . . . . 15 |- ( z = ( F ` y ) <-> ( F ` y ) = z )
19		fnbrfvb 5927	. . . . . . . . . . . . . . 15 |- ( ( F Fn A /\ y e. A ) -> ( ( F ` y ) = z <-> y F z ) )
20	18, 19	syl5bb 265	. . . . . . . . . . . . . 14 |- ( ( F Fn A /\ y e. A ) -> ( z = ( F ` y ) <-> y F z ) )
21	17, 20	bi2anan9 889	. . . . . . . . . . . . 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 844	. . . . . . . . . . . 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 651	. . . . . . . . . . 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 264	. . . . . . . . . 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 323	. . . . . . . . 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 452	. . . . . . . . 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 269	. . . . . . . 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 1777	. . . . . . 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 1796	. . . . . . . 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 1828	. . . . . . . . . 10 |- ( A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) <-> ( E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) )
31		fvex 5897	. . . . . . . . . . . 12 |- ( F ` x ) e. _V
32	31	eqvinc 3177	. . . . . . . . . . 11 |- ( ( F ` x ) = ( F ` y ) <-> E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) )
33	32	imbi1i 331	. . . . . . . . . 10 |- ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) )
34	30, 33	bitr4i 260	. . . . . . . . 9 |- ( A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) <-> ( ( F ` x ) = ( F ` y ) -> x = y ) )
35	34	imbi2i 318	. . . . . . . 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 257	. . . . . . 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 269	. . . . . 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 1779	. . . . 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 4418	. . . . . . . 8 |- ( x = y -> ( x F z <-> y F z ) )
40	39	mo4 2356	. . . . . . 7 |- ( E* x x F z <-> A. x A. y ( ( x F z /\ y F z ) -> x = y ) )
41	40	albii 1701	. . . . . 6 |- ( A. z E* x x F z <-> A. z A. x A. y ( ( x F z /\ y F z ) -> x = y ) )
42		alrot3 1934	. . . . . 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 257	. . . . 5 |- ( A. z E* x x F z <-> A. x A. y A. z ( ( x F z /\ y F z ) -> x = y ) )
44		r2al 2777	. . . . 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 296	. . . 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 647	. 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 257	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 189   /\ wa 375   A.wal 1452   = wceq 1454   E.wex 1673   e. wcel 1897   E*wmo 2310   A.wral 2748   class class class wbr 4415   dom cdm 4852   Fn wfn 5595   -->wf 5596   -1-1->wf1 5597   ` cfv 5600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-sbc 3279  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-opab 4475  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fv 5608

This theorem is referenced by:  dff13f  6184  f1veqaeq  6185  dff14a  6194  dff1o6  6198  fcof1  6209  soisoi  6243  f1o2ndf1  6930  fnwelem  6937  smo11  7108  tz7.48lem  7183  omsmo  7380  unxpdomlem3  7803  unfilem2  7861  fofinf1o  7877  inf3lem6  8163  r111  8271  fseqenlem1  8480  fodomacn  8512  alephf1  8541  alephiso  8554  ackbij1lem17  8691  infpssrlem5  8762  fin23lem28  8795  fin1a2lem2  8856  fin1a2lem4  8858  axcc2lem  8891  domtriomlem  8897  cnref1o  11325  injresinj  12056  om2uzf1oi  12198  wwlktovf1  13080  reeff1  14222  bitsf1  14468  crt  14774  eulerthlem2  14778  1arith  14919  vdwlem12  14990  xpsff1o  15522  setcmon  16030  fthestrcsetc  16083  embedsetcestrclem  16090  fthsetcestrc  16098  yoniso  16218  ghmf1  16959  orbsta  17015  symgextf1  17110  symgfixf1  17126  odf1  17261  kerf1hrm  18019  mvrf1  18697  ply1sclf1  18930  znf1o  19170  cygznlem3  19188  uvcf1  19398  lindff1  19426  scmatf1  19604  mdetunilem8  19692  mat2pmatf1  19801  pm2mpf1  19871  ist0-4  20792  ovolicc2lem4OLD  22521  ovolicc2lem4  22522  recosf1o  23532  efif1olem4  23542  basellem4  24058  dvdsmulf1o  24171  lgsqrlem2  24318  lgseisenlem2  24326  axlowdimlem15  25034  wlkntrllem3  25339  wlkdvspthlem  25385  fargshiftf1  25413  constr3trllem2  25427  wlknwwlkninj  25487  wlkiswwlkinj  25494  wwlkextinj  25506  clwwlkf1  25572  clwlkf1clwwlk  25626  frgrancvvdeqlemB  25814  numclwlk1lem2f1  25870  pjmf1  27417  unopf1o  27617  erdszelem9  29970  mrsubff1  30200  msubff1  30242  mvhf1  30245  ghomf1olem  30360  f1omptsnlem  31782  poimirlem26  32010  poimirlem27  32011  f1opr  32095  grpokerinj  32227  cdleme50f1  34154  dihf11  34879  dnnumch3  35949  wessf1ornlem  37496  projf1o  37511  sumnnodd  37747  dvnprodlem1  37858  fourierdlem34  38041  fourierdlem51  38058  fpropnf1  39077  upgrwlkdvdelem  39767