Theorem ismsg 7797

Description: Express the predicate "<.X, D>. is a metric space" with underlying set X and distance function D.

Assertion

Ref	Expression
ismsg	|- (D e. A -> (<.X, D>. e. MetSp <-> (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,X   x,D,y,z

Proof of Theorem ismsg

Step	Hyp	Ref	Expression
1		df-br 2625	. . . . 5 |- (XMetSpD <-> <.X, D>. e. MetSp)
2		msrel 7794	. . . . . 6 |- Rel MetSp
3	2	brrelexi 3214	. . . . 5 |- (XMetSpD -> X e. V)
4	1, 3	sylbir 201	. . . 4 |- (<.X, D>. e. MetSp -> X e. V)
5	4	anim1i 334	. . 3 |- ((<.X, D>. e. MetSp /\ D e. A) -> (X e. V /\ D e. A))
6	5	ancoms 438	. 2 |- ((D e. A /\ <.X, D>. e. MetSp) -> (X e. V /\ D e. A))
7		dmfex 3661	. . . . 5 |- ((D e. A /\ D:(X X. X)-->RR) -> (X X. X) e. V)
8		xpexr 3485	. . . . . 6 |- ((X X. X) e. V -> (X e. V \/ X e. V))
9		oridm 243	. . . . . 6 |- ((X e. V \/ X e. V) <-> X e. V)
10	8, 9	sylib 198	. . . . 5 |- ((X X. X) e. V -> X e. V)
11	7, 10	syl 10	. . . 4 |- ((D e. A /\ D:(X X. X)-->RR) -> X e. V)
12		pm3.26 319	. . . 4 |- ((D e. A /\ D:(X X. X)-->RR) -> D e. A)
13	11, 12	jca 288	. . 3 |- ((D e. A /\ D:(X X. X)-->RR) -> (X e. V /\ D e. A))
14	13	adantrr 397	. 2 |- ((D e. A /\ (D:(X X. X)-->RR /\ A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))))) -> (X e. V /\ D e. A))
15		xpeq1 3206	. . . . . . 7 |- (w = X -> (w X. w) = (X X. w))
16		xpeq2 3207	. . . . . . 7 |- (w = X -> (X X. w) = (X X. X))
17	15, 16	eqtrd 1510	. . . . . 6 |- (w = X -> (w X. w) = (X X. X))
18		feq2 3627	. . . . . 6 |- ((w X. w) = (X X. X) -> (v:(w X. w)-->RR <-> v:(X X. X)-->RR))
19	17, 18	syl 10	. . . . 5 |- (w = X -> (v:(w X. w)-->RR <-> v:(X X. X)-->RR))
20		raleq1 1789	. . . . . . . 8 |- (w = X -> (A.z e. w (xvy) <_ ((zvx) + (zvy)) <-> A.z e. X (xvy) <_ ((zvx) + (zvy))))
21	20	anbi2d 618	. . . . . . 7 |- (w = X -> ((((xvy) = 0 <-> x = y) /\ A.z e. w (xvy) <_ ((zvx) + (zvy))) <-> (((xvy) = 0 <-> x = y) /\ A.z e. X (xvy) <_ ((zvx) + (zvy)))))
22	21	raleqd 1794	. . . . . 6 |- (w = X -> (A.y e. w (((xvy) = 0 <-> x = y) /\ A.z e. w (xvy) <_ ((zvx) + (zvy))) <-> A.y e. X (((xvy) = 0 <-> x = y) /\ A.z e. X (xvy) <_ ((zvx) + (zvy)))))
23	22	raleqd 1794	. . . . 5 |- (w = X -> (A.x e. w A.y e. w (((xvy) = 0 <-> x = y) /\ A.z e. w (xvy) <_ ((zvx) + (zvy))) <-> A.x e. X A.y e. X (((xvy) = 0 <-> x = y) /\ A.z e. X (xvy) <_ ((zvx) + (zvy)))))
24	19, 23	anbi12d 630	. . . 4 |- (w = X -> ((v:(w X. w)-->RR /\ A.x e. w A.y e. w (((xvy) = 0 <-> x = y) /\ A.z e. w (xvy) <_ ((zvx) + (zvy)))) <-> (v:(X X. X)-->RR /\ A.x e. X A.y e. X (((xvy) = 0 <-> x = y) /\ A.z e. X (xvy) <_ ((zvx) + (zvy))))))
25		feq1 3626	. . . . 5 |- (v = D -> (v:(X X. X)-->RR <-> D:(X X. X)-->RR))
26		opreq 3973	. . . . . . . . 9 |- (v = D -> (xvy) = (xDy))
27	26	eqeq1d 1486	. . . . . . . 8 |- (v = D -> ((xvy) = 0 <-> (xDy) = 0))
28	27	bibi1d 621	. . . . . . 7 |- (v = D -> (((xvy) = 0 <-> x = y) <-> ((xDy) = 0 <-> x = y)))
29		opreq 3973	. . . . . . . . . 10 |- (v = D -> (zvx) = (zDx))
30		opreq 3973	. . . . . . . . . 10 |- (v = D -> (zvy) = (zDy))
31	29, 30	opreq12d 3984	. . . . . . . . 9 |- (v = D -> ((zvx) + (zvy)) = ((zDx) + (zDy)))
32	26, 31	breq12d 2636	. . . . . . . 8 |- (v = D -> ((xvy) <_ ((zvx) + (zvy)) <-> (xDy) <_ ((zDx) + (zDy))))
33	32	ralbidv 1666	. . . . . . 7 |- (v = D -> (A.z e. X (xvy) <_ ((zvx) + (zvy)) <-> A.z e. X (xDy) <_ ((zDx) + (zDy))))
34	28, 33	anbi12d 630	. . . . . 6 |- (v = D -> ((((xvy) = 0 <-> x = y) /\ A.z e. X (xvy) <_ ((zvx) + (zvy))) <-> (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy)))))
35	34	2ralbidv 1683	. . . . 5 |- (v = D -> (A.x e. X A.y e. X (((xvy) = 0 <-> x = y) /\ A.z e. X (xvy) <_ ((zvx) + (zvy))) <-> A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy)))))
36	25, 35	anbi12d 630	. . . 4 |- (v = D -> ((v:(X X. X)-->RR /\ A.x e. X A.y e. X (((xvy) = 0 <-> x = y) /\ A.z e. X (xvy) <_ ((zvx) + (zvy)))) <-> (D:(X X. X)-->RR /\ A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))))))
37	24, 36	opelopabg 2823	. . 3 |- ((X e. V /\ D e. A) -> (<.X, D>. e. {<.w, v>. | (v:(w X. w)-->RR /\ A.x e. w A.y e. w (((xvy) = 0 <-> x = y) /\ A.z e. w (xvy) <_ ((zvx) + (zvy))))} <-> (D:(X X. X)-->RR /\ A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))))))
38		dfms2 7796	. . . 4 |- MetSp = {<.w, v>. | (v:(w X. w)-->RR /\ A.x e. w A.y e. w (((xvy) = 0 <-> x = y) /\ A.z e. w (xvy) <_ ((zvx) + (zvy))))}
39	38	eleq2i 1541	. . 3 |- (<.X, D>. e. MetSp <-> <.X, D>. e. {<.w, v>. | (v:(w X. w)-->RR /\ A.x e. w A.y e. w (((xvy) = 0 <-> x = y) /\ A.z e. w (xvy) <_ ((zvx) + (zvy))))})
40	37, 39	syl5bb 534	. 2 |- ((X e. V /\ D e. A) -> (<.X, D>. e. MetSp <-> (D:(X X. X)-->RR /\ A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))))))
41	6, 14, 40	pm5.21nd 682	1 |- (D e. A -> (<.X, D>. e. MetSp <-> (D:(X X. X)-->RR /\ A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))))))

Syntax hints:   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223   = wceq 958   e. wcel 960  A.wral 1648  Vcvv 1814  <.cop 2415   class class class wbr 2624  {copab 2671   X. cxp 3174  -->wf 3184  (class class class)co 3969  RRcr 5245  0cc0 5246   +