Theorem dff13 5811

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 5458	. 2 |- ( F : A -1-1-> B <-> ( F : A --> B /\ A. z E* x x F z ) )
2		ffn 5403	. . . 4 |- ( F : A --> B -> F Fn A )
3		vex 2763	. . . . . . . . . . . . . . 15 |- x e. _V
4		vex 2763	. . . . . . . . . . . . . . 15 |- z e. _V
5	3, 4	breldm 4866	. . . . . . . . . . . . . 14 |- ( x F z -> x e. dom F )
6		fndm 5353	. . . . . . . . . . . . . . 15 |- ( F Fn A -> dom F = A )
7	6	eleq2d 2263	. . . . . . . . . . . . . 14 |- ( F Fn A -> ( x e. dom F <-> x e. A ) )
8	5, 7	imbitrid 154	. . . . . . . . . . . . 13 |- ( F Fn A -> ( x F z -> x e. A ) )
9		vex 2763	. . . . . . . . . . . . . . 15 |- y e. _V
10	9, 4	breldm 4866	. . . . . . . . . . . . . 14 |- ( y F z -> y e. dom F )
11	6	eleq2d 2263	. . . . . . . . . . . . . 14 |- ( F Fn A -> ( y e. dom F <-> y e. A ) )
12	10, 11	imbitrid 154	. . . . . . . . . . . . 13 |- ( F Fn A -> ( y F z -> y e. A ) )
13	8, 12	anim12d 335	. . . . . . . . . . . 12 |- ( F Fn A -> ( ( x F z /\ y F z ) -> ( x e. A /\ y e. A ) ) )
14	13	pm4.71rd 394	. . . . . . . . . . 11 |- ( F Fn A -> ( ( x F z /\ y F z ) <-> ( ( x e. A /\ y e. A ) /\ ( x F z /\ y F z ) ) ) )
15		eqcom 2195	. . . . . . . . . . . . . . 15 |- ( z = ( F ` x ) <-> ( F ` x ) = z )
16		fnbrfvb 5597	. . . . . . . . . . . . . . 15 |- ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = z <-> x F z ) )
17	15, 16	bitrid 192	. . . . . . . . . . . . . 14 |- ( ( F Fn A /\ x e. A ) -> ( z = ( F ` x ) <-> x F z ) )
18		eqcom 2195	. . . . . . . . . . . . . . 15 |- ( z = ( F ` y ) <-> ( F ` y ) = z )
19		fnbrfvb 5597	. . . . . . . . . . . . . . 15 |- ( ( F Fn A /\ y e. A ) -> ( ( F ` y ) = z <-> y F z ) )
20	18, 19	bitrid 192	. . . . . . . . . . . . . 14 |- ( ( F Fn A /\ y e. A ) -> ( z = ( F ` y ) <-> y F z ) )
21	17, 20	bi2anan9 606	. . . . . . . . . . . . 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 592	. . . . . . . . . . . 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 452	. . . . . . . . . . 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 191	. . . . . . . . . 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 231	. . . . . . . . 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 263	. . . . . . . . 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	bitrdi 196	. . . . . . . 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 1835	. . . . . . 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 1884	. . . . . . . 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 1894	. . . . . . . . . . 11 |- ( A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) <-> ( E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) )
31		funfvex 5571	. . . . . . . . . . . . . 14 |- ( ( Fun F /\ x e. dom F ) -> ( F ` x ) e. _V )
32	31	funfni 5354	. . . . . . . . . . . . 13 |- ( ( F Fn A /\ x e. A ) -> ( F ` x ) e. _V )
33		eqvincg 2884	. . . . . . . . . . . . 13 |- ( ( F ` x ) e. _V -> ( ( F ` x ) = ( F ` y ) <-> E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) ) )
34	32, 33	syl 14	. . . . . . . . . . . 12 |- ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = ( F ` y ) <-> E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) ) )
35	34	imbi1d 231	. . . . . . . . . . 11 |- ( ( F Fn A /\ x e. A ) -> ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) ) )
36	30, 35	bitr4id 199	. . . . . . . . . 10 |- ( ( F Fn A /\ x e. A ) -> ( A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) <-> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
37	36	adantrr 479	. . . . . . . . 9 |- ( ( F Fn A /\ ( x e. A /\ y e. A ) ) -> ( A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) <-> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
38	37	pm5.74da 443	. . . . . . . 8 |- ( F Fn A -> ( ( ( 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 ) ) ) )
39	29, 38	bitrid 192	. . . . . . 7 |- ( F Fn A -> ( 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 ) ) ) )
40	28, 39	bitrd 188	. . . . . 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 ) ) ) )
41	40	2albidv 1878	. . . . 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 ) ) ) )
42		breq1 4032	. . . . . . . 8 |- ( x = y -> ( x F z <-> y F z ) )
43	42	mo4 2103	. . . . . . 7 |- ( E* x x F z <-> A. x A. y ( ( x F z /\ y F z ) -> x = y ) )
44	43	albii 1481	. . . . . 6 |- ( A. z E* x x F z <-> A. z A. x A. y ( ( x F z /\ y F z ) -> x = y ) )
45		alrot3 1496	. . . . . 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 ) )
46	44, 45	bitri 184	. . . . 5 |- ( A. z E* x x F z <-> A. x A. y A. z ( ( x F z /\ y F z ) -> x = y ) )
47		r2al 2513	. . . . 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 ) ) )
48	41, 46, 47	3bitr4g 223	. . . 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 ) ) )
49	2, 48	syl 14	. . 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 ) ) )
50	49	pm5.32i 454	. 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 ) ) )
51	1, 50	bitri 184	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   /\ wa 104   <-> wb 105   A.wal 1362   = wceq 1364   E.wex 1503   E*wmo 2043   e. wcel 2164   A.wral 2472   _Vcvv 2760   class class class wbr 4029   dom cdm 4659   Fn wfn 5249   -->wf 5250   -1-1->wf1 5251   ` cfv 5254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-sbc 2986  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fv 5262

This theorem is referenced by:  f1veqaeq  5812  dff13f  5813  dff1o6  5819  fcof1  5826  f1o2ndf1  6281  cc2lem  7326  cnref1o  9716  frec2uzf1od  10477  iseqf1olemqf1o  10577  reeff1  11843  crth  12362  eulerthlemh  12369  1arith  12505  nninfdclemf1  12609  xpsff1o  12932  ghmf1  13343  kerf1ghm  13344  znf1o  14139  ioocosf1o  14989  gausslemma2dlem1f1o  15176  lgseisenlem2  15187  peano4nninf  15496  exmidsbthrlem  15512