Theorem ismet 7798

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 3620	. . . . . 6 |- (d = D -> (d:(t X. t)-->RR <-> D:(t X. t)-->RR))
2		opreq 3967	. . . . . . . . . 10 |- (d = D -> (xdy) = (xDy))
3	2	eqeq1d 1483	. . . . . . . . 9 |- (d = D -> ((xdy) = 0 <-> (xDy) = 0))
4	3	bibi1d 619	. . . . . . . 8 |- (d = D -> (((xdy) = 0 <-> x = y) <-> ((xDy) = 0 <-> x = y)))
5		opreq 3967	. . . . . . . . . . 11 |- (d = D -> (zdx) = (zDx))
6		opreq 3967	. . . . . . . . . . 11 |- (d = D -> (zdy) = (zDy))
7	5, 6	opreq12d 3978	. . . . . . . . . 10 |- (d = D -> ((zdx) + (zdy)) = ((zDx) + (zDy)))
8	2, 7	breq12d 2631	. . . . . . . . 9 |- (d = D -> ((xdy) <_ ((zdx) + (zdy)) <-> (xDy) <_ ((zDx) + (zDy))))
9	8	ralbidv 1663	. . . . . . . 8 |- (d = D -> (A.z e. t (xdy) <_ ((zdx) + (zdy)) <-> A.z e. t (xDy) <_ ((zDx) + (zDy))))
10	4, 9	anbi12d 628	. . . . . . 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 1680	. . . . . 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 628	. . . . 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 1279	. . . 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 7793	. . . 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 1900	. . 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 3631	. . . . . . 7 |- (D:(t X. t)-->RR -> dom D = (t X. t))
17		dmeq 3311	. . . . . . . 8 |- (dom D = (t X. t) -> dom dom D = dom ( t X. t))
18		dmxpid 3333	. . . . . . . 8 |- dom ( t X. t) = t
19	17, 18	syl6req 1524	. . . . . . 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 389	. . . . 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 638	. . . 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 1051	. . 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 536	. 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 3358	. . 3 |- (D e. A -> dom D e. V)
26		dmexg 3358	. . 3 |- (dom D e. V -> dom dom D e. V)
27		ismet.1	. . . . . 6 |- X = dom dom D
28	27	eqeq2i 1485	. . . . 5 |- (t = X <-> t = dom dom D)
29		xpeq1 3200	. . . . . . . 8 |- (t = X -> (t X. t) = (X X. t))
30		xpeq2 3201	. . . . . . . 8 |- (t = X -> (X X. t) = (X X. X))
31	29, 30	eqtrd 1507	. . . . . . 7 |- (t = X -> (t X. t) = (X X. X))
32		feq2 3621	. . . . . . 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 1786	. . . . . . . . 9 |- (t = X -> (A.z e. t (xDy) <_ ((zDx) + (zDy)) <-> A.z e. X (xDy) <_ ((zDx) + (zDy))))
35	34	anbi2d 616	. . . . . . . 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 1791	. . . . . . 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 1791	. . . . . 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 628	. . . . 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