ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  metrest Unicode version
Theorem metrest 13673
Description: Two alternate formulations of a subspace topology of a metric space topology. (Contributed by Jeff Hankins, 19-Aug-2009.) (Proof shortened by Mario Carneiro, 5-Jan-2014.)
Hypotheses
Ref Expression
metrest.1 |- D = ( C |` ( Y X. Y ) )
metrest.3 |- J = ( MetOpen ` C )
metrest.4 |- K = ( MetOpen ` D )
Assertion
Ref Expression
metrest |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( J ↾t Y ) = K )
Proof of Theorem metrest
Dummy variables u r x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inss1 3355 . . . . . . . . . 10 |- ( u i^i Y ) C_ u
2 metrest.3 . . . . . . . . . . . . 13 |- J = ( MetOpen ` C )
32elmopn2 13616 . . . . . . . . . . . 12 |- ( C e. ( *Met ` X ) -> ( u e. J <-> ( u C_ X /\ A. y e. u E. r e. RR+ ( y ( ball ` C ) r ) C_ u ) ) )
43simplbda 384 . . . . . . . . . . 11 |- ( ( C e. ( *Met ` X ) /\ u e. J ) -> A. y e. u E. r e. RR+ ( y ( ball ` C ) r ) C_ u )
54adantlr 477 . . . . . . . . . 10 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ u e. J ) -> A. y e. u E. r e. RR+ ( y ( ball ` C ) r ) C_ u )
6 ssralv 3219 . . . . . . . . . 10 |- ( ( u i^i Y ) C_ u -> ( A. y e. u E. r e. RR+ ( y ( ball ` C ) r ) C_ u -> A. y e. ( u i^i Y ) E. r e. RR+ ( y ( ball ` C ) r ) C_ u ) )
71, 5, 6mpsyl 65 . . . . . . . . 9 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ u e. J ) -> A. y e. ( u i^i Y ) E. r e. RR+ ( y ( ball ` C ) r ) C_ u )
8 ssrin 3360 . . . . . . . . . . 11 |- ( ( y ( ball ` C ) r ) C_ u -> ( ( y ( ball ` C ) r ) i^i Y ) C_ ( u i^i Y ) )
98reximi 2574 . . . . . . . . . 10 |- ( E. r e. RR+ ( y ( ball ` C ) r ) C_ u -> E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ ( u i^i Y ) )
109ralimi 2540 . . . . . . . . 9 |- ( A. y e. ( u i^i Y ) E. r e. RR+ ( y ( ball ` C ) r ) C_ u -> A. y e. ( u i^i Y ) E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ ( u i^i Y ) )
117, 10syl 14 . . . . . . . 8 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ u e. J ) -> A. y e. ( u i^i Y ) E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ ( u i^i Y ) )
12 inss2 3356 . . . . . . . 8 |- ( u i^i Y ) C_ Y
1311, 12jctil 312 . . . . . . 7 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ u e. J ) -> ( ( u i^i Y ) C_ Y /\ A. y e. ( u i^i Y ) E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ ( u i^i Y ) ) )
14 sseq1 3178 . . . . . . . 8 |- ( x = ( u i^i Y ) -> ( x C_ Y <-> ( u i^i Y ) C_ Y ) )
15 sseq2 3179 . . . . . . . . . 10 |- ( x = ( u i^i Y ) -> ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x <-> ( ( y ( ball ` C ) r ) i^i Y ) C_ ( u i^i Y ) ) )
1615rexbidv 2478 . . . . . . . . 9 |- ( x = ( u i^i Y ) -> ( E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x <-> E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ ( u i^i Y ) ) )
1716raleqbi1dv 2680 . . . . . . . 8 |- ( x = ( u i^i Y ) -> ( A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x <-> A. y e. ( u i^i Y ) E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ ( u i^i Y ) ) )
1814, 17anbi12d 473 . . . . . . 7 |- ( x = ( u i^i Y ) -> ( ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) <-> ( ( u i^i Y ) C_ Y /\ A. y e. ( u i^i Y ) E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ ( u i^i Y ) ) ) )
1913, 18syl5ibrcom 157 . . . . . 6 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ u e. J ) -> ( x = ( u i^i Y ) -> ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) )
2019rexlimdva 2594 . . . . 5 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( E. u e. J x = ( u i^i Y ) -> ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) )
212mopntop 13611 . . . . . . . . 9 |- ( C e. ( *Met ` X ) -> J e. Top )
2221ad2antrr 488 . . . . . . . 8 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> J e. Top )
23 ssel2 3150 . . . . . . . . . . . . . 14 |- ( ( x C_ Y /\ y e. x ) -> y e. Y )
24 ssel2 3150 . . . . . . . . . . . . . . . 16 |- ( ( Y C_ X /\ y e. Y ) -> y e. X )
25 rpxr 9648 . . . . . . . . . . . . . . . . . 18 |- ( r e. RR+ -> r e. RR* )
262blopn 13657 . . . . . . . . . . . . . . . . . . . 20 |- ( ( C e. ( *Met ` X ) /\ y e. X /\ r e. RR* ) -> ( y ( ball ` C ) r ) e. J )
27 eleq1a 2249 . . . . . . . . . . . . . . . . . . . 20 |- ( ( y ( ball ` C ) r ) e. J -> ( z = ( y ( ball ` C ) r ) -> z e. J ) )
2826, 27syl 14 . . . . . . . . . . . . . . . . . . 19 |- ( ( C e. ( *Met ` X ) /\ y e. X /\ r e. RR* ) -> ( z = ( y ( ball ` C ) r ) -> z e. J ) )
29283expa 1203 . . . . . . . . . . . . . . . . . 18 |- ( ( ( C e. ( *Met ` X ) /\ y e. X ) /\ r e. RR* ) -> ( z = ( y ( ball ` C ) r ) -> z e. J ) )
3025, 29sylan2 286 . . . . . . . . . . . . . . . . 17 |- ( ( ( C e. ( *Met ` X ) /\ y e. X ) /\ r e. RR+ ) -> ( z = ( y ( ball ` C ) r ) -> z e. J ) )
3130rexlimdva 2594 . . . . . . . . . . . . . . . 16 |- ( ( C e. ( *Met ` X ) /\ y e. X ) -> ( E. r e. RR+ z = ( y ( ball ` C ) r ) -> z e. J ) )
3224, 31sylan2 286 . . . . . . . . . . . . . . 15 |- ( ( C e. ( *Met ` X ) /\ ( Y C_ X /\ y e. Y ) ) -> ( E. r e. RR+ z = ( y ( ball ` C ) r ) -> z e. J ) )
3332anassrs 400 . . . . . . . . . . . . . 14 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ y e. Y ) -> ( E. r e. RR+ z = ( y ( ball ` C ) r ) -> z e. J ) )
3423, 33sylan2 286 . . . . . . . . . . . . 13 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ y e. x ) ) -> ( E. r e. RR+ z = ( y ( ball ` C ) r ) -> z e. J ) )
3534anassrs 400 . . . . . . . . . . . 12 |- ( ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ x C_ Y ) /\ y e. x ) -> ( E. r e. RR+ z = ( y ( ball ` C ) r ) -> z e. J ) )
3635rexlimdva 2594 . . . . . . . . . . 11 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ x C_ Y ) -> ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) -> z e. J ) )
3736adantrd 279 . . . . . . . . . 10 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ x C_ Y ) -> ( ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) -> z e. J ) )
3837adantrr 479 . . . . . . . . 9 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> ( ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) -> z e. J ) )
3938abssdv 3229 . . . . . . . 8 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } C_ J )
40 uniopn 13166 . . . . . . . 8 |- ( ( J e. Top /\ { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } C_ J ) -> U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } e. J )
4122, 39, 40syl2anc 411 . . . . . . 7 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } e. J )
42 oveq1 5876 . . . . . . . . . . . . . . . . . 18 |- ( y = u -> ( y ( ball ` C ) r ) = ( u ( ball ` C ) r ) )
4342ineq1d 3335 . . . . . . . . . . . . . . . . 17 |- ( y = u -> ( ( y ( ball ` C ) r ) i^i Y ) = ( ( u ( ball ` C ) r ) i^i Y ) )
4443sseq1d 3184 . . . . . . . . . . . . . . . 16 |- ( y = u -> ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x <-> ( ( u ( ball ` C ) r ) i^i Y ) C_ x ) )
4544rexbidv 2478 . . . . . . . . . . . . . . 15 |- ( y = u -> ( E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x <-> E. r e. RR+ ( ( u ( ball ` C ) r ) i^i Y ) C_ x ) )
4645rspccv 2838 . . . . . . . . . . . . . 14 |- ( A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x -> ( u e. x -> E. r e. RR+ ( ( u ( ball ` C ) r ) i^i Y ) C_ x ) )
4746ad2antll 491 . . . . . . . . . . . . 13 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> ( u e. x -> E. r e. RR+ ( ( u ( ball ` C ) r ) i^i Y ) C_ x ) )
48 ssel 3149 . . . . . . . . . . . . . . 15 |- ( x C_ Y -> ( u e. x -> u e. Y ) )
49 ssel 3149 . . . . . . . . . . . . . . . 16 |- ( Y C_ X -> ( u e. Y -> u e. X ) )
50 blcntr 13583 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( C e. ( *Met ` X ) /\ u e. X /\ r e. RR+ ) -> u e. ( u ( ball ` C ) r ) )
5150a1d 22 . . . . . . . . . . . . . . . . . . . 20 |- ( ( C e. ( *Met ` X ) /\ u e. X /\ r e. RR+ ) -> ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x -> u e. ( u ( ball ` C ) r ) ) )
5251ancld 325 . . . . . . . . . . . . . . . . . . 19 |- ( ( C e. ( *Met ` X ) /\ u e. X /\ r e. RR+ ) -> ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x -> ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( u ( ball ` C ) r ) ) ) )
53523expa 1203 . . . . . . . . . . . . . . . . . 18 |- ( ( ( C e. ( *Met ` X ) /\ u e. X ) /\ r e. RR+ ) -> ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x -> ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( u ( ball ` C ) r ) ) ) )
5453reximdva 2579 . . . . . . . . . . . . . . . . 17 |- ( ( C e. ( *Met ` X ) /\ u e. X ) -> ( E. r e. RR+ ( ( u ( ball ` C ) r ) i^i Y ) C_ x -> E. r e. RR+ ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( u ( ball ` C ) r ) ) ) )
5554ex 115 . . . . . . . . . . . . . . . 16 |- ( C e. ( *Met ` X ) -> ( u e. X -> ( E. r e. RR+ ( ( u ( ball ` C ) r ) i^i Y ) C_ x -> E. r e. RR+ ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( u ( ball ` C ) r ) ) ) ) )
5649, 55sylan9r 410 . . . . . . . . . . . . . . 15 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( u e. Y -> ( E. r e. RR+ ( ( u ( ball ` C ) r ) i^i Y ) C_ x -> E. r e. RR+ ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( u ( ball ` C ) r ) ) ) ) )
5748, 56sylan9r 410 . . . . . . . . . . . . . 14 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ x C_ Y ) -> ( u e. x -> ( E. r e. RR+ ( ( u ( ball ` C ) r ) i^i Y ) C_ x -> E. r e. RR+ ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( u ( ball ` C ) r ) ) ) ) )
5857adantrr 479 . . . . . . . . . . . . 13 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> ( u e. x -> ( E. r e. RR+ ( ( u ( ball ` C ) r ) i^i Y ) C_ x -> E. r e. RR+ ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( u ( ball ` C ) r ) ) ) ) )
5947, 58mpdd 41 . . . . . . . . . . . 12 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> ( u e. x -> E. r e. RR+ ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( u ( ball ` C ) r ) ) ) )
6042eleq2d 2247 . . . . . . . . . . . . . . . 16 |- ( y = u -> ( u e. ( y ( ball ` C ) r ) <-> u e. ( u ( ball ` C ) r ) ) )
6144, 60anbi12d 473 . . . . . . . . . . . . . . 15 |- ( y = u -> ( ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) <-> ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( u ( ball ` C ) r ) ) ) )
6261rexbidv 2478 . . . . . . . . . . . . . 14 |- ( y = u -> ( E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) <-> E. r e. RR+ ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( u ( ball ` C ) r ) ) ) )
6362rspcev 2841 . . . . . . . . . . . . 13 |- ( ( u e. x /\ E. r e. RR+ ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( u ( ball ` C ) r ) ) ) -> E. y e. x E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) )
6463ex 115 . . . . . . . . . . . 12 |- ( u e. x -> ( E. r e. RR+ ( ( ( u ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( u ( ball ` C ) r ) ) -> E. y e. x E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) ) )
6559, 64sylcom 28 . . . . . . . . . . 11 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> ( u e. x -> E. y e. x E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) ) )
66 simprl 529 . . . . . . . . . . . 12 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> x C_ Y )
6766sseld 3154 . . . . . . . . . . 11 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> ( u e. x -> u e. Y ) )
6865, 67jcad 307 . . . . . . . . . 10 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> ( u e. x -> ( E. y e. x E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) /\ u e. Y ) ) )
69 elin 3318 . . . . . . . . . . . . . . 15 |- ( u e. ( ( y ( ball ` C ) r ) i^i Y ) <-> ( u e. ( y ( ball ` C ) r ) /\ u e. Y ) )
70 ssel2 3150 . . . . . . . . . . . . . . 15 |- ( ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( ( y ( ball ` C ) r ) i^i Y ) ) -> u e. x )
7169, 70sylan2br 288 . . . . . . . . . . . . . 14 |- ( ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ ( u e. ( y ( ball ` C ) r ) /\ u e. Y ) ) -> u e. x )
7271expr 375 . . . . . . . . . . . . 13 |- ( ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) -> ( u e. Y -> u e. x ) )
7372rexlimivw 2590 . . . . . . . . . . . 12 |- ( E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) -> ( u e. Y -> u e. x ) )
7473rexlimivw 2590 . . . . . . . . . . 11 |- ( E. y e. x E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) -> ( u e. Y -> u e. x ) )
7574imp 124 . . . . . . . . . 10 |- ( ( E. y e. x E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) /\ u e. Y ) -> u e. x )
7668, 75impbid1 142 . . . . . . . . 9 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> ( u e. x <-> ( E. y e. x E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) /\ u e. Y ) ) )
77 elin 3318 . . . . . . . . . . 11 |- ( u e. ( U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } i^i Y ) <-> ( u e. U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } /\ u e. Y ) )
78 eluniab 3819 . . . . . . . . . . . . . 14 |- ( u e. U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } <-> E. z ( u e. z /\ ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) ) )
79 ancom 266 . . . . . . . . . . . . . . . 16 |- ( ( u e. z /\ ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) ) <-> ( ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) /\ u e. z ) )
80 anass 401 . . . . . . . . . . . . . . . 16 |- ( ( ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) /\ u e. z ) <-> ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) )
81 r19.41v 2633 . . . . . . . . . . . . . . . . . 18 |- ( E. r e. RR+ ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) <-> ( E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) )
8281rexbii 2484 . . . . . . . . . . . . . . . . 17 |- ( E. y e. x E. r e. RR+ ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) <-> E. y e. x ( E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) )
83 r19.41v 2633 . . . . . . . . . . . . . . . . 17 |- ( E. y e. x ( E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) <-> ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) )
8482, 83bitr2i 185 . . . . . . . . . . . . . . . 16 |- ( ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) <-> E. y e. x E. r e. RR+ ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) )
8579, 80, 843bitri 206 . . . . . . . . . . . . . . 15 |- ( ( u e. z /\ ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) ) <-> E. y e. x E. r e. RR+ ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) )
8685exbii 1605 . . . . . . . . . . . . . 14 |- ( E. z ( u e. z /\ ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) ) <-> E. z E. y e. x E. r e. RR+ ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) )
8778, 86bitri 184 . . . . . . . . . . . . 13 |- ( u e. U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } <-> E. z E. y e. x E. r e. RR+ ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) )
88 vex 2740 . . . . . . . . . . . . . . . . . . 19 |- y e. _V
89 blex 13554 . . . . . . . . . . . . . . . . . . 19 |- ( C e. ( *Met ` X ) -> ( ball ` C ) e. _V )
90 vex 2740 . . . . . . . . . . . . . . . . . . . 20 |- r e. _V
9190a1i 9 . . . . . . . . . . . . . . . . . . 19 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> r e. _V )
92 ovexg 5903 . . . . . . . . . . . . . . . . . . 19 |- ( ( y e. _V /\ ( ball ` C ) e. _V /\ r e. _V ) -> ( y ( ball ` C ) r ) e. _V )
9388, 89, 91, 92mp3an2ani 1344 . . . . . . . . . . . . . . . . . 18 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( y ( ball ` C ) r ) e. _V )
94 ineq1 3329 . . . . . . . . . . . . . . . . . . . . 21 |- ( z = ( y ( ball ` C ) r ) -> ( z i^i Y ) = ( ( y ( ball ` C ) r ) i^i Y ) )
9594sseq1d 3184 . . . . . . . . . . . . . . . . . . . 20 |- ( z = ( y ( ball ` C ) r ) -> ( ( z i^i Y ) C_ x <-> ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) )
96 eleq2 2241 . . . . . . . . . . . . . . . . . . . 20 |- ( z = ( y ( ball ` C ) r ) -> ( u e. z <-> u e. ( y ( ball ` C ) r ) ) )
9795, 96anbi12d 473 . . . . . . . . . . . . . . . . . . 19 |- ( z = ( y ( ball ` C ) r ) -> ( ( ( z i^i Y ) C_ x /\ u e. z ) <-> ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) ) )
9897ceqsexgv 2866 . . . . . . . . . . . . . . . . . 18 |- ( ( y ( ball ` C ) r ) e. _V -> ( E. z ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) <-> ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) ) )
9993, 98syl 14 . . . . . . . . . . . . . . . . 17 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( E. z ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) <-> ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) ) )
10099rexbidv 2478 . . . . . . . . . . . . . . . 16 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( E. r e. RR+ E. z ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) <-> E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) ) )
101 rexcom4 2760 . . . . . . . . . . . . . . . 16 |- ( E. r e. RR+ E. z ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) <-> E. z E. r e. RR+ ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) )
102100, 101bitr3di 195 . . . . . . . . . . . . . . 15 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) <-> E. z E. r e. RR+ ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) ) )
103102rexbidv 2478 . . . . . . . . . . . . . 14 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( E. y e. x E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) <-> E. y e. x E. z E. r e. RR+ ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) ) )
104 rexcom4 2760 . . . . . . . . . . . . . 14 |- ( E. y e. x E. z E. r e. RR+ ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) <-> E. z E. y e. x E. r e. RR+ ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) )
105103, 104bitr2di 197 . . . . . . . . . . . . 13 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( E. z E. y e. x E. r e. RR+ ( z = ( y ( ball ` C ) r ) /\ ( ( z i^i Y ) C_ x /\ u e. z ) ) <-> E. y e. x E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) ) )
10687, 105bitrid 192 . . . . . . . . . . . 12 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( u e. U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } <-> E. y e. x E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) ) )
107106anbi1d 465 . . . . . . . . . . 11 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( ( u e. U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } /\ u e. Y ) <-> ( E. y e. x E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) /\ u e. Y ) ) )
10877, 107bitr2id 193 . . . . . . . . . 10 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( ( E. y e. x E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) /\ u e. Y ) <-> u e. ( U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } i^i Y ) ) )
109108adantr 276 . . . . . . . . 9 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> ( ( E. y e. x E. r e. RR+ ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) /\ u e. Y ) <-> u e. ( U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } i^i Y ) ) )
11076, 109bitrd 188 . . . . . . . 8 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> ( u e. x <-> u e. ( U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } i^i Y ) ) )
111110eqrdv 2175 . . . . . . 7 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> x = ( U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } i^i Y ) )
112 ineq1 3329 . . . . . . . 8 |- ( u = U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } -> ( u i^i Y ) = ( U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } i^i Y ) )
113112rspceeqv 2859 . . . . . . 7 |- ( ( U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } e. J /\ x = ( U. { z | ( E. y e. x E. r e. RR+ z = ( y ( ball ` C ) r ) /\ ( z i^i Y ) C_ x ) } i^i Y ) ) -> E. u e. J x = ( u i^i Y ) )
11441, 111, 113syl2anc 411 . . . . . 6 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) -> E. u e. J x = ( u i^i Y ) )
115114ex 115 . . . . 5 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) -> E. u e. J x = ( u i^i Y ) ) )
11620, 115impbid 129 . . . 4 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( E. u e. J x = ( u i^i Y ) <-> ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) )
117 simpr 110 . . . . . . . . . . 11 |- ( ( Y C_ X /\ y e. Y ) -> y e. Y )
11824, 117elind 3320 . . . . . . . . . 10 |- ( ( Y C_ X /\ y e. Y ) -> y e. ( X i^i Y ) )
119 metrest.1 . . . . . . . . . . . . . . 15 |- D = ( C |` ( Y X. Y ) )
120119blres 13601 . . . . . . . . . . . . . 14 |- ( ( C e. ( *Met ` X ) /\ y e. ( X i^i Y ) /\ r e. RR* ) -> ( y ( ball ` D ) r ) = ( ( y ( ball ` C ) r ) i^i Y ) )
121120sseq1d 3184 . . . . . . . . . . . . 13 |- ( ( C e. ( *Met ` X ) /\ y e. ( X i^i Y ) /\ r e. RR* ) -> ( ( y ( ball ` D ) r ) C_ x <-> ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) )
1221213expa 1203 . . . . . . . . . . . 12 |- ( ( ( C e. ( *Met ` X ) /\ y e. ( X i^i Y ) ) /\ r e. RR* ) -> ( ( y ( ball ` D ) r ) C_ x <-> ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) )
12325, 122sylan2 286 . . . . . . . . . . 11 |- ( ( ( C e. ( *Met ` X ) /\ y e. ( X i^i Y ) ) /\ r e. RR+ ) -> ( ( y ( ball ` D ) r ) C_ x <-> ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) )
124123rexbidva 2474 . . . . . . . . . 10 |- ( ( C e. ( *Met ` X ) /\ y e. ( X i^i Y ) ) -> ( E. r e. RR+ ( y ( ball ` D ) r ) C_ x <-> E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) )
125118, 124sylan2 286 . . . . . . . . 9 |- ( ( C e. ( *Met ` X ) /\ ( Y C_ X /\ y e. Y ) ) -> ( E. r e. RR+ ( y ( ball ` D ) r ) C_ x <-> E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) )
126125anassrs 400 . . . . . . . 8 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ y e. Y ) -> ( E. r e. RR+ ( y ( ball ` D ) r ) C_ x <-> E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) )
12723, 126sylan2 286 . . . . . . 7 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ ( x C_ Y /\ y e. x ) ) -> ( E. r e. RR+ ( y ( ball ` D ) r ) C_ x <-> E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) )
128127anassrs 400 . . . . . 6 |- ( ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ x C_ Y ) /\ y e. x ) -> ( E. r e. RR+ ( y ( ball ` D ) r ) C_ x <-> E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) )
129128ralbidva 2473 . . . . 5 |- ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ x C_ Y ) -> ( A. y e. x E. r e. RR+ ( y ( ball ` D ) r ) C_ x <-> A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) )
130129pm5.32da 452 . . . 4 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( ( x C_ Y /\ A. y e. x E. r e. RR+ ( y ( ball ` D ) r ) C_ x ) <-> ( x C_ Y /\ A. y e. x E. r e. RR+ ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) ) )
131116, 130bitr4d 191 . . 3 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( E. u e. J x = ( u i^i Y ) <-> ( x C_ Y /\ A. y e. x E. r e. RR+ ( y ( ball ` D ) r ) C_ x ) ) )
13221adantr 276 . . . 4 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> J e. Top )
133 id 19 . . . . 5 |- ( Y C_ X -> Y C_ X )
1342mopnm 13615 . . . . 5 |- ( C e. ( *Met ` X ) -> X e. J )
135 ssexg 4139 . . . . 5 |- ( ( Y C_ X /\ X e. J ) -> Y e. _V )
136133, 134, 135syl2anr 290 . . . 4 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> Y e. _V )
137 elrest 12643 . . . 4 |- ( ( J e. Top /\ Y e. _V ) -> ( x e. ( J ↾t Y ) <-> E. u e. J x = ( u i^i Y ) ) )
138132, 136, 137syl2anc 411 . . 3 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( x e. ( J ↾t Y ) <-> E. u e. J x = ( u i^i Y ) ) )
139 xmetres2 13546 . . . . 5 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( C |` ( Y X. Y ) ) e. ( *Met ` Y ) )
140119, 139eqeltrid 2264 . . . 4 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> D e. ( *Met ` Y ) )
141 metrest.4 . . . . 5 |- K = ( MetOpen ` D )
142141elmopn2 13616 . . . 4 |- ( D e. ( *Met ` Y ) -> ( x e. K <-> ( x C_ Y /\ A. y e. x E. r e. RR+ ( y ( ball ` D ) r ) C_ x ) ) )
143140, 142syl 14 . . 3 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( x e. K <-> ( x C_ Y /\ A. y e. x E. r e. RR+ ( y ( ball ` D ) r ) C_ x ) ) )
144131, 138, 1433bitr4d 220 . 2 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( x e. ( J ↾t Y ) <-> x e. K ) )
145144eqrdv 2175 1 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( J ↾t Y ) = K )
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 978   = wceq 1353   E.wex 1492   e. wcel 2148   {cab 2163   A.wral 2455   E.wrex 2456   _Vcvv 2737   i^i cin 3128   C_ wss 3129   U.cuni 3807   X. cxp 4621   |` cres 4625   ` cfv 5212  (class class class)co 5869   RR*cxr 7981   RR+crp 9640   ↾t crest 12636   *Metcxmet 13147   ballcbl 13149   MetOpencmopn 13152   Topctop 13162
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584  ax-cnex 7893  ax-resscn 7894  ax-1cn 7895  ax-1re 7896  ax-icn 7897  ax-addcl 7898  ax-addrcl 7899  ax-mulcl 7900  ax-mulrcl 7901  ax-addcom 7902  ax-mulcom 7903  ax-addass 7904  ax-mulass 7905  ax-distr 7906  ax-i2m1 7907  ax-0lt1 7908  ax-1rid 7909  ax-0id 7910  ax-rnegex 7911  ax-precex 7912  ax-cnre 7913  ax-pre-ltirr 7914  ax-pre-ltwlin 7915  ax-pre-lttrn 7916  ax-pre-apti 7917  ax-pre-ltadd 7918  ax-pre-mulgt0 7919  ax-pre-mulext 7920  ax-arch 7921  ax-caucvg 7922
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-po 4293  df-iso 4294  df-iord 4363  df-on 4365  df-ilim 4366  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-isom 5221  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-recs 6300  df-frec 6386  df-map 6644  df-sup 6977  df-inf 6978  df-pnf 7984  df-mnf 7985  df-xr 7986  df-ltxr 7987  df-le 7988  df-sub 8120  df-neg 8121  df-reap 8522  df-ap 8529  df-div 8619  df-inn 8909  df-2 8967  df-3 8968  df-4 8969  df-n0 9166  df-z 9243  df-uz 9518  df-q 9609  df-rp 9641  df-xneg 9759  df-xadd 9760  df-seqfrec 10432  df-exp 10506  df-cj 10835  df-re 10836  df-im 10837  df-rsqrt 10991  df-abs 10992  df-rest 12638  df-topgen 12657  df-psmet 13154  df-xmet 13155  df-bl 13157  df-mopn 13158  df-top 13163  df-topon 13176  df-bases 13208
This theorem is referenced by:  resubmet  13715  tgioo2cntop  13716  divcnap  13722  cncfcncntop  13747  limcimolemlt  13800  cnplimcim  13803  cnplimclemr  13805  limccnpcntop  13811  limccnp2cntop  13813
  Copyright terms: Public domain W3C validator