Theorem icoshftf1oi 6350

Description: Shifting a closed-below, open-above interval is one-to-one onto. (Contributed by Paul Chapman, 25-Mar-2008.)

Hypotheses

Ref	Expression
icoshftf1o.1	|- F = {<.x, y>. | (x e. (A[,)B) /\ y = (x + C))}
icoshftf1o.2	|- A e. RR
icoshftf1o.3	|- B e. RR
icoshftf1o.4	|- C e. RR

Assertion

Ref	Expression
icoshftf1oi	|- F:(A[,)B)-1-1-onto->((A + C)[,)(B + C))

Distinct variable groups:   x,A,y   x,B,y   x,C,y

Proof of Theorem icoshftf1oi

Step	Hyp	Ref	Expression
1		df-f1o 3192	. 2 |- (F:(A[,)B)-1-1-onto->((A + C)[,)(B + C)) <-> (F:(A[,)B)-1-1->((A + C)[,)(B + C)) /\ F:(A[,)B)-onto->((A + C)[,)(B + C))))
2		f1fv 3865	. . 3 |- (F:(A[,)B)-1-1->((A + C)[,)(B + C)) <-> (F:(A[,)B)-->((A + C)[,)(B + C)) /\ A.z e. (A[,)B)A.w e. (A[,)B)((F` z) = (F` w) -> z = w)))
3		icoshftf1o.1	. . . 4 |- F = {<.x, y>. | (x e. (A[,)B) /\ y = (x + C))}
4		icoshftf1o.2	. . . . 5 |- A e. RR
5		icoshftf1o.3	. . . . 5 |- B e. RR
6		icoshftf1o.4	. . . . 5 |- C e. RR
7		icoshft 6349	. . . . 5 |- ((A e. RR /\ B e. RR /\ C e. RR) -> (x e. (A[,)B) -> (x + C) e. ((A + C)[,)(B + C))))
8	4, 5, 6, 7	mp3an 914	. . . 4 |- (x e. (A[,)B) -> (x + C) e. ((A + C)[,)(B + C)))
9	3, 8	fopab 3818	. . 3 |- F:(A[,)B)-->((A + C)[,)(B + C))
10		opreq1 3959	. . . . . . 7 |- (x = z -> (x + C) = (z + C))
11		oprex 3974	. . . . . . 7 |- (z + C) e. V
12	10, 3, 11	fvopab4 3771	. . . . . 6 |- (z e. (A[,)B) -> (F` z) = (z + C))
13		opreq1 3959	. . . . . . 7 |- (x = w -> (x + C) = (w + C))
14		oprex 3974	. . . . . . 7 |- (w + C) e. V
15	13, 3, 14	fvopab4 3771	. . . . . 6 |- (w e. (A[,)B) -> (F` w) = (w + C))
16	12, 15	eqeqan12d 1487	. . . . 5 |- ((z e. (A[,)B) /\ w e. (A[,)B)) -> ((F` z) = (F` w) <-> (z + C) = (w + C)))
17	6	recn 5294	. . . . . . . 8 |- C e. CC
18		addcan2t 5333	. . . . . . . 8 |- ((z e. CC /\ w e. CC /\ C e. CC) -> ((z + C) = (w + C) <-> z = w))
19	17, 18	mp3an3 903	. . . . . . 7 |- ((z e. CC /\ w e. CC) -> ((z + C) = (w + C) <-> z = w))
20	19	biimpd 153	. . . . . 6 |- ((z e. CC /\ w e. CC) -> ((z + C) = (w + C) -> z = w))
21		elico2t 6331	. . . . . . . . . 10 |- ((A e. RR /\ B e. RR) -> (z e. (A[,)B) <-> (z e. RR /\ A <_ z /\ z < B)))
22	4, 5, 21	mp2an 696	. . . . . . . . 9 |- (z e. (A[,)B) <-> (z e. RR /\ A <_ z /\ z < B))
23	22	biimp 151	. . . . . . . 8 |- (z e. (A[,)B) -> (z e. RR /\ A <_ z /\ z < B))
24	23	3simp1d 793	. . . . . . 7 |- (z e. (A[,)B) -> z e. RR)
25	24	recnd 5295	. . . . . 6 |- (z e. (A[,)B) -> z e. CC)
26		elico2t 6331	. . . . . . . . . 10 |- ((A e. RR /\ B e. RR) -> (w e. (A[,)B) <-> (w e. RR /\ A <_ w /\ w < B)))
27	4, 5, 26	mp2an 696	. . . . . . . . 9 |- (w e. (A[,)B) <-> (w e. RR /\ A <_ w /\ w < B))
28	27	biimp 151	. . . . . . . 8 |- (w e. (A[,)B) -> (w e. RR /\ A <_ w /\ w < B))
29	28	3simp1d 793	. . . . . . 7 |- (w e. (A[,)B) -> w e. RR)
30	29	recnd 5295	. . . . . 6 |- (w e. (A[,)B) -> w e. CC)
31	20, 25, 30	syl2an 454	. . . . 5 |- ((z e. (A[,)B) /\ w e. (A[,)B)) -> ((z + C) = (w + C) -> z = w))
32	16, 31	sylbid 203	. . . 4 |- ((z e. (A[,)B) /\ w e. (A[,)B)) -> ((F` z) = (F` w) -> z = w))
33	32	rgen2a 1696	. . 3 |- A.z e. (A[,)B)A.w e. (A[,)B)((F` z) = (F` w) -> z = w)
34	2, 9, 33	mpbir2an 729	. 2 |- F:(A[,)B)-1-1->((A + C)[,)(B + C))
35		dffo3 3810	. . 3 |- (F:(A[,)B)-onto->((A + C)[,)(B + C)) <-> (F:(A[,)B)-->((A + C)[,)(B + C)) /\ A.z e. ((A + C)[,)(B + C))E.w e. (A[,)B)z = (F` w)))
36		fveq2 3715	. . . . . . 7 |- (w = (z - C) -> (F` w) = (F` (z - C)))
37	36	eqeq2d 1483	. . . . . 6 |- (w = (z - C) -> (z = (F` w) <-> z = (F` (z - C))))
38	37	rcla4ev 1873	. . . . 5 |- (((z - C) e. (A[,)B) /\ z = (F` (z - C))) -> E.w e. (A[,)B)z = (F` w))
39	4, 6	readdcl 5314	. . . . . . . . . 10 |- (A + C) e. RR
40	5, 6	readdcl 5314	. . . . . . . . . 10 |- (B + C) e. RR
41		elico2t 6331	. . . . . . . . . 10 |- (((A + C) e. RR /\ (B + C) e. RR) -> (z e. ((A + C)[,)(B + C)) <-> (z e. RR /\ (A + C) <_ z /\ z < (B + C))))
42	39, 40, 41	mp2an 696	. . . . . . . . 9 |- (z e. ((A + C)[,)(B + C)) <-> (z e. RR /\ (A + C) <_ z /\ z < (B + C)))
43	42	biimp 151	. . . . . . . 8 |- (z e. ((A + C)[,)(B + C)) -> (z e. RR /\ (A + C) <_ z /\ z < (B + C)))
44	43	3simp1d 793	. . . . . . 7 |- (z e. ((A + C)[,)(B + C)) -> z e. RR)
45		recnt 5293	. . . . . . 7 |- (z e. RR -> z e. CC)
46		negsubt 5362	. . . . . . . 8 |- ((z e. CC /\ C e. CC) -> (z + -uC) = (z - C))
47	17, 46	mpan2 695	. . . . . . 7 |- (z e. CC -> (z + -uC) = (z - C))
48	44, 45, 47	3syl 20	. . . . . 6 |- (z e. ((A + C)[,)(B + C)) -> (z + -uC) = (z - C))
49	6	renegcl 5396	. . . . . . . 8 |- -uC e. RR
50		icoshft 6349	. . . . . . . 8 |- (((A + C) e. RR /\ (B + C) e. RR /\ -uC e. RR) -> (z e. ((A + C)[,)(B + C)) -> (z + -uC) e. (((A + C) + -uC)[,)((B + C) + -uC))))
51	39, 40, 49, 50	mp3an 914	. . . . . . 7 |- (z e. ((A + C)[,)(B + C)) -> (z + -uC) e. (((A + C) + -uC)[,)((B + C) + -uC)))
52	39	recn 5294	. . . . . . . . . 10 |- (A + C) e. CC
53	52, 17	negsub 5361	. . . . . . . . 9 |- ((A + C) + -uC) = ((A + C) - C)
54	4	recn 5294	. . . . . . . . . 10 |- A e. CC
55		pncant 5377	. . . . . . . . . 10 |- ((A e. CC /\ C e. CC) -> ((A + C) - C) = A)
56	54, 17, 55	mp2an 696	. . . . . . . . 9 |- ((A + C) - C) = A
57	53, 56	eqtr 1492	. . . . . . . 8 |- ((A + C) + -uC) = A
58	40	recn 5294	. . . . . . . . . 10 |- (B + C) e. CC
59	58, 17	negsub 5361	. . . . . . . . 9 |- ((B + C) + -uC) = ((B + C) - C)
60	5	recn 5294	. . . . . . . . . 10 |- B e. CC
61		pncant 5377	. . . . . . . . . 10 |- ((B e. CC /\ C e. CC) -> ((B + C) - C) = B)
62	60, 17, 61	mp2an 696	. . . . . . . . 9 |- ((B + C) - C) = B
63	59, 62	eqtr 1492	. . . . . . . 8 |- ((B + C) + -uC) = B
64	57, 63	opreq12i 3964	. . . . . . 7 |- (((A + C) + -uC)[,)((B + C) + -uC)) = (A[,)B)
65	51, 64	syl6eleq 1555	. . . . . 6 |- (z e. ((A + C)[,)(B + C)) -> (z + -uC) e. (A[,)B))
66	48, 65	eqeltrrd 1546	. . . . 5 |- (z e. ((A + C)[,)(B + C)) -> (z - C) e. (A[,)B))
67		opreq1 3959	. . . . . . . 8 |- (x = (z - C) -> (x + C) = ((z - C) + C))
68		oprex 3974	. . . . . . . 8 |- ((z - C) + C) e. V
69	67, 3, 68	fvopab4 3771	. . . . . . 7 |- ((z - C) e. (A[,)B) -> (F` (z - C)) = ((z - C) + C))
70	66, 69	syl 10	. . . . . 6 |- (z e. ((A + C)[,)(B + C)) -> (F` (z - C)) = ((z - C) + C))
71		npcant 5379	. . . . . . . 8 |- ((z e. CC /\ C e. CC) -> ((z - C) + C) = z)
72	17, 71	mpan2 695	. . . . . . 7 |- (z e. CC -> ((z - C) + C) = z)
73	44, 45, 72	3syl 20	. . . . . 6 |- (z e. ((A + C)[,)(B + C)) -> ((z - C) + C) = z)
74	70, 73	eqtr2d 1505	. . . . 5 |- (z e. ((A + C)[,)(B + C)) -> z = (F` (z - C)))
75	38, 66, 74	sylanc 471	. . . 4 |- (z e. ((A + C)[,)(B + C)) -> E.w e. (A[,)B)z = (F` w