Theorem dff13 7233

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	⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦

Allowed substitution hints:   𝐵(𝑥,𝑦)

Proof of Theorem dff13

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dff12 6754	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧))
2		ffn 6686	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3		vex 3457	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
4		vex 3457	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
5	3, 4	breldm 5880	. . . . . . . . . . . . . 14 ⊢ (𝑥𝐹𝑧 → 𝑥 ∈ dom 𝐹)
6		fndm 6619	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
7	6	eleq2d 2847	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴))
8	5, 7	imbitrid 246	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑧 → 𝑥 ∈ 𝐴))
9		vex 3457	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
10	9, 4	breldm 5880	. . . . . . . . . . . . . 14 ⊢ (𝑦𝐹𝑧 → 𝑦 ∈ dom 𝐹)
11	6	eleq2d 2847	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴))
12	10, 11	imbitrid 246	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝐴 → (𝑦𝐹𝑧 → 𝑦 ∈ 𝐴))
13	8, 12	anim12d 618	. . . . . . . . . . . 12 ⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)))
14	13	pm4.71rd 570	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧))))
15		eqcom 2768	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑧)
16		fnbrfvb 6912	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑧 ↔ 𝑥𝐹𝑧))
17	15, 16	bitrid 285	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑧 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑧))
18		eqcom 2768	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = 𝑧)
19		fnbrfvb 6912	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) = 𝑧 ↔ 𝑦𝐹𝑧))
20	18, 19	bitrid 285	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑧 = (𝐹‘𝑦) ↔ 𝑦𝐹𝑧))
21	17, 20	bi2anan9 647	. . . . . . . . . . . . 13 ⊢ (((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) ↔ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧)))
22	21	anandis 688	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) ↔ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧)))
23	22	pm5.32da 587	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧))))
24	14, 23	bitr4d 284	. . . . . . . . . 10 ⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)))))
25	24	imbi1d 343	. . . . . . . . 9 ⊢ (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) → 𝑥 = 𝑦)))
26		impexp 454	. . . . . . . . 9 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)))
27	25, 26	bitrdi 289	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))))
28	27	albidv 1939	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))))
29		19.21v 1958	. . . . . . . 8 ⊢ (∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)))
30		19.23v 1961	. . . . . . . . . 10 ⊢ (∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))
31		fvex 6875	. . . . . . . . . . . 12 ⊢ (𝐹‘𝑥) ∈ V
32	31	eqvinc 3607	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ ∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)))
33	32	imbi1i 351	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))
34	30, 33	bitr4i 280	. . . . . . . . 9 ⊢ (∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
35	34	imbi2i 338	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
36	29, 35	bitri 277	. . . . . . 7 ⊢ (∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
37	28, 36	bitrdi 289	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))
38	37	2albidv 1942	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))
39		breq1 5100	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥𝐹𝑧 ↔ 𝑦𝐹𝑧))
40	39	mo4 2592	. . . . . . 7 ⊢ (∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦))
41	40	albii 1838	. . . . . 6 ⊢ (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑧∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦))
42		alrot3 2193	. . . . . 6 ⊢ (∀𝑧∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦))
43	41, 42	bitri 277	. . . . 5 ⊢ (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦))
44		r2al 3197	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
45	38, 43, 44	3bitr4g 316	. . . 4 ⊢ (𝐹 Fn 𝐴 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
46	2, 45	syl 17	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
47	46	pm5.32i 582	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
48	1, 47	bitri 277	1 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1557   = wceq 1559  ∃wex 1798   ∈ wcel 2141  ∃*wmo 2563  ∀wral 3075   class class class wbr 5097  dom cdm 5643   Fn wfn 6511  ⟶wf 6512  –1-1→wf1 6513  ‘cfv 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fv 6524

This theorem is referenced by:  dff13f  7234  f1veqaeq  7235  fpropnf1  7246  dff14a  7249  dff1o6  7254  fcof1  7266  nf1const  7283  soisoi  7307  f1opr  7447  f1o2ndf1  8095  fnwelem  8105  smo11  8329  tz7.48lem  8406  omsmo  8622  unxpdomlem3  9196  unfilem2  9244  fofinf1o  9269  inf3lem6  9582  r111  9727  fseqenlem1  9974  fodomacn  10006  alephf1  10035  alephiso  10048  ackbij1lem17  10185  infpssrlem5  10258  fin23lem28  10291  fin1a2lem2  10352  fin1a2lem4  10354  axcc2lem  10387  domtriomlem  10393  cnref1o  12980  injresinj  13791  om2uzf1oi  13960  cshf1  14817  wwlktovf1  14964  reeff1  16143  bitsf1  16471  crth  16804  eulerthlem2  16808  1arith  16954  vdwlem12  17019  xpsff1o  17588  setcmon  18111  fthestrcsetc  18173  embedsetcestrclem  18180  fthsetcestrc  18188  yoniso  18308  chnpof1  18653  ghmf1  19277  kerf1ghm  19278  orbsta  19344  symgextf1  19452  symgfixf1  19468  odf1  19593  znf1o  21591  cygznlem3  21609  uvcf1  21832  lindff1  21860  mvrf1  22025  ply1sclf1  22340  scmatf1  22579  mdetunilem8  22667  mat2pmatf1  22777  pm2mpf1  22847  ist0-4  23777  ovolicc2lem4  25570  recosf1o  26588  efif1olem4  26598  basellem4  27136  mpodvdsmulf1o  27246  dvdsmulf1o  27248  lgsqrlem2  27399  lgseisenlem2  27428  2lgslem1b  27444  negsf1o  28135  oniso  28352  om2noseqf1o  28382  bdayn0sf1o  28451  axlowdimlem15  29114  upgrwlkdvdelem  29893  wlkswwlksf1o  30036  wwlksnextinj  30056  clwlkclwwlkf1  30169  clwwlkf1  30208  frgrncvvdeqlem8  30465  numclwwlk1lem2f1  30516  pjmf1  31876  unopf1o  32076  2ndresdju  32812  fnpreimac  32833  s3f1  33086  ccatf1  33088  swrdf1  33095  mndlactf1  33165  mndractf1  33167  tocyccntz  33285  extvfvcl  33794  dff15  35339  f1resrcmplf1d  35342  onvfowev  35420  f1resfz0f1d  35425  erdszelem9  35510  mrsubff1  35825  msubff1  35867  mvhf1  35870  f1omptsnlem  37791  fvineqsnf1  37865  fvineqsneu  37866  poimirlem26  38106  poimirlem27  38107  grpokerinj  38353  cdleme50f1  41128  dihf11  41852  hashscontpow  42700  hashnexinj  42706  aks6d1c5  42717  sticksstones2  42725  aks6d1c6lem3  42750  fimgmcyc  43113  dnnumch3  43585  wessf1ornlem  45724  projf1o  45735  sumnnodd  46167  dvnprodlem1  46481  fourierdlem34  46676  fourierdlem51  46692  fsetsnf1  47607  cfsetsnfsetf1  47614  fcoresf1  47624  imasetpreimafvbijlemf1  47971  fargshiftf1  48008  sprsymrelf1  48063  prproropf1o  48074  fmtnof1  48105  prmdvdsfmtnof1  48157  uspgrsprf1  48730  1arymaptf1  49225  2arymaptf1  49236  rrx2xpref1o  49301  oppff1  49730  diag1f1  49889  diag2f1  49891