Theorem ismet 7795

Description: Express the predicate "D is a metric."

Hypothesis

Ref	Expression
ismet.1	|- X = dom dom D

Assertion

Ref	Expression
ismet	|- (D e. A -> (D e. Met <-> (D:(X X. X)-->RR /\ A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))))))

Distinct variable groups:   x,y,z,D   x,X,y,z

Proof of Theorem ismet

Step	Hyp	Ref	Expression
1		feq1 3626	. . . . . 6 |- (d = D -> (d:(t X. t)-->RR <-> D:(t X. t)-->RR))
2		opreq 3973	. . . . . . . . . 10 |- (d = D -> (xdy) = (xDy))
3	2	eqeq1d 1486	. . . . . . . . 9 |- (d = D -> ((xdy) = 0 <-> (xDy) = 0))
4	3	bibi1d 621	. . . . . . . 8 |- (d = D -> (((xdy) = 0 <-> x = y) <-> ((xDy) = 0 <-> x = y)))
5		opreq 3973	. . . . . . . . . . 11 |- (d = D -> (zdx) = (zDx))
6		opreq 3973	. . . . . . . . . . 11 |- (d = D -> (zdy) = (zDy))
7	5, 6	opreq12d 3984	. . . . . . . . . 10 |- (d = D -> ((zdx) + (zdy)) = ((zDx) + (zDy)))
8	2, 7	breq12d 2636	. . . . . . . . 9 |- (d = D -> ((xdy) <_ ((zdx) + (zdy)) <-> (xDy) <_ ((zDx) + (zDy))))
9	8	ralbidv 1666	. . . . . . . 8 |- (d = D -> (A.z e. t (xdy) <_ ((zdx) + (zdy)) <-> A.z e. t (xDy) <_ ((zDx) + (zDy))))
10	4, 9	anbi12d 630	. . . . . . 7 |- (d = D -> ((((xdy) = 0 <-> x = y) /\ A.z e. t (xdy) <_ ((zdx) + (zdy))) <-> (((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy)))))
11	10	2ralbidv 1683	. . . . . 6 |- (d = D -> (A.x e. t A.y e. t (((xdy) = 0 <-> x = y) /\ A.z e. t (xdy) <_ ((zdx) + (zdy))) <-> A.x e. t A.y e. t (((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy)))))
12	1, 11	anbi12d 630	. . . . 5 |- (d = D -> ((d:(t X. t)-->RR /\ A.x e. t A.y e. t (((xdy) = 0 <-> x = y) /\ A.z e. t (xdy) <_ ((zdx) + (zdy)))) <-> (D:(t X. t)-->RR /\ A.x e. t A.y e. t (((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy))))))
13	12	exbidv 1281	. . . 4 |- (d = D -> (E.t(d:(t X. t)-->RR /\ A.x e. t A.y e. t (((xdy) = 0 <-> x = y) /\ A.z e. t (xdy) <_ ((zdx) + (zdy)))) <-> E.t(D:(t X. t)-->RR /\ A.x e. t A.y e. t (((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy))))))
14		df-met 7790	. . . 4 |- Met = {d | E.t(d:(t X. t)-->RR /\ A.x e. t A.y e. t (((xdy) = 0 <-> x = y) /\ A.z e. t (xdy) <_ ((zdx) + (zdy))))}
15	13, 14	elab2g 1903	. . 3 |- (D e. A -> (D e. Met <-> E.t(D:(t X. t)-->RR /\ A.x e. t A.y e. t (((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy))))))
16		fdm 3637	. . . . . . 7 |- (D:(t X. t)-->RR -> dom D = (t X. t))
17		dmeq 3317	. . . . . . . 8 |- (dom D = (t X. t) -> dom dom D = dom ( t X. t))
18		dmxpid 3339	. . . . . . . 8 |- dom ( t X. t) = t
19	17, 18	syl6req 1527	. . . . . . 7 |- (dom D = (t X. t) -> t = dom dom D)
20	16, 19	syl 10	. . . . . 6 |- (D:(t X. t)-->RR -> t = dom dom D)
21	20	adantr 391	. . . . 5 |- ((D:(t X. t)-->RR /\ A.x e. t A.y e. t (((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy)))) -> t = dom dom D)
22	21	pm4.71ri 640	. . . 4 |- ((D:(t X. t)-->RR /\ A.x e. t A.y e. t (((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy)))) <-> (t = dom dom D /\ (D:(t X. t)-->RR /\ A.x e. t A.y e. t (((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy))))))
23	22	exbii 1053	. . 3 |- (E.t(D:(t X. t)-->RR /\ A.x e. t A.y e. t (((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy)))) <-> E.t(t = dom dom D /\ (D:(t X. t)-->RR /\ A.x e. t A.y e. t (((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy))))))
24	15, 23	syl6bb 538	. 2 |- (D e. A -> (D e. Met <-> E.t(t = dom dom D /\ (D:(t X. t)-->RR /\ A.x e. t A.y e. t (((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy)))))))
25		dmexg 3364	. . 3 |- (D e. A -> dom D e. V)
26		dmexg 3364	. . 3 |- (dom D e. V -> dom dom D e. V)
27		ismet.1	. . . . . 6 |- X = dom dom D
28	27	eqeq2i 1488	. . . . 5 |- (t = X <-> t = dom dom D)
29		xpeq1 3206	. . . . . . . 8 |- (t = X -> (t X. t) = (X X. t))
30		xpeq2 3207	. . . . . . . 8 |- (t = X -> (X X. t) = (X X. X))
31	29, 30	eqtrd 1510	. . . . . . 7 |- (t = X -> (t X. t) = (X X. X))
32		feq2 3627	. . . . . . 7 |- ((t X. t) = (X X. X) -> (D:(t X. t)-->RR <-> D:(X X. X)-->RR))
33	31, 32	syl 10	. . . . . 6 |- (t = X -> (D:(t X. t)-->RR <-> D:(X X. X)-->RR))
34		raleq1 1789	. . . . . . . . 9 |- (t = X -> (A.z e. t (xDy) <_ ((zDx) + (zDy)) <-> A.z e. X (xDy) <_ ((zDx) + (zDy))))
35	34	anbi2d 618	. . . . . . . 8 |- (t = X -> ((((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy))) <-> (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy)))))
36	35	raleqd 1794	. . . . . . 7 |- (t = X -> (A.y e. t (((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy))) <-> A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy)))))
37	36	raleqd 1794	. . . . . 6 |- (t = X -> (A.x e. t A.y e. t (((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy))) <-> A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy)))))
38	33, 37	anbi12d 630	. . . . 5 |- (t = X -> ((D:(t X. t)-->RR /\ A.x e. t A.y e. t (((xDy) = 0 <-> x = y) /\ A.z e. t (xDy) <_ ((zDx) + (zDy)))) <-> (D:(X X. X)-->RR /\ A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))))))
39	28, 38	sylbir 201	. . . 4 |- (t = dom dom D -> ((D:(t X. t)-->RR