Theorem metreslem 7822

Description: Lemma for metres 7823. (Contributed by FL, 10-Nov-2006.)

Hypotheses

Ref	Expression
metf.1	|- X = dom dom D
metreslem.2	|- A = dom dom ( D |` (R X. R))

Assertion

Ref	Expression
metreslem	|- ((D e. Met /\ R (_ X) -> (D |` (R X. R)) e. Met)

Proof of Theorem metreslem

Step	Hyp	Ref	Expression
1		fssres 3643	. . . . . 6 |- ((D:(X X. X)-->RR /\ (R X. R) (_ (X X. X)) -> (D |` (R X. R)):(R X. R)-->RR)
2		ssxp 3256	. . . . . . 7 |- ((R (_ X /\ R (_ X) -> (R X. R) (_ (X X. X))
3	2	anidms 434	. . . . . 6 |- (R (_ X -> (R X. R) (_ (X X. X))
4	1, 3	sylan2 451	. . . . 5 |- ((D:(X X. X)-->RR /\ R (_ X) -> (D |` (R X. R)):(R X. R)-->RR)
5		ssel 2063	. . . . . . . . 9 |- (R (_ X -> (x e. R -> x e. X))
6		ssel 2063	. . . . . . . . . . 11 |- (R (_ X -> (y e. R -> y e. X))
7		ssralv 2114	. . . . . . . . . . . 12 |- (R (_ X -> (A.z e. X (xDy) <_ ((zDx) + (zDy)) -> A.z e. R (xDy) <_ ((zDx) + (zDy))))
8	7	anim2d 561	. . . . . . . . . . 11 |- (R (_ X -> ((((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))) -> (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy)))))
9	6, 8	imim12d 29	. . . . . . . . . 10 |- (R (_ X -> ((y e. X -> (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy)))) -> (y e. R -> (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy))))))
10	9	r19.20dv2 1711	. . . . . . . . 9 |- (R (_ X -> (A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))) -> A.y e. R (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy)))))
11	5, 10	imim12d 29	. . . . . . . 8 |- (R (_ X -> ((x e. X -> A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy)))) -> (x e. R -> A.y e. R (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy))))))
12	11	r19.20dv2 1711	. . . . . . 7 |- (R (_ X -> (A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))) -> A.x e. R A.y e. R (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy)))))
13		oprvalres 4033	. . . . . . . . . . . 12 |- ((x e. R /\ y e. R) -> (x(D |` (R X. R))y) = (xDy))
14	13	eqeq1d 1483	. . . . . . . . . . 11 |- ((x e. R /\ y e. R) -> ((x(D |` (R X. R))y) = 0 <-> (xDy) = 0))
15	14	bibi1d 619	. . . . . . . . . 10 |- ((x e. R /\ y e. R) -> (((x(D |` (R X. R))y) = 0 <-> x = y) <-> ((xDy) = 0 <-> x = y)))
16	13	adantl 388	. . . . . . . . . . . . 13 |- ((z e. R /\ (x e. R /\ y e. R)) -> (x(D |` (R X. R))y) = (xDy))
17		oprvalres 4033	. . . . . . . . . . . . . . 15 |- ((z e. R /\ x e. R) -> (z(D |` (R X. R))x) = (zDx))
18		oprvalres 4033	. . . . . . . . . . . . . . 15 |- ((z e. R /\ y e. R) -> (z(D |` (R X. R))y) = (zDy))
19	17, 18	opreqan12d 3979	. . . . . . . . . . . . . 14 |- (((z e. R /\ x e. R) /\ (z e. R /\ y e. R)) -> ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)) = ((zDx) + (zDy)))
20	19	anandis 512	. . . . . . . . . . . . 13 |- ((z e. R /\ (x e. R /\ y e. R)) -> ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)) = ((zDx) + (zDy)))
21	16, 20	breq12d 2631	. . . . . . . . . . . 12 |- ((z e. R /\ (x e. R /\ y e. R)) -> ((x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)) <-> (xDy) <_ ((zDx) + (zDy))))
22	21	ancoms 436	. . . . . . . . . . 11 |- (((x e. R /\ y e. R) /\ z e. R) -> ((x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)) <-> (xDy) <_ ((zDx) + (zDy))))
23	22	ralbidva 1659	. . . . . . . . . 10 |- ((x e. R /\ y e. R) -> (A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)) <-> A.z e. R (xDy) <_ ((zDx) + (zDy))))
24	15, 23	anbi12d 628	. . . . . . . . 9 |- ((x e. R /\ y e. R) -> ((((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))) <-> (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy)))))
25	24	ralbidva 1659	. . . . . . . 8 |- (x e. R -> (A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))) <-> A.y e. R (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy)))))
26	25	ralbiia 1673	. . . . . . 7 |- (A.x e. R A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))) <-> A.x e. R A.y e. R (((xDy) = 0 <-> x = y) /\ A.z e. R (xDy) <_ ((zDx) + (zDy))))
27	12, 26	syl6ibr 213	. . . . . 6 |- (R (_ X -> (A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))) -> A.x e. R A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y)))))
28	27	impcom 351	. . . . 5 |- ((A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))) /\ R (_ X) -> A.x e. R A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (R X. R))y) <_ ((z(D |` (R X. R))x) + (z(D |` (R X. R))y))))
29	4, 28	anim12i 333	. . . 4 |- (((D:(X X. X)-->RR /\ R (_ X) /\ (A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))) /\ R (_ X)) -> ((D |` (R X. R)):(R X. R)-->RR /\ A.x e. R A.y e. R (((x(D |` (R X. R))y) = 0 <-> x = y) /\ A.z e. R (x(D |` (