Metamath Proof Explorer


Theorem metustid

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) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Hypothesis metust.1 F = ran a + D -1 0 a
Assertion metustid D PsMet X A F I X A

Proof

Step Hyp Ref Expression
1 metust.1 F = ran a + D -1 0 a
2 relres Rel I X
3 2 a1i D PsMet X A F Rel I X
4 vex q V
5 4 brresi p I X q p X p I q
6 df-br p I X q p q I X
7 4 ideq p I q p = q
8 7 anbi2i p X p I q p X p = q
9 5 6 8 3bitr3i p q I X p X p = q
10 9 biimpi p q I X p X p = q
11 10 ad2antlr D PsMet X A F p q I X a + p X p = q
12 11 simprd D PsMet X A F p q I X a + p = q
13 df-ov p D p = D p p
14 opeq2 p = q p p = p q
15 14 fveq2d p = q D p p = D p q
16 13 15 syl5eq p = q p D p = D p q
17 12 16 syl D PsMet X A F p q I X a + p D p = D p q
18 simplll D PsMet X A F p q I X a + D PsMet X
19 11 simpld D PsMet X A F p q I X a + p X
20 psmet0 D PsMet X p X p D p = 0
21 18 19 20 syl2anc D PsMet X A F p q I X a + p D p = 0
22 17 21 eqtr3d D PsMet X A F p q I X a + D p q = 0
23 0xr 0 *
24 rpxr a + a *
25 rpgt0 a + 0 < a
26 lbico1 0 * a * 0 < a 0 0 a
27 23 24 25 26 mp3an2i a + 0 0 a
28 27 adantl D PsMet X A F p q I X a + 0 0 a
29 22 28 eqeltrd D PsMet X A F p q I X a + D p q 0 a
30 psmetf D PsMet X D : X × X *
31 30 ffund D PsMet X Fun D
32 31 ad3antrrr D PsMet X A F p q I X a + Fun D
33 12 19 eqeltrrd D PsMet X A F p q I X a + q X
34 19 33 opelxpd D PsMet X A F p q I X a + p q X × X
35 30 fdmd D PsMet X dom D = X × X
36 35 ad3antrrr D PsMet X A F p q I X a + dom D = X × X
37 34 36 eleqtrrd D PsMet X A F p q I X a + p q dom D
38 fvimacnv Fun D p q dom D D p q 0 a p q D -1 0 a
39 32 37 38 syl2anc D PsMet X A F p q I X a + D p q 0 a p q D -1 0 a
40 29 39 mpbid D PsMet X A F p q I X a + p q D -1 0 a
41 40 adantr D PsMet X A F p q I X a + A = D -1 0 a p q D -1 0 a
42 simpr D PsMet X A F p q I X a + A = D -1 0 a A = D -1 0 a
43 41 42 eleqtrrd D PsMet X A F p q I X a + A = D -1 0 a p q A
44 simplr D PsMet X A F p q I X A F
45 1 metustel D PsMet X A F a + A = D -1 0 a
46 45 ad2antrr D PsMet X A F p q I X A F a + A = D -1 0 a
47 44 46 mpbid D PsMet X A F p q I X a + A = D -1 0 a
48 43 47 r19.29a D PsMet X A F p q I X p q A
49 48 ex D PsMet X A F p q I X p q A
50 3 49 relssdv D PsMet X A F I X A