Theorem dff13 7260

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 6780	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧))
2		ffn 6712	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
4		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
5	3, 4	breldm 5890	. . . . . . . . . . . . . 14 ⊢ (𝑥𝐹𝑧 → 𝑥 ∈ dom 𝐹)
6		fndm 6645	. . . . . . . . . . . . . . 15 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
7	6	eleq2d 2846	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴))
8	5, 7	imbitrid 247	. . . . . . . . . . . . 13 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑧 → 𝑥 ∈ 𝐴))
9		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
10	9, 4	breldm 5890	. . . . . . . . . . . . . 14 ⊢ (𝑦𝐹𝑧 → 𝑦 ∈ dom 𝐹)
11	6	eleq2d 2846	. . . . . . . . . . . . . 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 2767	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑧)
16		fnbrfvb 6938	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑧 ↔ 𝑥𝐹𝑧))
17	15, 16	bitrid 286	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑧 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑧))
18		eqcom 2767	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = 𝑧)
19		fnbrfvb 6938	. . . . . . . . . . . . . . 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 1952	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))))
29		19.21v 1971	. . . . . . . 8 ⊢ (∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)))
30		19.23v 1974	. . . . . . . . . 10 ⊢ (∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))
31		fvex 6901	. . . . . . . . . . . 12 ⊢ (𝐹‘𝑥) ∈ V
32	31	eqvinc 3602	. . . . . . . . . . 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 1955	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))
39		breq1 5105	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥𝐹𝑧 ↔ 𝑦𝐹𝑧))
40	39	mo4 2591	. . . . . . 7 ⊢ (∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦))
41	40	albii 1851	. . . . . 6 ⊢ (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑧∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦))
42		alrot3 2196	. . . . . 6 ⊢ (∀𝑧∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦))
43	41, 42	bitri 278	. . . . 5 ⊢ (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦))
44		r2al 3198	. . . . 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 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ∃*wmo 2562  ∀wral 3076   class class class wbr 5102  dom cdm 5650   Fn wfn 6536  ⟶wf 6537  –1-1→wf1 6538  ‘cfv 6541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6496  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fv 6549

This theorem is used by:  dff13f  7261  f1veqaeq  7262  fpropnf1  7273  dff14a  7276  dff15  7278  f1resrcmplf1d  7281  dff1o6  7285  fcof1  7297  nf1const  7314  soisoi  7338  f1opr  7478  f1o2ndf1  8137  fnwelem  8147  smo11  8377  onelfvnef1  8454  tz7.48lemOLD  8456  omsmo  8672  unxpdomlem3  9254  unfilem2  9303  fofinf1o  9326  inf3lem6  9639  r111  9787  fseqenlem1  10108  fodomacn  10140  alephf1  10169  alephiso  10182  ackbij1lem17  10318  infpssrlem5  10390  fin23lem28  10423  fin1a2lem2  10484  fin1a2lem4  10486  axcc2lem  10519  domtriomlem  10525  cnref1o  13118  injresinj  13931  f1resfz0f1d  13932  om2uzf1oi  14101  ccatf1  14741  swrdf1  14805  cshf1  14967  wwlktovf1  15117  reeff1  16295  bitsf1  16623  crth  16962  eulerthlem2  16966  1arith  17112  vdwlem12  17177  xpsff1o  17746  setcmon  18269  fthestrcsetc  18331  embedsetcestrclem  18338  fthsetcestrc  18346  yoniso  18466  chnpof1  18811  ghmf1  19467  kerf1ghm  19468  orbsta  19534  symgextf1  19642  symgfixf1  19658  odf1  19783  znf1o  21864  cygznlem3  21882  uvcf1  22105  lindff1  22133  mvrf1  22300  ply1sclf1  22615  scmatf1  22853  mdetunilem8  22941  mat2pmatf1  23054  pm2mpf1  23124  ist0-4  24055  ovolicc2lem4  25848  recosf1o  26870  efif1olem4  26880  basellem4  27418  mpodvdsmulf1o  27528  dvdsmulf1o  27530  lgsqrlem2  27681  lgseisenlem2  27710  2lgslem1b  27726  negsf1o  28447  oniso  28664  om2noseqf1o  28694  bdayn0sf1o  28763  axlowdimlem15  29541  upgrwlkdvdelem  30329  wlkswwlksf1o  30475  wwlksnextinj  30495  clwlkclwwlkf1  30608  clwwlkf1  30647  frgrncvvdeqlem8  30914  numclwwlk1lem2f1  30965  pjmf1  32325  unopf1o  32525  2ndresdju  33292  fnpreimac  33313  s3f1  33559  mndlactf1  33635  mndractf1  33637  tocyccntz  33753  extvfvcl  34216  onvfowev  35971  erdszelem9  36052  mrsubff1  36367  msubff1  36409  mvhf1  36412  f1omptsnlem  38366  fvineqsnf1  38440  fvineqsneu  38441  poimirlem26  38671  poimirlem27  38672  grpokerinj  38934  cdleme50f1  41707  dihf11  42431  hashscontpow  43279  hashnexinj  43285  aks6d1c5  43296  sticksstones2  43304  aks6d1c6lem3  43329  fimgmcyc  43705  dnnumch3  44161  wessf1ornlem  46307  projf1o  46318  sumnnodd  46749  dvnprodlem1  47063  fourierdlem34  47258  fourierdlem51  47274  fsetsnf1  48229  cfsetsnfsetf1  48236  fcoresf1  48246  imasetpreimafvbijlemf1  48593  fargshiftf1  48630  sprsymrelf1  48685  prproropf1o  48696  fmtnof1  48727  prmdvdsfmtnof1  48779  uspgrsprf1  49352  1arymaptf1  49861  2arymaptf1  49872  oppff1  50371  diag1f1  50536  diag2f1  50538