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 birani 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> E. p p e. X )
36 opelidres 
 |-  ( p e. X -> ( <. p , p >. e. ( _I |` X ) <-> p e. X ) )
37 36 ibir 
 |-  ( p e. X -> <. p , p >. e. ( _I |` X ) )
38 37 ne0d 
 |-  ( p e. X -> ( _I |` X ) =/= (/) )
39 38 exlimiv 
 |-  ( E. p p e. X -> ( _I |` X ) =/= (/) )
40 35 39 syl 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( _I |` X ) =/= (/) )
41 40 adantr 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ x e. F ) -> ( _I |` X ) =/= (/) )
42 ssn0 
 |-  ( ( ( _I |` X ) C_ x /\ ( _I |` X ) =/= (/) ) -> x =/= (/) )
43 33 41 42 syl2anc 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ x e. F ) -> x =/= (/) )
44 43 nelrdva 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> -. (/) e. F )
45 df-nel 
 |-  ( (/) e/ F <-> -. (/) e. F )
46 44 45 sylibr 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> (/) e/ F )
47 dfss2 
 |-  ( x C_ y <-> ( x i^i y ) = x )
48 47 bilani 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) /\ x C_ y ) -> ( x i^i y ) = x )
49 simplrl 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) /\ x C_ y ) -> x e. F )
50 48 49 eqeltrd 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) /\ x C_ y ) -> ( x i^i y ) e. F )
51 sseqin2 
 |-  ( y C_ x <-> ( x i^i y ) = y )
52 51 bilani 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) /\ y C_ x ) -> ( x i^i y ) = y )
53 simplrr 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) /\ y C_ x ) -> y e. F )
54 52 53 eqeltrd 
 |-  ( ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) /\ y C_ x ) -> ( x i^i y ) e. F )
55 simplr 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) -> D e. ( PsMet ` X ) )
56 simprl 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) -> x e. F )
57 simprr 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) -> y e. F )
58 1 metustto 
 |-  ( ( D e. ( PsMet ` X ) /\ x e. F /\ y e. F ) -> ( x C_ y \/ y C_ x ) )
59 55 56 57 58 syl3anc 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) -> ( x C_ y \/ y C_ x ) )
60 50 54 59 mpjaodan 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) -> ( x i^i y ) e. F )
61 ssidd 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) -> ( x i^i y ) C_ ( x i^i y ) )
62 sseq1 
 |-  ( z = ( x i^i y ) -> ( z C_ ( x i^i y ) <-> ( x i^i y ) C_ ( x i^i y ) ) )
63 62 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 ) )
64 60 61 63 syl2anc 
 |-  ( ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) /\ ( x e. F /\ y e. F ) ) -> E. z e. F z C_ ( x i^i y ) )
65 64 ralrimivva 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) )
66 31 46 65 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 ) ) )
67 elfvex 
 |-  ( D e. ( PsMet ` X ) -> X e. _V )
68 67 adantl 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> X e. _V )
69 68 68 xpexd 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> ( X X. X ) e. _V )
70 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 ) ) ) ) )
71 69 70 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 ) ) ) ) )
72 16 66 71 mpbir2and 
 |-  ( ( X =/= (/) /\ D e. ( PsMet ` X ) ) -> F e. ( fBas ` ( X X. X ) ) )