Theorem ismet 7807

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

Hypothesis

Ref	Expression
ismet.1	⊢ X = dom dom D

Assertion

Ref	Expression
ismet	⊢ (D ∈ A → (D ∈ Met ↔ (D:(X × X)–→ℝ ⋀ ∀x ∈ X ∀y ∈ X (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ 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 3634	. . . . . 6 ⊢ (d = D → (d:(t × t)–→ℝ ↔ D:(t × t)–→ℝ))
2		opreq 3981	. . . . . . . . . 10 ⊢ (d = D → (xdy) = (xDy))
3	2	eqeq1d 1490	. . . . . . . . 9 ⊢ (d = D → ((xdy) = 0 ↔ (xDy) = 0))
4	3	bibi1d 622	. . . . . . . 8 ⊢ (d = D → (((xdy) = 0 ↔ x = y) ↔ ((xDy) = 0 ↔ x = y)))
5		opreq 3981	. . . . . . . . . . 11 ⊢ (d = D → (zdx) = (zDx))
6		opreq 3981	. . . . . . . . . . 11 ⊢ (d = D → (zdy) = (zDy))
7	5, 6	opreq12d 3992	. . . . . . . . . 10 ⊢ (d = D → ((zdx) + (zdy)) = ((zDx) + (zDy)))
8	2, 7	breq12d 2644	. . . . . . . . 9 ⊢ (d = D → ((xdy) ≤ ((zdx) + (zdy)) ↔ (xDy) ≤ ((zDx) + (zDy))))
9	8	ralbidv 1670	. . . . . . . 8 ⊢ (d = D → (∀z ∈ t (xdy) ≤ ((zdx) + (zdy)) ↔ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy))))
10	4, 9	anbi12d 631	. . . . . . 7 ⊢ (d = D → ((((xdy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xdy) ≤ ((zdx) + (zdy))) ↔ (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy)))))
11	10	2ralbidv 1687	. . . . . 6 ⊢ (d = D → (∀x ∈ t ∀y ∈ t (((xdy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xdy) ≤ ((zdx) + (zdy))) ↔ ∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy)))))
12	1, 11	anbi12d 631	. . . . 5 ⊢ (d = D → ((d:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xdy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xdy) ≤ ((zdx) + (zdy)))) ↔ (D:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy))))))
13	12	exbidv 1285	. . . 4 ⊢ (d = D → (∃t(d:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xdy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xdy) ≤ ((zdx) + (zdy)))) ↔ ∃t(D:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy))))))
14		df-met 7802	. . . 4 ⊢ Met = {d∣∃t(d:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xdy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xdy) ≤ ((zdx) + (zdy))))}
15	13, 14	elab2g 1907	. . 3 ⊢ (D ∈ A → (D ∈ Met ↔ ∃t(D:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy))))))
16		fdm 3645	. . . . . . 7 ⊢ (D:(t × t)–→ℝ → dom D = (t × t))
17		dmeq 3325	. . . . . . . 8 ⊢ (dom D = (t × t) → dom dom D = dom ( t × t))
18		dmxpid 3347	. . . . . . . 8 ⊢ dom ( t × t) = t
19	17, 18	syl6req 1531	. . . . . . 7 ⊢ (dom D = (t × t) → t = dom dom D)
20	16, 19	syl 10	. . . . . 6 ⊢ (D:(t × t)–→ℝ → t = dom dom D)
21	20	adantr 391	. . . . 5 ⊢ ((D:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy)))) → t = dom dom D)
22	21	pm4.71ri 641	. . . 4 ⊢ ((D:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy)))) ↔ (t = dom dom D ⋀ (D:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy))))))
23	22	exbii 1057	. . 3 ⊢ (∃t(D:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy)))) ↔ ∃t(t = dom dom D ⋀ (D:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy))))))
24	15, 23	syl6bb 539	. 2 ⊢ (D ∈ A → (D ∈ Met ↔ ∃t(t = dom dom D ⋀ (D:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy)))))))
25		dmexg 3372	. . 3 ⊢ (D ∈ A → dom D ∈ V)
26		dmexg 3372	. . 3 ⊢ (dom D ∈ V → dom dom D ∈ V)
27		ismet.1	. . . . . 6 ⊢ X = dom dom D
28	27	eqeq2i 1492	. . . . 5 ⊢ (t = X ↔ t = dom dom D)
29		xpeq1 3214	. . . . . . . 8 ⊢ (t = X → (t × t) = (X × t))
30		xpeq2 3215	. . . . . . . 8 ⊢ (t = X → (X × t) = (X × X))
31	29, 30	eqtrd 1514	. . . . . . 7 ⊢ (t = X → (t × t) = (X × X))
32		feq2 3635	. . . . . . 7 ⊢ ((t × t) = (X × X) → (D:(t × t)–→ℝ ↔ D:(X × X)–→ℝ))
33	31, 32	syl 10	. . . . . 6 ⊢ (t = X → (D:(t × t)–→ℝ ↔ D:(X × X)–→ℝ))
34		raleq1 1793	. . . . . . . . 9 ⊢ (t = X → (∀z ∈ t (xDy) ≤ ((zDx) + (zDy)) ↔ ∀z ∈ X (xDy) ≤ ((zDx) + (zDy))))
35	34	anbi2d 619	. . . . . . . 8 ⊢ (t = X → ((((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy))) ↔ (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ X (xDy) ≤ ((zDx) + (zDy)))))
36	35	raleqd 1798	. . . . . . 7 ⊢ (t = X → (∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy))) ↔ ∀y ∈ X (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ X (xDy) ≤ ((zDx) + (zDy)))))
37	36	raleqd 1798	. . . . . 6 ⊢ (t = X → (∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy))) ↔ ∀x ∈ X ∀y ∈ X (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ X (xDy) ≤ ((zDx) + (zDy)))))
38	33, 37	anbi12d 631	. . . . 5 ⊢ (t = X → ((D:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy)))) ↔ (D:(X × X)–→ℝ ⋀ ∀x ∈ X ∀y ∈ X (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ X (xDy) ≤ ((zDx) + (zDy))))))
39	28, 38	sylbir 201	. . . 4 ⊢ (t = dom dom D → ((D:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy)))) ↔ (D:(X × X)–→ℝ ⋀ ∀x ∈ X ∀y ∈ X (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ X (xDy) ≤ ((zDx) + (zDy))))))
40	39	ceqsexgv 1895	. . 3 ⊢ (dom dom D ∈ V → (∃t(t = dom dom D ⋀ (D:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy))))) ↔ (D:(X × X)–→ℝ ⋀ ∀x ∈ X ∀y ∈ X (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ X (xDy) ≤ ((zDx) + (zDy))))))
41	25, 26, 40	3syl 20	. 2 ⊢ (D ∈ A → (∃t(t = dom dom D ⋀ (D:(t × t)–→ℝ ⋀ ∀x ∈ t ∀y ∈ t (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ t (xDy) ≤ ((zDx) + (zDy))))) ↔ (D:(X × X)–→ℝ ⋀ ∀x ∈ X ∀y ∈ X (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ X (xDy) ≤ ((zDx) + (zDy))))))
42	24, 41	bitrd 531	1 ⊢ (D ∈ A → (D ∈ Met ↔ (D:(X × X)–→ℝ ⋀ ∀x ∈ X ∀y ∈ X (((xDy) = 0 ↔ x = y) ⋀ ∀z ∈ X (xDy) ≤ ((zDx) + (zDy))))))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   = wceq 960   ∈ wcel 962  ∃wex 984  ∀wral 1652  Vcvv 1818   class class class wbr 2632   × cxp 3182  dom cdm 3184  –→wf 3192  (class class class)co 3977  ℝcr 5246  0cc0 5247   + caddc 5250   ≤ cle 5308  Metcme 7798

This theorem is referenced by:  dfms2 7808  ismeti 7811  metflem 7815  metreslem 7831  0met 7834

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1129  ax-10o 1146  ax-16 1216  ax-11o 1224  ax-ext 1466  ax-sep 2716  ax-pow 2756  ax-pr 2793  ax-un 2880

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1178  df-eu 1388  df-mo 1389  df-clab 1471  df-cleq 1476  df-clel 1479  df-ne 1594  df-ral 1656  df-v 1819  df-dif 2058  df-un 2059  df-in 2060  df-ss 2062  df-nul 2290  df-pw 2412  df-sn 2422  df-pr 2423  df-op 2426  df-uni 2516  df-br 2633  df-opab 2680  df-id 2849  df-xp 3198  df-rel 3199  df-cnv 3200  df-co 3201  df-dm 3202  df-rn 3203  df-res 3204  df-ima 3205  df-fun 3206  df-fn 3207  df-f 3208  df-fv 3212  df-opr 3979  df-met 7802

Copyright terms: Public domain