Theorem dff13 7256

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 6775	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧))
2		ffn 6707	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3		vex 3455	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
4		vex 3455	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
5	3, 4	breldm 5890	. . . . . . . . . . . . . 14 ⊢ (𝑥𝐹𝑧 → 𝑥 ∈ dom 𝐹)
6		fndm 6640	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
7	6	eleq2d 2847	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴))
8	5, 7	imbitrid 247	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑧 → 𝑥 ∈ 𝐴))
9		vex 3455	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
10	9, 4	breldm 5890	. . . . . . . . . . . . . 14 ⊢ (𝑦𝐹𝑧 → 𝑦 ∈ dom 𝐹)
11	6	eleq2d 2847	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴))
12	10, 11	imbitrid 247	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝐴 → (𝑦𝐹𝑧 → 𝑦 ∈ 𝐴))
13	8, 12	anim12d 621	. . . . . . . . . . . 12 ⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)))
14	13	pm4.71rd 572	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧))))
15		eqcom 2768	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑧)
16		fnbrfvb 6933	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑧 ↔ 𝑥𝐹𝑧))
17	15, 16	bitrid 286	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑧 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑧))
18		eqcom 2768	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = 𝑧)
19		fnbrfvb 6933	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) = 𝑧 ↔ 𝑦𝐹𝑧))
20	18, 19	bitrid 286	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑧 = (𝐹‘𝑦) ↔ 𝑦𝐹𝑧))
21	17, 20	bi2anan9 650	. . . . . . . . . . . . 13 ⊢ (((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) ↔ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧)))
22	21	anandis 691	. . . . . . . . . . . 12 ⊢ ((𝐹 Fn 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) ↔ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧)))
23	22	pm5.32da 590	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧))))
24	14, 23	bitr4d 285	. . . . . . . . . 10 ⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)))))
25	24	imbi1d 344	. . . . . . . . 9 ⊢ (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) → 𝑥 = 𝑦)))
26		impexp 456	. . . . . . . . 9 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)))
27	25, 26	bitrdi 290	. . . . . . . 8 ⊢ (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))))
28	27	albidv 1953	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))))
29		19.21v 1972	. . . . . . . 8 ⊢ (∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)))
30		19.23v 1975	. . . . . . . . . 10 ⊢ (∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))
31		fvex 6896	. . . . . . . . . . . 12 ⊢ (𝐹‘𝑥) ∈ V
32	31	eqvinc 3603	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ ∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)))
33	32	imbi1i 352	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))
34	30, 33	bitr4i 281	. . . . . . . . 9 ⊢ (∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
35	34	imbi2i 339	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
36	29, 35	bitri 278	. . . . . . 7 ⊢ (∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
37	28, 36	bitrdi 290	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))
38	37	2albidv 1956	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))
39		breq1 5106	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥𝐹𝑧 ↔ 𝑦𝐹𝑧))
40	39	mo4 2592	. . . . . . 7 ⊢ (∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦))
41	40	albii 1852	. . . . . 6 ⊢ (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑧∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦))
42		alrot3 2197	. . . . . 6 ⊢ (∀𝑧∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦))
43	41, 42	bitri 278	. . . . 5 ⊢ (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦))
44		r2al 3199	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
45	38, 43, 44	3bitr4g 317	. . . 4 ⊢ (𝐹 Fn 𝐴 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
46	2, 45	syl 18	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
47	46	pm5.32i 585	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
48	1, 47	bitri 278	1 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∃*wmo 2563  ∀wral 3077   class class class wbr 5103  dom cdm 5651   Fn wfn 6532  ⟶wf 6533  –1-1→wf1 6534  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fv 6545

This theorem is used by:  dff13f  7257  f1veqaeq  7258  fpropnf1  7269  dff14a  7272  dff15  7274  f1resrcmplf1d  7277  dff1o6  7281  fcof1  7293  nf1const  7310  soisoi  7334  f1opr  7474  f1o2ndf1  8131  fnwelem  8141  smo11  8365  onelfvnef1  8442  tz7.48lemOLD  8444  omsmo  8660  unxpdomlem3  9242  unfilem2  9291  fofinf1o  9314  inf3lem6  9627  r111  9775  fseqenlem1  10096  fodomacn  10128  alephf1  10157  alephiso  10170  ackbij1lem17  10306  infpssrlem5  10378  fin23lem28  10411  fin1a2lem2  10472  fin1a2lem4  10474  axcc2lem  10507  domtriomlem  10513  cnref1o  13106  injresinj  13919  f1resfz0f1d  13920  om2uzf1oi  14089  ccatf1  14729  swrdf1  14792  cshf1  14954  wwlktovf1  15103  reeff1  16281  bitsf1  16609  crth  16948  eulerthlem2  16952  1arith  17098  vdwlem12  17163  xpsff1o  17732  setcmon  18255  fthestrcsetc  18317  embedsetcestrclem  18324  fthsetcestrc  18332  yoniso  18452  chnpof1  18797  ghmf1  19453  kerf1ghm  19454  orbsta  19520  symgextf1  19628  symgfixf1  19644  odf1  19769  znf1o  21850  cygznlem3  21868  uvcf1  22091  lindff1  22119  mvrf1  22286  ply1sclf1  22601  scmatf1  22839  mdetunilem8  22927  mat2pmatf1  23040  pm2mpf1  23110  ist0-4  24041  ovolicc2lem4  25834  recosf1o  26856  efif1olem4  26866  basellem4  27404  mpodvdsmulf1o  27514  dvdsmulf1o  27516  lgsqrlem2  27667  lgseisenlem2  27696  2lgslem1b  27712  negsf1o  28433  oniso  28650  om2noseqf1o  28680  bdayn0sf1o  28749  axlowdimlem15  29527  upgrwlkdvdelem  30315  wlkswwlksf1o  30461  wwlksnextinj  30481  clwlkclwwlkf1  30594  clwwlkf1  30633  frgrncvvdeqlem8  30900  numclwwlk1lem2f1  30951  pjmf1  32311  unopf1o  32511  2ndresdju  33236  fnpreimac  33257  s3f1  33504  mndlactf1  33580  mndractf1  33582  tocyccntz  33698  extvfvcl  34161  onvfowev  35878  erdszelem9  35943  mrsubff1  36258  msubff1  36300  mvhf1  36303  f1omptsnlem  38239  fvineqsnf1  38313  fvineqsneu  38314  poimirlem26  38544  poimirlem27  38545  grpokerinj  38807  cdleme50f1  41580  dihf11  42304  hashscontpow  43152  hashnexinj  43158  aks6d1c5  43169  sticksstones2  43177  aks6d1c6lem3  43202  fimgmcyc  43578  dnnumch3  44033  wessf1ornlem  46169  projf1o  46180  sumnnodd  46611  dvnprodlem1  46925  fourierdlem34  47120  fourierdlem51  47136  fsetsnf1  48091  cfsetsnfsetf1  48098  fcoresf1  48108  imasetpreimafvbijlemf1  48455  fargshiftf1  48492  sprsymrelf1  48547  prproropf1o  48558  fmtnof1  48589  prmdvdsfmtnof1  48641  uspgrsprf1  49214  1arymaptf1  49723  2arymaptf1  49734  rrx2xpref1o  49799  oppff1  50225  diag1f1  50384  diag2f1  50386