ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  metrest Unicode version
Theorem metrest 15371
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 3441 . . . . . . . . . 10 |- ( u i^i Y ) C_ u
2 metrest.3 . . . . . . . . . . . . 13 |- J = ( MetOpen ` C )
32elmopn2 15314 . . . . . . . . . . . 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 3302 . . . . . . . . . 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 3446 . . . . . . . . . . 11 |- ( ( y ( ball ` C ) r ) C_ u -> ( ( y ( ball ` C ) r ) i^i Y ) C_ ( u i^i Y ) )
98reximi 2639 . . . . . . . . . 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 2605 . . . . . . . . 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 3442 . . . . . . . 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 3261 . . . . . . . 8 |- ( x = ( u i^i Y ) -> ( x C_ Y <-> ( u i^i Y ) C_ Y ) )
15 sseq2 3262 . . . . . . . . . 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 2543 . . . . . . . . 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 2753 . . . . . . . 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 2660 . . . . 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 15309 . . . . . . . . 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 3233 . . . . . . . . . . . . . 14 |- ( ( x C_ Y /\ y e. x ) -> y e. Y )
24 ssel2 3233 . . . . . . . . . . . . . . . 16 |- ( ( Y C_ X /\ y e. Y ) -> y e. X )
25 rpxr 9994 . . . . . . . . . . . . . . . . . 18 |- ( r e. RR+ -> r e. RR* )
262blopn 15355 . . . . . . . . . . . . . . . . . . . 20 |- ( ( C e. ( *Met ` X ) /\ y e. X /\ r e. RR* ) -> ( y ( ball ` C ) r ) e. J )
27 eleq1a 2304 . . . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . . 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 2660 . . . . . . . . . . . . . . . 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 2660 . . . . . . . . . . 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 3312 . . . . . . . 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 14866 . . . . . . . 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 6057 . . . . . . . . . . . . . . . . . 18 |- ( y = u -> ( y ( ball ` C ) r ) = ( u ( ball ` C ) r ) )
4342ineq1d 3421 . . . . . . . . . . . . . . . . 17 |- ( y = u -> ( ( y ( ball ` C ) r ) i^i Y ) = ( ( u ( ball ` C ) r ) i^i Y ) )
4443sseq1d 3267 . . . . . . . . . . . . . . . 16 |- ( y = u -> ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x <-> ( ( u ( ball ` C ) r ) i^i Y ) C_ x ) )
4544rexbidv 2543 . . . . . . . . . . . . . . 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 2918 . . . . . . . . . . . . . 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 3232 . . . . . . . . . . . . . . 15 |- ( x C_ Y -> ( u e. x -> u e. Y ) )
49 ssel 3232 . . . . . . . . . . . . . . . 16 |- ( Y C_ X -> ( u e. Y -> u e. X ) )
50 blcntr 15281 . . . . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . . 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 2644 . . . . . . . . . . . . . . . . 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 2302 . . . . . . . . . . . . . . . 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 2543 . . . . . . . . . . . . . 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 2921 . . . . . . . . . . . . 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 531 . . . . . . . . . . . 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 3237 . . . . . . . . . . 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 3402 . . . . . . . . . . . . . . 15 |- ( u e. ( ( y ( ball ` C ) r ) i^i Y ) <-> ( u e. ( y ( ball ` C ) r ) /\ u e. Y ) )
70 ssel2 3233 . . . . . . . . . . . . . . 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 2656 . . . . . . . . . . . 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 2656 . . . . . . . . . . 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 3402 . . . . . . . . . . 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 3926 . . . . . . . . . . . . . 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 2699 . . . . . . . . . . . . . . . . . 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 2549 . . . . . . . . . . . . . . . . 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 2699 . . . . . . . . . . . . . . . . 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 1654 . . . . . . . . . . . . . 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 2816 . . . . . . . . . . . . . . . . . . 19 |- y e. _V
89 blex 15252 . . . . . . . . . . . . . . . . . . 19 |- ( C e. ( *Met ` X ) -> ( ball ` C ) e. _V )
90 vex 2816 . . . . . . . . . . . . . . . . . . . 20 |- r e. _V
9190a1i 9 . . . . . . . . . . . . . . . . . . 19 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> r e. _V )
92 ovexg 6084 . . . . . . . . . . . . . . . . . . 19 |- ( ( y e. _V /\ ( ball ` C ) e. _V /\ r e. _V ) -> ( y ( ball ` C ) r ) e. _V )
9388, 89, 91, 92mp3an2ani 1381 . . . . . . . . . . . . . . . . . 18 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( y ( ball ` C ) r ) e. _V )
94 ineq1 3415 . . . . . . . . . . . . . . . . . . . . 21 |- ( z = ( y ( ball ` C ) r ) -> ( z i^i Y ) = ( ( y ( ball ` C ) r ) i^i Y ) )
9594sseq1d 3267 . . . . . . . . . . . . . . . . . . . 20 |- ( z = ( y ( ball ` C ) r ) -> ( ( z i^i Y ) C_ x <-> ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) )
96 eleq2 2296 . . . . . . . . . . . . . . . . . . . 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 2946 . . . . . . . . . . . . . . . . . 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 2543 . . . . . . . . . . . . . . . 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 2837 . . . . . . . . . . . . . . . 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 2543 . . . . . . . . . . . . . 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 2837 . . . . . . . . . . . . . 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 2230 . . . . . . 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 3415 . . . . . . . 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 2939 . . . . . . 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 3404 . . . . . . . . . 10 |- ( ( Y C_ X /\ y e. Y ) -> y e. ( X i^i Y ) )
119 metrest.1 . . . . . . . . . . . . . . 15 |- D = ( C |` ( Y X. Y ) )
120119blres 15299 . . . . . . . . . . . . . 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 3267 . . . . . . . . . . . . 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 1230 . . . . . . . . . . . 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 2539 . . . . . . . . . 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 2538 . . . . 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 15313 . . . . 5 |- ( C e. ( *Met ` X ) -> X e. J )
135 ssexg 4249 . . . . 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 13459 . . . 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 15244 . . . . 5 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( C |` ( Y X. Y ) ) e. ( *Met ` Y ) )
140119, 139eqeltrid 2319 . . . 4 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> D e. ( *Met ` Y ) )
141 metrest.4 . . . . 5 |- K = ( MetOpen ` D )
142141elmopn2 15314 . . . 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 2230 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 1005   = wceq 1398   E.wex 1541   e. wcel 2203   {cab 2218   A.wral 2520   E.wrex 2521   _Vcvv 2813   i^i cin 3210   C_ wss 3211   U.cuni 3914   X. cxp 4747   |` cres 4751   ` cfv 5352  (class class class)co 6050   RR*cxr 8307   RR+crp 9986   ↾t crest 13452   *Metcxmet 14684   ballcbl 14686   MetOpencmopn 14689   Topctop 14862
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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-coll 4225  ax-sep 4228  ax-nul 4236  ax-pow 4287  ax-pr 4322  ax-un 4554  ax-setind 4659  ax-iinf 4710  ax-cnex 8218  ax-resscn 8219  ax-1cn 8220  ax-1re 8221  ax-icn 8222  ax-addcl 8223  ax-addrcl 8224  ax-mulcl 8225  ax-mulrcl 8226  ax-addcom 8227  ax-mulcom 8228  ax-addass 8229  ax-mulass 8230  ax-distr 8231  ax-i2m1 8232  ax-0lt1 8233  ax-1rid 8234  ax-0id 8235  ax-rnegex 8236  ax-precex 8237  ax-cnre 8238  ax-pre-ltirr 8239  ax-pre-ltwlin 8240  ax-pre-lttrn 8241  ax-pre-apti 8242  ax-pre-ltadd 8243  ax-pre-mulgt0 8244  ax-pre-mulext 8245  ax-arch 8246  ax-caucvg 8247
This theorem depends on definitions:  df-bi 117  df-stab 839  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rmo 2528  df-rab 2529  df-v 2815  df-sbc 3043  df-csb 3139  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-nul 3509  df-if 3621  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-int 3950  df-iun 3993  df-br 4110  df-opab 4172  df-mpt 4173  df-tr 4209  df-id 4414  df-po 4417  df-iso 4418  df-iord 4487  df-on 4489  df-ilim 4490  df-suc 4492  df-iom 4713  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-res 4761  df-ima 4762  df-iota 5312  df-fun 5354  df-fn 5355  df-f 5356  df-f1 5357  df-fo 5358  df-f1o 5359  df-fv 5360  df-isom 5361  df-riota 6003  df-ov 6053  df-oprab 6054  df-mpo 6055  df-1st 6334  df-2nd 6335  df-recs 6536  df-frec 6622  df-map 6884  df-sup 7275  df-inf 7276  df-pnf 8310  df-mnf 8311  df-xr 8312  df-ltxr 8313  df-le 8314  df-sub 8446  df-neg 8447  df-reap 8849  df-ap 8856  df-div 8947  df-inn 9238  df-2 9296  df-3 9297  df-4 9298  df-n0 9497  df-z 9578  df-uz 9854  df-q 9952  df-rp 9987  df-xneg 10105  df-xadd 10106  df-seqfrec 10810  df-exp 10901  df-cj 11527  df-re 11528  df-im 11529  df-rsqrt 11683  df-abs 11684  df-rest 13454  df-topgen 13473  df-psmet 14691  df-xmet 14692  df-bl 14694  df-mopn 14695  df-top 14863  df-topon 14876  df-bases 14908
This theorem is referenced by:  resubmet  15421  tgioo2cntop  15422  tgioo2  15424  divcnap  15430  cncfcncntop  15458  limcimolemlt  15529  cnplimcim  15532  cnplimclemr  15534  limccnpcntop  15540  limccnp2cntop  15542
  Copyright terms: Public domain W3C validator