Theorem trnij 10637

Description: A translation is 1-1-onto.

Hypothesis

Ref	Expression
trnij.1	|- F = (x e. RR |-> (x + A))

Assertion

Ref	Expression
trnij	|- (A e. RR -> F:RR-1-1-onto->RR)

Distinct variable groups:   x,A   x,F

Proof of Theorem trnij

Step	Hyp	Ref	Expression
1		eqimss 2109	. . . . . . . 8 |- (ran F = RR -> ran F (_ RR)
2	1	anim2i 335	. . . . . . 7 |- ((F Fn RR /\ ran F = RR) -> (F Fn RR /\ ran F (_ RR))
3		trnij.1	. . . . . . . . . 10 |- F = (x e. RR |-> (x + A))
4	3	trdom 10635	. . . . . . . . 9 |- (A e. RR -> dom F = RR)
5	3	cmpfun 10467	. . . . . . . . 9 |- Fun F
6	4, 5	jctil 292	. . . . . . . 8 |- (A e. RR -> (Fun F /\ dom F = RR))
7		df-fn 3193	. . . . . . . 8 |- (F Fn RR <-> (Fun F /\ dom F = RR))
8	6, 7	sylibr 200	. . . . . . 7 |- (A e. RR -> F Fn RR)
9	3	trran 10636	. . . . . . 7 |- (A e. RR -> ran F = RR)
10	2, 8, 9	sylanc 471	. . . . . 6 |- (A e. RR -> (F Fn RR /\ ran F (_ RR))
11		df-f 3194	. . . . . 6 |- (F:RR-->RR <-> (F Fn RR /\ ran F (_ RR))
12	10, 11	sylibr 200	. . . . 5 |- (A e. RR -> F:RR-->RR)
13		axaddrcl 5272	. . . . . . . . . . 11 |- ((x e. RR /\ A e. RR) -> (x + A) e. RR)
14	13	expcom 374	. . . . . . . . . 10 |- (A e. RR -> (x e. RR -> (x + A) e. RR))
15		axaddrcl 5272	. . . . . . . . . . 11 |- ((y e. RR /\ A e. RR) -> (y + A) e. RR)
16	15	expcom 374	. . . . . . . . . 10 |- (A e. RR -> (y e. RR -> (y + A) e. RR))
17	14, 16	anim12d 558	. . . . . . . . 9 |- (A e. RR -> ((x e. RR /\ y e. RR) -> ((x + A) e. RR /\ (y + A) e. RR)))
18	17	imp 350	. . . . . . . 8 |- ((A e. RR /\ (x e. RR /\ y e. RR)) -> ((x + A) e. RR /\ (y + A) e. RR))
19		pm3.27 323	. . . . . . . . . . . 12 |- ((((A e. RR /\ (x e. RR /\ y e. RR)) /\ ((x + A) e. RR /\ (y + A) e. RR)) /\ (F` x) = (F` y)) -> (F` x) = (F` y))
20	3	fveq1i 3725	. . . . . . . . . . . 12 |- (F` x) = ((x e. RR |-> (x + A))` x)
21		df-mpt 4073	. . . . . . . . . . . . . . 15 |- (x e. RR |-> (x + A)) = {<.x, u>. | (x e. RR /\ u = (x + A))}
22		eleq1 1534	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (x e. RR <-> y e. RR))
23	22	adantr 389	. . . . . . . . . . . . . . . . 17 |- ((x = y /\ u = v) -> (x e. RR <-> y e. RR))
24		eqeq1 1481	. . . . . . . . . . . . . . . . . 18 |- (u = v -> (u = (x + A) <-> v = (x + A)))
25		opreq1 3968	. . . . . . . . . . . . . . . . . . 19 |- (x = y -> (x + A) = (y + A))
26	25	eqeq2d 1486	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (v = (x + A) <-> v = (y + A)))
27	24, 26	sylan9bbr 541	. . . . . . . . . . . . . . . . 17 |- ((x = y /\ u = v) -> (u = (x + A) <-> v = (y + A)))
28	23, 27	anbi12d 628	. . . . . . . . . . . . . . . 16 |- ((x = y /\ u = v) -> ((x e. RR /\ u = (x + A)) <-> (y e. RR /\ v = (y + A))))
29	28	cbvopabv 2673	. . . . . . . . . . . . . . 15 |- {<.x, u>. | (x e. RR /\ u = (x + A))} = {<.y, v>. | (y e. RR /\ v = (y + A))}
30	3, 21, 29	3eqtr 1499	. . . . . . . . . . . . . 14 |- F = {<.y, v>. | (y e. RR /\ v = (y + A))}
31		df-mpt 4073	. . . . . . . . . . . . . 14 |- (y e. RR |-> (y + A)) = {<.y, v>. | (y e. RR /\ v = (y + A))}
32	30, 31	eqtr4 1498	. . . . . . . . . . . . 13 |- F = (y e. RR |-> (y + A))
33	32	fveq1i 3725	. . . . . . . . . . . 12 |- (F` y) = ((y e. RR |-> (y + A))` y)
34	19, 20, 33	3eqtr3g 1530	. . . . . . . . . . 11 |- ((((A e. RR /\ (x e. RR /\ y e. RR)) /\ ((x + A) e. RR /\ (y + A) e. RR)) /\ (F` x) = (F` y)) -> ((x e. RR |-> (x + A))` x) = ((y e. RR |-> (y + A))` y))
35		fvopab2a 10463	. . . . . . . . . . . 12 |- ((x e. RR /\ (x + A) e. RR) -> ((x e. RR |-> (x + A))` x) = (x + A))
36		simprl 414	. . . . . . . . . . . . 13 |- ((A e. RR /\ (x e. RR /\ y e. RR)) -> x e. RR)
37	36	ad2antrr 404	. . . . . . . . . . . 12 |- ((((A e. RR /\ (x e. RR /\ y e. RR)) /\ ((x + A) e. RR /\ (y + A) e. RR)) /\ (F` x) = (F` y)) -> x e. RR)
38		pm3.26 319	. . . . . . . . . . . . 13 |- (((x + A) e. RR /\ (y + A) e. RR) -> (x + A) e. RR)
39	38	ad2antlr 405	. . . . . . . . . . . 12 |- ((((A e. RR /\ (x e. RR /\ y e. RR)) /\ ((x + A) e. RR /\ (y + A) e. RR)) /\ (F` x) = (F` y)) -> (x + A) e. RR)
40	35, 37, 39	sylanc 471	. . . . . . . . . . 11 |- ((((A e. RR /\ (x e. RR /\ y e. RR)) /\ ((x + A) e. RR /\ (y + A) e. RR)) /\ (F` x) = (F` y)) -> ((x e. RR |-> (x + A))` x) = (x + A))
41		simprr 415	. . . . . . . . . . . . . . 15 |- ((A e. RR /\ (x e. RR /\ y e. RR)) -> y e. RR)
42	41	adantr 389	. . . . . . . . . . . . . 14 |- (((A e. RR /\ (x e. RR /\ y e. RR)) /\ ((x + A) e. RR /\ (y + A) e. RR)) -> y e. RR)
43		simprr 415	. . . . . . . . . . . . . 14 |- (((A e. RR /\ (x e. RR /\ y e. RR)) /\ ((x + A) e. RR /\ (y + A) e. RR)) -> (y + A) e. RR)
44	42, 43	jca 288	. . . . . . . . . . . . 13 |- (((A e. RR /\ (x e. RR /\ y e. RR)) /\ ((x + A) e. RR /\ (y + A) e. RR)) -> (y e. RR /\ (y + A) e. RR))
45	44	adantr 389	. . . . . . . . . . . 12 |- ((((A e. RR /\ (x e. RR /\ y e. RR)) /\ ((x + A) e. RR /\ (y + A) e. RR)) /\ (F` x) = (F` y)) -> (y e. RR /\ (y + A) e. RR))
46		fvopab2a 10463	. . . . . . . . . . . 12 |- ((y e. RR /\ (y + A) e. RR) -> ((y e. RR |-> (y + A))` y) = (y + A))
47	45, 46	syl 10	. . . . . . . . . . 11 |- ((((A e. RR /\ (x e. RR /\ y e. RR)) /\ ((x + A) e. RR /\ (y + A) e. RR)) /\ (F` x) = (F` y)) -> ((y e. RR |-> (y + A))` y) = (y + A))
48	34, 40, 47	3eqtr3d 1515	. . . . . . . . . 10 |- ((((A e. RR /\ (x e. RR /\ y e. RR)) /\ ((x + A) e. RR /\ (y + A) e. RR)) /\ (F` x) = (F` y)) -> (x + A) = (y + A))
49		recnt 5313	. . . . . . . . . . . . . 14 |- (x e. RR -> x e. CC)
50	49	ad2antrl 406	. . . . . . . . . . . . 13 |- ((A e. RR /\ (x e. RR /\ y e. RR)) -> x e. CC)
51		recnt 5313	. . . . . . . . . . . . . 14 |- (y e. RR -> y e. CC)
52	51	ad2antll 407	. . . . . . . . . . . . 13 |- ((A e. RR /\ (x e. RR /\ y e. RR)) -> y e. CC)
53		recnt 5313	. . . . . . . . . . . . . 14 |- (A e. RR -> A e. CC)
54	53	adantr 389	. . . . . . . . . . . . 13 |- ((A e. RR /\ (x e. RR /\ y e. RR)) -> A e. CC)
55	50, 52, 54	3jca 819	. . . . . . . . . . . 12 |- ((A e. RR /\ (x e. RR /\ y e. RR)) -> (x e. CC /\ y e. CC /\ A e. CC))
56	55	ad2antrr 404	. . . . . . . . . . 11 |- ((((A e. RR /\ (x e. RR /\ y e. RR)) /\ ((x + A) e. RR /\ (y + A) e. RR)) /\ (F` x) = (F` y)) -> (x e. CC /\ y e. CC /\ A e. CC))
57		addcan2t 5353	. . . . . . . . . . 11 |- ((x e. CC /\ y e. CC /\ A e. CC) -> ((x + A) = (y + A) <-> x = y))
58	56, 57	syl 10	. . . . . . . . . 10 |- ((((A e. RR /\ (x e. RR /\ y e. RR)) /\ ((x + A) e. RR /\ (y + A) e. RR)) /\ (F` x) = (F` y)) -> ((x + A) = (y + A) <-> x = y))
59	48, 58	mpbid 195	. . . . . . . . 9 |- ((((A e. RR /\ (x e. RR /\ y e. RR)) /\ ((x + A) e. RR /\ (y + A) e. RR)) /\ (F` x) = (F` y)) -> x = y)
60	59	exp31 376	. . . . . . . 8 |- ((A e. RR /\ (x e. RR /\ y e. RR)) -> (((x + A) e. RR /\ (y + A) e. RR) -> ((F` x) = (F` y) -> x = y)))
61	18, 60	mpd 26	. . . . . . 7 |- ((A e. RR /\ (x e. RR /\ y e. RR)) -> ((F` x) = (F` y) -> x = y))
62	61