Metamath Proof Explorer

Theorem met2ndci

Description: A separable metric space (a metric space with a countable dense subset) is second-countable. (Contributed by Mario Carneiro, 13-Apr-2015)

Ref Expression
Hypothesis methaus.1 
|- J = ( MetOpen ` D )
Assertion met2ndci 
|- ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> J e. 2ndc )

Proof

Step Hyp Ref Expression
1 methaus.1 
 |-  J = ( MetOpen ` D )
2 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
3 2 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> J e. Top )
4 simpll 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( x e. NN /\ y e. A ) ) -> D e. ( *Met ` X ) )
5 simplr1 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( x e. NN /\ y e. A ) ) -> A C_ X )
6 simprr 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( x e. NN /\ y e. A ) ) -> y e. A )
7 5 6 sseldd 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( x e. NN /\ y e. A ) ) -> y e. X )
8 simprl 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( x e. NN /\ y e. A ) ) -> x e. NN )
9 8 nnrpd 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( x e. NN /\ y e. A ) ) -> x e. RR+ )
10 9 rpreccld 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( x e. NN /\ y e. A ) ) -> ( 1 / x ) e. RR+ )
11 10 rpxrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( x e. NN /\ y e. A ) ) -> ( 1 / x ) e. RR* )
12 1 blopn 
 |-  ( ( D e. ( *Met ` X ) /\ y e. X /\ ( 1 / x ) e. RR* ) -> ( y ( ball ` D ) ( 1 / x ) ) e. J )
13 4 7 11 12 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( x e. NN /\ y e. A ) ) -> ( y ( ball ` D ) ( 1 / x ) ) e. J )
14 13 ralrimivva 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> A. x e. NN A. y e. A ( y ( ball ` D ) ( 1 / x ) ) e. J )
15 eqid 
 |-  ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) = ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) )
16 15 fmpo 
 |-  ( A. x e. NN A. y e. A ( y ( ball ` D ) ( 1 / x ) ) e. J <-> ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) : ( NN X. A ) --> J )
17 14 16 sylib 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) : ( NN X. A ) --> J )
18 17 frnd 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) C_ J )
19 simpll 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) -> D e. ( *Met ` X ) )
20 simprl 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) -> u e. J )
21 simprr 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) -> z e. u )
22 1 mopni2 
 |-  ( ( D e. ( *Met ` X ) /\ u e. J /\ z e. u ) -> E. r e. RR+ ( z ( ball ` D ) r ) C_ u )
23 19 20 21 22 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) -> E. r e. RR+ ( z ( ball ` D ) r ) C_ u )
24 simprl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) ) -> r e. RR+ )
25 24 rphalfcld 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) ) -> ( r / 2 ) e. RR+ )
26 elrp 
 |-  ( ( r / 2 ) e. RR+ <-> ( ( r / 2 ) e. RR /\ 0 < ( r / 2 ) ) )
27 nnrecl 
 |-  ( ( ( r / 2 ) e. RR /\ 0 < ( r / 2 ) ) -> E. n e. NN ( 1 / n ) < ( r / 2 ) )
28 26 27 sylbi 
 |-  ( ( r / 2 ) e. RR+ -> E. n e. NN ( 1 / n ) < ( r / 2 ) )
29 25 28 syl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) ) -> E. n e. NN ( 1 / n ) < ( r / 2 ) )
30 3 ad2antrr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> J e. Top )
31 simpr1 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> A C_ X )
32 31 ad2antrr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> A C_ X )
33 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
34 33 ad3antrrr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> X = U. J )
35 32 34 sseqtrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> A C_ U. J )
36 simplrr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> z e. u )
37 simplrl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> u e. J )
38 elunii 
 |-  ( ( z e. u /\ u e. J ) -> z e. U. J )
39 36 37 38 syl2anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> z e. U. J )
40 39 34 eleqtrrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> z e. X )
41 simpr3 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> ( ( cls ` J ) ` A ) = X )
42 41 ad2antrr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> ( ( cls ` J ) ` A ) = X )
43 40 42 eleqtrrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> z e. ( ( cls ` J ) ` A ) )
44 19 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> D e. ( *Met ` X ) )
45 simprrl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> n e. NN )
46 45 nnrpd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> n e. RR+ )
47 46 rpreccld 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> ( 1 / n ) e. RR+ )
48 47 rpxrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> ( 1 / n ) e. RR* )
49 1 blopn 
 |-  ( ( D e. ( *Met ` X ) /\ z e. X /\ ( 1 / n ) e. RR* ) -> ( z ( ball ` D ) ( 1 / n ) ) e. J )
50 44 40 48 49 syl3anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> ( z ( ball ` D ) ( 1 / n ) ) e. J )
51 blcntr 
 |-  ( ( D e. ( *Met ` X ) /\ z e. X /\ ( 1 / n ) e. RR+ ) -> z e. ( z ( ball ` D ) ( 1 / n ) ) )
52 44 40 47 51 syl3anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> z e. ( z ( ball ` D ) ( 1 / n ) ) )
53 eqid 
 |-  U. J = U. J
54 53 clsndisj 
 |-  ( ( ( J e. Top /\ A C_ U. J /\ z e. ( ( cls ` J ) ` A ) ) /\ ( ( z ( ball ` D ) ( 1 / n ) ) e. J /\ z e. ( z ( ball ` D ) ( 1 / n ) ) ) ) -> ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) =/= (/) )
55 30 35 43 50 52 54 syl32anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) =/= (/) )
56 n0 
 |-  ( ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) =/= (/) <-> E. t t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) )
57 55 56 sylib 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> E. t t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) )
58 45 adantr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> n e. NN )
59 simpr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) )
60 59 elin2d 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> t e. A )
61 eqidd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> ( t ( ball ` D ) ( 1 / n ) ) = ( t ( ball ` D ) ( 1 / n ) ) )
62 oveq2 
 |-  ( x = n -> ( 1 / x ) = ( 1 / n ) )
63 62 oveq2d 
 |-  ( x = n -> ( y ( ball ` D ) ( 1 / x ) ) = ( y ( ball ` D ) ( 1 / n ) ) )
64 63 eqeq2d 
 |-  ( x = n -> ( ( t ( ball ` D ) ( 1 / n ) ) = ( y ( ball ` D ) ( 1 / x ) ) <-> ( t ( ball ` D ) ( 1 / n ) ) = ( y ( ball ` D ) ( 1 / n ) ) ) )
65 oveq1 
 |-  ( y = t -> ( y ( ball ` D ) ( 1 / n ) ) = ( t ( ball ` D ) ( 1 / n ) ) )
66 65 eqeq2d 
 |-  ( y = t -> ( ( t ( ball ` D ) ( 1 / n ) ) = ( y ( ball ` D ) ( 1 / n ) ) <-> ( t ( ball ` D ) ( 1 / n ) ) = ( t ( ball ` D ) ( 1 / n ) ) ) )
67 64 66 rspc2ev 
 |-  ( ( n e. NN /\ t e. A /\ ( t ( ball ` D ) ( 1 / n ) ) = ( t ( ball ` D ) ( 1 / n ) ) ) -> E. x e. NN E. y e. A ( t ( ball ` D ) ( 1 / n ) ) = ( y ( ball ` D ) ( 1 / x ) ) )
68 58 60 61 67 syl3anc 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> E. x e. NN E. y e. A ( t ( ball ` D ) ( 1 / n ) ) = ( y ( ball ` D ) ( 1 / x ) ) )
69 ovex 
 |-  ( t ( ball ` D ) ( 1 / n ) ) e. _V
70 eqeq1 
 |-  ( z = ( t ( ball ` D ) ( 1 / n ) ) -> ( z = ( y ( ball ` D ) ( 1 / x ) ) <-> ( t ( ball ` D ) ( 1 / n ) ) = ( y ( ball ` D ) ( 1 / x ) ) ) )
71 70 2rexbidv 
 |-  ( z = ( t ( ball ` D ) ( 1 / n ) ) -> ( E. x e. NN E. y e. A z = ( y ( ball ` D ) ( 1 / x ) ) <-> E. x e. NN E. y e. A ( t ( ball ` D ) ( 1 / n ) ) = ( y ( ball ` D ) ( 1 / x ) ) ) )
72 15 rnmpo 
 |-  ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) = { z | E. x e. NN E. y e. A z = ( y ( ball ` D ) ( 1 / x ) ) }
73 69 71 72 elab2 
 |-  ( ( t ( ball ` D ) ( 1 / n ) ) e. ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) <-> E. x e. NN E. y e. A ( t ( ball ` D ) ( 1 / n ) ) = ( y ( ball ` D ) ( 1 / x ) ) )
74 68 73 sylibr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> ( t ( ball ` D ) ( 1 / n ) ) e. ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) )
75 59 elin1d 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> t e. ( z ( ball ` D ) ( 1 / n ) ) )
76 44 adantr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> D e. ( *Met ` X ) )
77 48 adantr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> ( 1 / n ) e. RR* )
78 40 adantr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> z e. X )
79 32 adantr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> A C_ X )
80 79 60 sseldd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> t e. X )
81 blcom 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( 1 / n ) e. RR* ) /\ ( z e. X /\ t e. X ) ) -> ( t e. ( z ( ball ` D ) ( 1 / n ) ) <-> z e. ( t ( ball ` D ) ( 1 / n ) ) ) )
82 76 77 78 80 81 syl22anc 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> ( t e. ( z ( ball ` D ) ( 1 / n ) ) <-> z e. ( t ( ball ` D ) ( 1 / n ) ) ) )
83 75 82 mpbid 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> z e. ( t ( ball ` D ) ( 1 / n ) ) )
84 simprll 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> r e. RR+ )
85 84 adantr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> r e. RR+ )
86 85 rphalfcld 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> ( r / 2 ) e. RR+ )
87 86 rpxrd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> ( r / 2 ) e. RR* )
88 simprrr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> ( 1 / n ) < ( r / 2 ) )
89 84 rphalfcld 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> ( r / 2 ) e. RR+ )
90 rpre 
 |-  ( ( 1 / n ) e. RR+ -> ( 1 / n ) e. RR )
91 rpre 
 |-  ( ( r / 2 ) e. RR+ -> ( r / 2 ) e. RR )
92 ltle 
 |-  ( ( ( 1 / n ) e. RR /\ ( r / 2 ) e. RR ) -> ( ( 1 / n ) < ( r / 2 ) -> ( 1 / n ) <_ ( r / 2 ) ) )
93 90 91 92 syl2an 
 |-  ( ( ( 1 / n ) e. RR+ /\ ( r / 2 ) e. RR+ ) -> ( ( 1 / n ) < ( r / 2 ) -> ( 1 / n ) <_ ( r / 2 ) ) )
94 47 89 93 syl2anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> ( ( 1 / n ) < ( r / 2 ) -> ( 1 / n ) <_ ( r / 2 ) ) )
95 88 94 mpd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> ( 1 / n ) <_ ( r / 2 ) )
96 95 adantr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> ( 1 / n ) <_ ( r / 2 ) )
97 ssbl 
 |-  ( ( ( D e. ( *Met ` X ) /\ t e. X ) /\ ( ( 1 / n ) e. RR* /\ ( r / 2 ) e. RR* ) /\ ( 1 / n ) <_ ( r / 2 ) ) -> ( t ( ball ` D ) ( 1 / n ) ) C_ ( t ( ball ` D ) ( r / 2 ) ) )
98 76 80 77 87 96 97 syl221anc 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> ( t ( ball ` D ) ( 1 / n ) ) C_ ( t ( ball ` D ) ( r / 2 ) ) )
99 85 rpred 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> r e. RR )
100 98 83 sseldd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> z e. ( t ( ball ` D ) ( r / 2 ) ) )
101 blhalf 
 |-  ( ( ( D e. ( *Met ` X ) /\ t e. X ) /\ ( r e. RR /\ z e. ( t ( ball ` D ) ( r / 2 ) ) ) ) -> ( t ( ball ` D ) ( r / 2 ) ) C_ ( z ( ball ` D ) r ) )
102 76 80 99 100 101 syl22anc 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> ( t ( ball ` D ) ( r / 2 ) ) C_ ( z ( ball ` D ) r ) )
103 simprlr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> ( z ( ball ` D ) r ) C_ u )
104 103 adantr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> ( z ( ball ` D ) r ) C_ u )
105 102 104 sstrd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> ( t ( ball ` D ) ( r / 2 ) ) C_ u )
106 98 105 sstrd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> ( t ( ball ` D ) ( 1 / n ) ) C_ u )
107 eleq2 
 |-  ( w = ( t ( ball ` D ) ( 1 / n ) ) -> ( z e. w <-> z e. ( t ( ball ` D ) ( 1 / n ) ) ) )
108 sseq1 
 |-  ( w = ( t ( ball ` D ) ( 1 / n ) ) -> ( w C_ u <-> ( t ( ball ` D ) ( 1 / n ) ) C_ u ) )
109 107 108 anbi12d 
 |-  ( w = ( t ( ball ` D ) ( 1 / n ) ) -> ( ( z e. w /\ w C_ u ) <-> ( z e. ( t ( ball ` D ) ( 1 / n ) ) /\ ( t ( ball ` D ) ( 1 / n ) ) C_ u ) ) )
110 109 rspcev 
 |-  ( ( ( t ( ball ` D ) ( 1 / n ) ) e. ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) /\ ( z e. ( t ( ball ` D ) ( 1 / n ) ) /\ ( t ( ball ` D ) ( 1 / n ) ) C_ u ) ) -> E. w e. ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ( z e. w /\ w C_ u ) )
111 74 83 106 110 syl12anc 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) /\ t e. ( ( z ( ball ` D ) ( 1 / n ) ) i^i A ) ) -> E. w e. ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ( z e. w /\ w C_ u ) )
112 57 111 exlimddv 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) ) -> E. w e. ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ( z e. w /\ w C_ u ) )
113 112 anassrs 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) ) /\ ( n e. NN /\ ( 1 / n ) < ( r / 2 ) ) ) -> E. w e. ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ( z e. w /\ w C_ u ) )
114 29 113 rexlimddv 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) /\ ( r e. RR+ /\ ( z ( ball ` D ) r ) C_ u ) ) -> E. w e. ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ( z e. w /\ w C_ u ) )
115 23 114 rexlimddv 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) /\ ( u e. J /\ z e. u ) ) -> E. w e. ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ( z e. w /\ w C_ u ) )
116 115 ralrimivva 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> A. u e. J A. z e. u E. w e. ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ( z e. w /\ w C_ u ) )
117 basgen2 
 |-  ( ( J e. Top /\ ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) C_ J /\ A. u e. J A. z e. u E. w e. ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ( z e. w /\ w C_ u ) ) -> ( topGen ` ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ) = J )
118 3 18 116 117 syl3anc 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> ( topGen ` ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ) = J )
119 118 3 eqeltrd 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> ( topGen ` ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ) e. Top )
120 tgclb 
 |-  ( ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) e. TopBases <-> ( topGen ` ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ) e. Top )
121 119 120 sylibr 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) e. TopBases )
122 omelon 
 |-  _om e. On
123 simpr2 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> A ~<_ _om )
124 nnex 
 |-  NN e. _V
125 124 xpdom2 
 |-  ( A ~<_ _om -> ( NN X. A ) ~<_ ( NN X. _om ) )
126 123 125 syl 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> ( NN X. A ) ~<_ ( NN X. _om ) )
127 nnenom 
 |-  NN ~~ _om
128 omex 
 |-  _om e. _V
129 128 enref 
 |-  _om ~~ _om
130 xpen 
 |-  ( ( NN ~~ _om /\ _om ~~ _om ) -> ( NN X. _om ) ~~ ( _om X. _om ) )
131 127 129 130 mp2an 
 |-  ( NN X. _om ) ~~ ( _om X. _om )
132 xpomen 
 |-  ( _om X. _om ) ~~ _om
133 131 132 entri 
 |-  ( NN X. _om ) ~~ _om
134 domentr 
 |-  ( ( ( NN X. A ) ~<_ ( NN X. _om ) /\ ( NN X. _om ) ~~ _om ) -> ( NN X. A ) ~<_ _om )
135 126 133 134 sylancl 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> ( NN X. A ) ~<_ _om )
136 ondomen 
 |-  ( ( _om e. On /\ ( NN X. A ) ~<_ _om ) -> ( NN X. A ) e. dom card )
137 122 135 136 sylancr 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> ( NN X. A ) e. dom card )
138 17 ffnd 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) Fn ( NN X. A ) )
139 dffn4 
 |-  ( ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) Fn ( NN X. A ) <-> ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) : ( NN X. A ) -onto-> ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) )
140 138 139 sylib 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) : ( NN X. A ) -onto-> ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) )
141 fodomnum 
 |-  ( ( NN X. A ) e. dom card -> ( ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) : ( NN X. A ) -onto-> ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) -> ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ~<_ ( NN X. A ) ) )
142 137 140 141 sylc 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ~<_ ( NN X. A ) )
143 domtr 
 |-  ( ( ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ~<_ ( NN X. A ) /\ ( NN X. A ) ~<_ _om ) -> ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ~<_ _om )
144 142 135 143 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ~<_ _om )
145 2ndci 
 |-  ( ( ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) e. TopBases /\ ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ~<_ _om ) -> ( topGen ` ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ) e. 2ndc )
146 121 144 145 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> ( topGen ` ran ( x e. NN , y e. A |-> ( y ( ball ` D ) ( 1 / x ) ) ) ) e. 2ndc )
147 118 146 eqeltrrd 
 |-  ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ _om /\ ( ( cls ` J ) ` A ) = X ) ) -> J e. 2ndc )