Theorem ismsg 7800

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 2620	. . . . 5 |- (XMetSpD <-> <.X, D>. e. MetSp)
2		msrel 7797	. . . . . 6 |- Rel MetSp
3	2	brrelexi 3208	. . . . 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 436	. 2 |- ((D e. A /\ <.X, D>. e. MetSp) -> (X e. V /\ D e. A))
7		dmfex 3655	. . . . 5 |- ((D e. A /\ D:(X X. X)-->RR) -> (X X. X) e. V)
8		xpexr 3479	. . . . . 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 395	. 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 3200	. . . . . . 7 |- (w = X -> (w X. w) = (X X. w))
16		xpeq2 3201	. . . . . . 7 |- (w = X -> (X X. w) = (X X. X))
17	15, 16	eqtrd 1507	. . . . . 6 |- (w = X -> (w X. w) = (X X. X))
18		feq2 3621	. . . . . 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 1786	. . . . . . . 8 |- (w = X -> (A.z e. w (xvy) <_ ((zvx) + (zvy)) <-> A.z e. X (xvy) <_ ((zvx) + (zvy))))
21	20	anbi2d 616	. . . . . . 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 1791	. . . . . 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 1791	. . . . 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 628	. . . 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 3620	. . . . 5 |- (v = D -> (v:(X X. X)-->RR <-> D:(X X. X)-->RR))
26		opreq 3967	. . . . . . . . 9 |- (v = D -> (xvy) = (xDy))
27	26	eqeq1d 1483	. . . . . . . 8 |- (v = D -> ((xvy) = 0 <-> (xDy) = 0))
28	27	bibi1d 619	. . . . . . 7 |- (v = D -> (((xvy) = 0 <-> x = y) <-> ((xDy) = 0 <-> x = y)))
29		opreq 3967	. . . . . . . . . 10 |- (v = D -> (zvx) = (zDx))
30		opreq 3967	. . . . . . . . . 10 |- (v = D -> (zvy) = (zDy))
31	29, 30	opreq12d 3978	. . . . . . . . 9 |- (v = D -> ((zvx) + (zvy)) = ((zDx) + (zDy)))
32	26, 31	breq12d 2631	. . . . . . . 8 |- (v = D -> ((xvy) <_ ((zvx) + (zvy)) <-> (xDy) <_ ((zDx) + (zDy))))
33	32	ralbidv 1663	. . . . . . 7 |- (v = D -> (A.z e. X (xvy) <_ ((zvx) + (zvy)) <-> A.z e. X (xDy) <_ ((zDx) + (zDy))))
34	28, 33	anbi12d 628	. . . . . 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 1680	. . . . 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 628	. . . 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 2817	. . 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 7799	. . . 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 1538	. . 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 532	. 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 680	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 956   e. wcel 958  A.wral 1645  Vcvv 1811  <.cop 2411   class class class wbr 2619  {copab 2666   X. cxp 3168  -->wf 3178  (class class class)co 3963  RRcr 5233  0cc0 5234   +