Theorem f1opr 15714

Description: Condition for an operation to be one-to-one.

Assertion

Ref	Expression
f1opr	|- (F:(A X. B)-1-1->C <-> (F:(A X. B)-->C /\ A.r e. A A.s e. B A.t e. A A.u e. B ((rFs) = (tFu) -> (r = t /\ s = u))))

Distinct variable groups:   A,r,s,t,u   B,r,s,t,u   F,r,s,t,u

Proof of Theorem f1opr

Step	Hyp	Ref	Expression
1		dff13 4850	. 2 |- (F:(A X. B)-1-1->C <-> (F:(A X. B)-->C /\ A.v e. (A X. B)A.w e. (A X. B)((F` v) = (F` w) -> v = w)))
2		fveq2 4681	. . . . . . . . 9 |- (v = <.r, s>. -> (F` v) = (F` <.r, s>.))
3		df-opr 4886	. . . . . . . . 9 |- (rFs) = (F` <.r, s>.)
4	2, 3	syl6eqr 1946	. . . . . . . 8 |- (v = <.r, s>. -> (F` v) = (rFs))
5	4	eqeq1d 1892	. . . . . . 7 |- (v = <.r, s>. -> ((F` v) = (F` w) <-> (rFs) = (F` w)))
6		eqeq1 1890	. . . . . . 7 |- (v = <.r, s>. -> (v = w <-> <.r, s>. = w))
7	5, 6	imbi12d 688	. . . . . 6 |- (v = <.r, s>. -> (((F` v) = (F` w) -> v = w) <-> ((rFs) = (F` w) -> <.r, s>. = w)))
8	7	ralbidv 2123	. . . . 5 |- (v = <.r, s>. -> (A.w e. (A X. B)((F` v) = (F` w) -> v = w) <-> A.w e. (A X. B)((rFs) = (F` w) -> <.r, s>. = w)))
9	8	ralxp 4041	. . . 4 |- (A.v e. (A X. B)A.w e. (A X. B)((F` v) = (F` w) -> v = w) <-> A.r e. A A.s e. B A.w e. (A X. B)((rFs) = (F` w) -> <.r, s>. = w))
10		fveq2 4681	. . . . . . . . 9 |- (w = <.t, u>. -> (F` w) = (F` <.t, u>.))
11		df-opr 4886	. . . . . . . . 9 |- (tFu) = (F` <.t, u>.)
12	10, 11	syl6eqr 1946	. . . . . . . 8 |- (w = <.t, u>. -> (F` w) = (tFu))
13	12	eqeq2d 1895	. . . . . . 7 |- (w = <.t, u>. -> ((rFs) = (F` w) <-> (rFs) = (tFu)))
14		eqeq2 1893	. . . . . . . 8 |- (w = <.t, u>. -> (<.r, s>. = w <-> <.r, s>. = <.t, u>.))
15		visset 2295	. . . . . . . . 9 |- r e. _V
16		visset 2295	. . . . . . . . 9 |- s e. _V
17		visset 2295	. . . . . . . . 9 |- u e. _V
18	15, 16, 17	opth 3532	. . . . . . . 8 |- (<.r, s>. = <.t, u>. <-> (r = t /\ s = u))
19	14, 18	syl6bb 595	. . . . . . 7 |- (w = <.t, u>. -> (<.r, s>. = w <-> (r = t /\ s = u)))
20	13, 19	imbi12d 688	. . . . . 6 |- (w = <.t, u>. -> (((rFs) = (F` w) -> <.r, s>. = w) <-> ((rFs) = (tFu) -> (r = t /\ s = u))))
21	20	ralxp 4041	. . . . 5 |- (A.w e. (A X. B)((rFs) = (F` w) -> <.r, s>. = w) <-> A.t e. A A.u e. B ((rFs) = (tFu) -> (r = t /\ s = u)))
22	21	2ralbii 2129	. . . 4 |- (A.r e. A A.s e. B A.w e. (A X. B)((rFs) = (F` w) -> <.r, s>. = w) <-> A.r e. A A.s e. B A.t e. A A.u e. B ((rFs) = (tFu) -> (r = t /\ s = u)))
23	9, 22	bitri 190	. . 3 |- (A.v e. (A X. B)A.w e. (A X. B)((F` v) = (F` w) -> v = w) <-> A.r e. A A.s e. B A.t e. A A.u e. B ((rFs) = (tFu) -> (r = t /\ s = u)))
24	23	anbi2i 538	. 2 |- ((F:(A X. B)-->C /\ A.v e. (A X. B)A.w e. (A X. B)((F` v) = (F` w) -> v = w)) <-> (F:(A X. B)-->C /\ A.r e. A A.s e. B A.t e. A A.u e. B ((rFs) = (tFu) -> (r = t /\ s = u))))
25	1, 24	bitri 190	1 |- (F:(A X. B)-1-1->C <-> (F:(A X. B)-->C /\ A.r e. A A.s e. B A.t e. A A.u e. B ((rFs) = (tFu) -> (r = t /\ s = u))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298  A.wral 2105  <.cop 3046   X. cxp 3984  -->wf 3994  -1-1->wf1 3995  ` cfv 3998  (class class class)co 4884

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fv 4014  df-opr 4886

Copyright terms: Public domain