Metamath Proof Explorer


Theorem metustfbas

Description: The filter base generated by a metric D . (Contributed by Thierry Arnoux, 26-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 e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
Assertion metustfbas
|- ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> F e. ( fBas ` ( X X. X ) ) )

Proof

Step Hyp Ref Expression
1 metust.1
 |-  F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
2 1 metustel
 |-  ( D e. ( PsMet ` X ) -> ( x e. F <-> E. a e. RR+ x = ( `' D " ( 0 [,) a ) ) ) )
3 simpr
 |-  ( ( D e. ( PsMet ` X ) /\ x = ( `' D " ( 0 [,) a ) ) ) -> x = ( `' D " ( 0 [,) a ) ) )
4 cnvimass
 |-  ( `' D " ( 0 [,) a ) ) C_ dom D
5 psmetf
 |-  ( D e. ( PsMet ` X ) -> D : ( X X. X ) --> RR* )
6 5 fdmd
 |-  ( D e. ( PsMet ` X ) -> dom D = ( X X. X ) )
7 6 adantr
 |-  ( ( D e. ( PsMet ` X ) /\ x = ( `' D " ( 0 [,) a ) ) ) -> dom D = ( X X. X ) )
8 4 7 sseqtrid
 |-  ( ( D e. ( PsMet ` X ) /\ x = ( `' D " ( 0 [,) a ) ) ) -> ( `' D " ( 0 [,) a ) ) C_ ( X X. X ) )
9 3 8 eqsstrd
 |-  ( ( D e. ( PsMet ` X ) /\ x = ( `' D " ( 0 [,) a ) ) ) -> x C_ ( X X. X ) )
10 9 ex
 |-  ( D e. ( PsMet ` X ) -> ( x = ( `' D " ( 0 [,) a ) ) -> x C_ ( X X. X ) ) )
11 10 rexlimdvw
 |-  ( D e. ( PsMet ` X ) -> ( E. a e. RR+ x = ( `' D " ( 0 [,) a ) ) -> x C_ ( X X. X ) ) )
12 2 11 sylbid
 |-  ( D e. ( PsMet ` X ) -> ( x e. F -> x C_ ( X X. X ) ) )
13 12 ralrimiv
 |-  ( D e. ( PsMet ` X ) -> A. x e. F x C_ ( X X. X ) )
14 pwssb
 |-  ( F C_ ~P ( X X. X ) <-> A. x e. F x C_ ( X X. X ) )
15 13 14 sylibr
 |-  ( D e. ( PsMet ` X ) -> F C_ ~P ( X X. X ) )
16 15 adantl
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> F C_ ~P ( X X. X ) )
17 cnvexg
 |-  ( D e. ( PsMet ` X ) -> `' D e. _V )
18 imaexg
 |-  ( `' D e. _V -> ( `' D " ( 0 [,) 1 ) ) e. _V )
19 elisset
 |-  ( ( `' D " ( 0 [,) 1 ) ) e. _V -> E. x x = ( `' D " ( 0 [,) 1 ) ) )
20 1rp
 |-  1 e. RR+
21 oveq2
 |-  ( a = 1 -> ( 0 [,) a ) = ( 0 [,) 1 ) )
22 21 imaeq2d
 |-  ( a = 1 -> ( `' D " ( 0 [,) a ) ) = ( `' D " ( 0 [,) 1 ) ) )
23 22 rspceeqv
 |-  ( ( 1 e. RR+ /\ x = ( `' D " ( 0 [,) 1 ) ) ) -> E. a e. RR+ x = ( `' D " ( 0 [,) a ) ) )
24 20 23 mpan
 |-  ( x = ( `' D " ( 0 [,) 1 ) ) -> E. a e. RR+ x = ( `' D " ( 0 [,) a ) ) )
25 24 eximi
 |-  ( E. x x = ( `' D " ( 0 [,) 1 ) ) -> E. x E. a e. RR+ x = ( `' D " ( 0 [,) a ) ) )
26 17 18 19 25 4syl
 |-  ( D e. ( PsMet ` X ) -> E. x E. a e. RR+ x = ( `' D " ( 0 [,) a ) ) )
27 2 exbidv
 |-  ( D e. ( PsMet ` X ) -> ( E. x x e. F <-> E. x E. a e. RR+ x = ( `' D " ( 0 [,) a ) ) ) )
28 26 27 mpbird
 |-  ( D e. ( PsMet ` X ) -> E. x x e. F )
29 28 adantl
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> E. x x e. F )
30 n0
 |-  ( F =/= (/) <-> E. x x e. F )
31 29 30 sylibr
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> F =/= (/) )
32 1 metustid
 |-  ( ( D e. ( PsMet ` X ) /\ x e. F ) -> ( _I |` X ) C_ x )
33 32 adantll
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ x e. F ) -> ( _I |` X ) C_ x )
34 n0
 |-  ( X =/= (/) <-> E. p p e. X )
35 34 biimpi
 |-  ( X =/= (/) -> E. p p e. X )
36 35 adantr
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> E. p p e. X )
37 opelidres
 |-  ( p e. X -> ( <. p , p >. e. ( _I |` X ) <-> p e. X ) )
38 37 ibir
 |-  ( p e. X -> <. p , p >. e. ( _I |` X ) )
39 38 ne0d
 |-  ( p e. X -> ( _I |` X ) =/= (/) )
40 39 exlimiv
 |-  ( E. p p e. X -> ( _I |` X ) =/= (/) )
41 36 40 syl
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( _I |` X ) =/= (/) )
42 41 adantr
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ x e. F ) -> ( _I |` X ) =/= (/) )
43 ssn0
 |-  ( ( ( _I |` X ) C_ x /\ ( _I |` X ) =/= (/) ) -> x =/= (/) )
44 33 42 43 syl2anc
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ x e. F ) -> x =/= (/) )
45 44 nelrdva
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> -. (/) e. F )
46 df-nel
 |-  ( (/) e/ F <-> -. (/) e. F )
47 45 46 sylibr
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> (/) e/ F )
48 df-ss
 |-  ( x C_ y <-> ( x i^i y ) = x )
49 48 biimpi
 |-  ( x C_ y -> ( x i^i y ) = x )
50 49 adantl
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) /\ x C_ y ) -> ( x i^i y ) = x )
51 simplrl
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) /\ x C_ y ) -> x e. F )
52 50 51 eqeltrd
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) /\ x C_ y ) -> ( x i^i y ) e. F )
53 sseqin2
 |-  ( y C_ x <-> ( x i^i y ) = y )
54 53 biimpi
 |-  ( y C_ x -> ( x i^i y ) = y )
55 54 adantl
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) /\ y C_ x ) -> ( x i^i y ) = y )
56 simplrr
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) /\ y C_ x ) -> y e. F )
57 55 56 eqeltrd
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) /\ y C_ x ) -> ( x i^i y ) e. F )
58 simplr
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) -> D e. ( PsMet ` X ) )
59 simprl
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) -> x e. F )
60 simprr
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) -> y e. F )
61 1 metustto
 |-  ( ( D e. ( PsMet ` X ) /\ x e. F /\ y e. F ) -> ( x C_ y \/ y C_ x ) )
62 58 59 60 61 syl3anc
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) -> ( x C_ y \/ y C_ x ) )
63 52 57 62 mpjaodan
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) -> ( x i^i y ) e. F )
64 ssidd
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) -> ( x i^i y ) C_ ( x i^i y ) )
65 sseq1
 |-  ( z = ( x i^i y ) -> ( z C_ ( x i^i y ) <-> ( x i^i y ) C_ ( x i^i y ) ) )
66 65 rspcev
 |-  ( ( ( x i^i y ) e. F /\ ( x i^i y ) C_ ( x i^i y ) ) -> E. z e. F z C_ ( x i^i y ) )
67 63 64 66 syl2anc
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) -> E. z e. F z C_ ( x i^i y ) )
68 67 ralrimivva
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) )
69 31 47 68 3jca
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) ) )
70 elfvex
 |-  ( D e. ( PsMet ` X ) -> X e. _V )
71 70 adantl
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> X e. _V )
72 71 71 xpexd
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( X X. X ) e. _V )
73 isfbas2
 |-  ( ( X X. X ) e. _V -> ( F e. ( fBas ` ( X X. X ) ) <-> ( F C_ ~P ( X X. X ) /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) ) ) ) )
74 72 73 syl
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( F e. ( fBas ` ( X X. X ) ) <-> ( F C_ ~P ( X X. X ) /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) ) ) ) )
75 16 69 74 mpbir2and
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> F e. ( fBas ` ( X X. X ) ) )