Theorem metustid 21040

Description: The identity diagonal is included in all elements of the filter base generated by the metric D. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)

Hypothesis

Ref	Expression
metust.1	|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )

Assertion

Ref	Expression
metustid	|- ( ( D e. (PsMet ` X ) /\ A e. F ) -> ( _I |` X ) C_ A )

Distinct variable groups:   D, a   X, a   A, a   F, a

Proof of Theorem metustid

Dummy variables p q are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relres 5291	. . 3 |- Rel ( _I |` X )
2	1	a1i 11	. 2 |- ( ( D e. (PsMet ` X ) /\ A e. F ) -> Rel ( _I |` X ) )
3		vex 3098	. . . . . . . . . . . . . . 15 |- q e. _V
4	3	brres 5270	. . . . . . . . . . . . . 14 |- ( p ( _I |` X ) q <-> ( p _I q /\ p e. X ) )
5		df-br 4438	. . . . . . . . . . . . . 14 |- ( p ( _I |` X ) q <-> <. p , q >. e. ( _I |` X ) )
6	3	ideq 5145	. . . . . . . . . . . . . . 15 |- ( p _I q <-> p = q )
7	6	anbi1i 695	. . . . . . . . . . . . . 14 |- ( ( p _I q /\ p e. X ) <-> ( p = q /\ p e. X ) )
8	4, 5, 7	3bitr3i 275	. . . . . . . . . . . . 13 |- ( <. p , q >. e. ( _I |` X ) <-> ( p = q /\ p e. X ) )
9	8	biimpi 194	. . . . . . . . . . . 12 |- ( <. p , q >. e. ( _I |` X ) -> ( p = q /\ p e. X ) )
10	9	ad2antlr 726	. . . . . . . . . . 11 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> ( p = q /\ p e. X ) )
11	10	simpld 459	. . . . . . . . . 10 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> p = q )
12		df-ov 6284	. . . . . . . . . . 11 |- ( p D p ) = ( D ` <. p , p >. )
13		opeq2 4203	. . . . . . . . . . . 12 |- ( p = q -> <. p , p >. = <. p , q >. )
14	13	fveq2d 5860	. . . . . . . . . . 11 |- ( p = q -> ( D ` <. p , p >. ) = ( D ` <. p , q >. ) )
15	12, 14	syl5eq 2496	. . . . . . . . . 10 |- ( p = q -> ( p D p ) = ( D ` <. p , q >. ) )
16	11, 15	syl 16	. . . . . . . . 9 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> ( p D p ) = ( D ` <. p , q >. ) )
17		simplll 759	. . . . . . . . . 10 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> D e. (PsMet ` X ) )
18	10	simprd 463	. . . . . . . . . 10 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> p e. X )
19		psmet0 20789	. . . . . . . . . 10 |- ( ( D e. (PsMet ` X ) /\ p e. X ) -> ( p D p ) = 0 )
20	17, 18, 19	syl2anc 661	. . . . . . . . 9 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> ( p D p ) = 0 )
21	16, 20	eqtr3d 2486	. . . . . . . 8 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> ( D ` <. p , q >. ) = 0 )
22		0xr 9643	. . . . . . . . . . 11 |- 0 e. RR*
23	22	a1i 11	. . . . . . . . . 10 |- ( a e. RR+ -> 0 e. RR* )
24		rpxr 11237	. . . . . . . . . 10 |- ( a e. RR+ -> a e. RR* )
25		rpgt0 11241	. . . . . . . . . 10 |- ( a e. RR+ -> 0 < a )
26		lbico1 11589	. . . . . . . . . 10 |- ( ( 0 e. RR* /\ a e. RR* /\ 0 < a ) -> 0 e. ( 0 [,) a ) )
27	23, 24, 25, 26	syl3anc 1229	. . . . . . . . 9 |- ( a e. RR+ -> 0 e. ( 0 [,) a ) )
28	27	adantl 466	. . . . . . . 8 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> 0 e. ( 0 [,) a ) )
29	21, 28	eqeltrd 2531	. . . . . . 7 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> ( D ` <. p , q >. ) e. ( 0 [,) a ) )
30		psmetf 20787	. . . . . . . . . 10 |- ( D e. (PsMet ` X ) -> D : ( X X. X ) --> RR* )
31		ffun 5723	. . . . . . . . . 10 |- ( D : ( X X. X ) --> RR* -> Fun D )
32	30, 31	syl 16	. . . . . . . . 9 |- ( D e. (PsMet ` X ) -> Fun D )
33	32	ad3antrrr 729	. . . . . . . 8 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> Fun D )
34	11, 18	eqeltrrd 2532	. . . . . . . . . 10 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> q e. X )
35		opelxpi 5021	. . . . . . . . . 10 |- ( ( p e. X /\ q e. X ) -> <. p , q >. e. ( X X. X ) )
36	18, 34, 35	syl2anc 661	. . . . . . . . 9 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> <. p , q >. e. ( X X. X ) )
37		fdm 5725	. . . . . . . . . . 11 |- ( D : ( X X. X ) --> RR* -> dom D = ( X X. X ) )
38	30, 37	syl 16	. . . . . . . . . 10 |- ( D e. (PsMet ` X ) -> dom D = ( X X. X ) )
39	38	ad3antrrr 729	. . . . . . . . 9 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> dom D = ( X X. X ) )
40	36, 39	eleqtrrd 2534	. . . . . . . 8 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> <. p , q >. e. dom D )
41		fvimacnv 5987	. . . . . . . 8 |- ( ( Fun D /\ <. p , q >. e. dom D ) -> ( ( D ` <. p , q >. ) e. ( 0 [,) a ) <-> <. p , q >. e. ( `' D " ( 0 [,) a ) ) ) )
42	33, 40, 41	syl2anc 661	. . . . . . 7 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> ( ( D ` <. p , q >. ) e. ( 0 [,) a ) <-> <. p , q >. e. ( `' D " ( 0 [,) a ) ) ) )
43	29, 42	mpbid 210	. . . . . 6 |- ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) -> <. p , q >. e. ( `' D " ( 0 [,) a ) ) )
44	43	adantr 465	. . . . 5 |- ( ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> <. p , q >. e. ( `' D " ( 0 [,) a ) ) )
45		simpr 461	. . . . 5 |- ( ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> A = ( `' D " ( 0 [,) a ) ) )
46	44, 45	eleqtrrd 2534	. . . 4 |- ( ( ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) /\ a e. RR+ ) /\ A = ( `' D " ( 0 [,) a ) ) ) -> <. p , q >. e. A )
47		simplr 755	. . . . 5 |- ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) -> A e. F )
48		metust.1	. . . . . . 7 |- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
49	48	metustel 21032	. . . . . 6 |- ( D e. (PsMet ` X ) -> ( A e. F <-> E. a e. RR+ A = ( `' D " ( 0 [,) a ) ) ) )
50	49	ad2antrr 725	. . . . 5 |- ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) -> ( A e. F <-> E. a e. RR+ A = ( `' D " ( 0 [,) a ) ) ) )
51	47, 50	mpbid 210	. . . 4 |- ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) -> E. a e. RR+ A = ( `' D " ( 0 [,) a ) ) )
52	46, 51	r19.29a 2985	. . 3 |- ( ( ( D e. (PsMet ` X ) /\ A e. F ) /\ <. p , q >. e. ( _I |` X ) ) -> <. p , q >. e. A )
53	52	ex 434	. 2 |- ( ( D e. (PsMet ` X ) /\ A e. F ) -> ( <. p , q >. e. ( _I |` X ) -> <. p , q >. e. A ) )
54	2, 53	relssdv 5085	1 |- ( ( D e. (PsMet ` X ) /\ A e. F ) -> ( _I |` X ) C_ A )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1383   e. wcel 1804   E.wrex 2794   C_ wss 3461   <.cop 4020   class class class wbr 4437   |-> cmpt 4495   _I cid 4780   X. cxp 4987   `'ccnv 4988   dom cdm 4989   ran crn 4990   |` cres 4991   "cima 4992   Rel wrel 4994   Fun wfun 5572   -->wf 5574   ` cfv 5578  (class class class)co 6281   0cc0 9495   RR*cxr 9630   < clt 9631   RR+crp 11230   [,)cico 11541  PsMetcpsmet 18380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-i2m1 9563  ax-1ne0 9564  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-po 4790  df-so 4791  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-er 7313  df-map 7424  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-rp 11231  df-ico 11545  df-psmet 18389

This theorem is referenced by:  metustfbas  21046  metust  21048