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 ) ) )