ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  metrest Unicode version
Theorem metrest 14742
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 3383 . . . . . . . . . 10 |- ( u i^i Y ) C_ u
2 metrest.3 . . . . . . . . . . . . 13 |- J = ( MetOpen ` C )
32elmopn2 14685 . . . . . . . . . . . 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 3247 . . . . . . . . . 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 3388 . . . . . . . . . . 11 |- ( ( y ( ball ` C ) r ) C_ u -> ( ( y ( ball ` C ) r ) i^i Y ) C_ ( u i^i Y ) )
98reximi 2594 . . . . . . . . . 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 2560 . . . . . . . . 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 3384 . . . . . . . 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 3206 . . . . . . . 8 |- ( x = ( u i^i Y ) -> ( x C_ Y <-> ( u i^i Y ) C_ Y ) )
15 sseq2 3207 . . . . . . . . . 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 2498 . . . . . . . . 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 2705 . . . . . . . 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 2614 . . . . 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 14680 . . . . . . . . 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 3178 . . . . . . . . . . . . . 14 |- ( ( x C_ Y /\ y e. x ) -> y e. Y )
24 ssel2 3178 . . . . . . . . . . . . . . . 16 |- ( ( Y C_ X /\ y e. Y ) -> y e. X )
25 rpxr 9736 . . . . . . . . . . . . . . . . . 18 |- ( r e. RR+ -> r e. RR* )
262blopn 14726 . . . . . . . . . . . . . . . . . . . 20 |- ( ( C e. ( *Met ` X ) /\ y e. X /\ r e. RR* ) -> ( y ( ball ` C ) r ) e. J )
27 eleq1a 2268 . . . . . . . . . . . . . . . . . . . 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 1205 . . . . . . . . . . . . . . . . . 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 2614 . . . . . . . . . . . . . . . 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 2614 . . . . . . . . . . 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 3257 . . . . . . . 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 14237 . . . . . . . 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 5929 . . . . . . . . . . . . . . . . . 18 |- ( y = u -> ( y ( ball ` C ) r ) = ( u ( ball ` C ) r ) )
4342ineq1d 3363 . . . . . . . . . . . . . . . . 17 |- ( y = u -> ( ( y ( ball ` C ) r ) i^i Y ) = ( ( u ( ball ` C ) r ) i^i Y ) )
4443sseq1d 3212 . . . . . . . . . . . . . . . 16 |- ( y = u -> ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x <-> ( ( u ( ball ` C ) r ) i^i Y ) C_ x ) )
4544rexbidv 2498 . . . . . . . . . . . . . . 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 2865 . . . . . . . . . . . . . 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 3177 . . . . . . . . . . . . . . 15 |- ( x C_ Y -> ( u e. x -> u e. Y ) )
49 ssel 3177 . . . . . . . . . . . . . . . 16 |- ( Y C_ X -> ( u e. Y -> u e. X ) )
50 blcntr 14652 . . . . . . . . . . . . . . . . . . . . 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 1205 . . . . . . . . . . . . . . . . . 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 2599 . . . . . . . . . . . . . . . . 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 2266 . . . . . . . . . . . . . . . 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 2498 . . . . . . . . . . . . . 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 2868 . . . . . . . . . . . . 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 3182 . . . . . . . . . . 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 3346 . . . . . . . . . . . . . . 15 |- ( u e. ( ( y ( ball ` C ) r ) i^i Y ) <-> ( u e. ( y ( ball ` C ) r ) /\ u e. Y ) )
70 ssel2 3178 . . . . . . . . . . . . . . 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 2610 . . . . . . . . . . . 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 2610 . . . . . . . . . . 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 3346 . . . . . . . . . . 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 3851 . . . . . . . . . . . . . 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 2653 . . . . . . . . . . . . . . . . . 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 2504 . . . . . . . . . . . . . . . . 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 2653 . . . . . . . . . . . . . . . . 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 1619 . . . . . . . . . . . . . 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 2766 . . . . . . . . . . . . . . . . . . 19 |- y e. _V
89 blex 14623 . . . . . . . . . . . . . . . . . . 19 |- ( C e. ( *Met ` X ) -> ( ball ` C ) e. _V )
90 vex 2766 . . . . . . . . . . . . . . . . . . . 20 |- r e. _V
9190a1i 9 . . . . . . . . . . . . . . . . . . 19 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> r e. _V )
92 ovexg 5956 . . . . . . . . . . . . . . . . . . 19 |- ( ( y e. _V /\ ( ball ` C ) e. _V /\ r e. _V ) -> ( y ( ball ` C ) r ) e. _V )
9388, 89, 91, 92mp3an2ani 1355 . . . . . . . . . . . . . . . . . 18 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( y ( ball ` C ) r ) e. _V )
94 ineq1 3357 . . . . . . . . . . . . . . . . . . . . 21 |- ( z = ( y ( ball ` C ) r ) -> ( z i^i Y ) = ( ( y ( ball ` C ) r ) i^i Y ) )
9594sseq1d 3212 . . . . . . . . . . . . . . . . . . . 20 |- ( z = ( y ( ball ` C ) r ) -> ( ( z i^i Y ) C_ x <-> ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) )
96 eleq2 2260 . . . . . . . . . . . . . . . . . . . 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 2893 . . . . . . . . . . . . . . . . . 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 2498 . . . . . . . . . . . . . . . 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 2786 . . . . . . . . . . . . . . . 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 2498 . . . . . . . . . . . . . 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 2786 . . . . . . . . . . . . . 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 2194 . . . . . . 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 3357 . . . . . . . 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 2886 . . . . . . 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 3348 . . . . . . . . . 10 |- ( ( Y C_ X /\ y e. Y ) -> y e. ( X i^i Y ) )
119 metrest.1 . . . . . . . . . . . . . . 15 |- D = ( C |` ( Y X. Y ) )
120119blres 14670 . . . . . . . . . . . . . 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 3212 . . . . . . . . . . . . 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 1205 . . . . . . . . . . . 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 2494 . . . . . . . . . 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 2493 . . . . 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 14684 . . . . 5 |- ( C e. ( *Met ` X ) -> X e. J )
135 ssexg 4172 . . . . 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 12917 . . . 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 14615 . . . . 5 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( C |` ( Y X. Y ) ) e. ( *Met ` Y ) )
140119, 139eqeltrid 2283 . . . 4 |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> D e. ( *Met ` Y ) )
141 metrest.4 . . . . 5 |- K = ( MetOpen ` D )
142141elmopn2 14685 . . . 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 2194 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 980   = wceq 1364   E.wex 1506   e. wcel 2167   {cab 2182   A.wral 2475   E.wrex 2476   _Vcvv 2763   i^i cin 3156   C_ wss 3157   U.cuni 3839   X. cxp 4661   |` cres 4665   ` cfv 5258  (class class class)co 5922   RR*cxr 8060   RR+crp 9728   ↾t crest 12910   *Metcxmet 14092   ballcbl 14094   MetOpencmopn 14097   Topctop 14233
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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-nul 4159  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-iinf 4624  ax-cnex 7970  ax-resscn 7971  ax-1cn 7972  ax-1re 7973  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-mulrcl 7978  ax-addcom 7979  ax-mulcom 7980  ax-addass 7981  ax-mulass 7982  ax-distr 7983  ax-i2m1 7984  ax-0lt1 7985  ax-1rid 7986  ax-0id 7987  ax-rnegex 7988  ax-precex 7989  ax-cnre 7990  ax-pre-ltirr 7991  ax-pre-ltwlin 7992  ax-pre-lttrn 7993  ax-pre-apti 7994  ax-pre-ltadd 7995  ax-pre-mulgt0 7996  ax-pre-mulext 7997  ax-arch 7998  ax-caucvg 7999
This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rmo 2483  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3451  df-if 3562  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-iun 3918  df-br 4034  df-opab 4095  df-mpt 4096  df-tr 4132  df-id 4328  df-po 4331  df-iso 4332  df-iord 4401  df-on 4403  df-ilim 4404  df-suc 4406  df-iom 4627  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-isom 5267  df-riota 5877  df-ov 5925  df-oprab 5926  df-mpo 5927  df-1st 6198  df-2nd 6199  df-recs 6363  df-frec 6449  df-map 6709  df-sup 7050  df-inf 7051  df-pnf 8063  df-mnf 8064  df-xr 8065  df-ltxr 8066  df-le 8067  df-sub 8199  df-neg 8200  df-reap 8602  df-ap 8609  df-div 8700  df-inn 8991  df-2 9049  df-3 9050  df-4 9051  df-n0 9250  df-z 9327  df-uz 9602  df-q 9694  df-rp 9729  df-xneg 9847  df-xadd 9848  df-seqfrec 10540  df-exp 10631  df-cj 11007  df-re 11008  df-im 11009  df-rsqrt 11163  df-abs 11164  df-rest 12912  df-topgen 12931  df-psmet 14099  df-xmet 14100  df-bl 14102  df-mopn 14103  df-top 14234  df-topon 14247  df-bases 14279
This theorem is referenced by:  resubmet  14792  tgioo2cntop  14793  tgioo2  14795  divcnap  14801  cncfcncntop  14829  limcimolemlt  14900  cnplimcim  14903  cnplimclemr  14905  limccnpcntop  14911  limccnp2cntop  14913
  Copyright terms: Public domain W3C validator