Metamath Proof Explorer

Theorem metrest

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)

Ref Expression
Hypotheses metrest.1 
|- D = ( C |` ( Y X. Y ) )
metrest.3 
|- J = ( MetOpen ` C )
metrest.4 
|- K = ( MetOpen ` D )
Assertion metrest 
|- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( J |`t Y ) = K )

Proof

Step Hyp Ref Expression
1 metrest.1 
 |-  D = ( C |` ( Y X. Y ) )
2 metrest.3 
 |-  J = ( MetOpen ` C )
3 metrest.4 
 |-  K = ( MetOpen ` D )
4 inss1 
 |-  ( u i^i Y ) C_ u
5 2 elmopn2 
 |-  ( C e. ( *Met ` X ) -> ( u e. J <-> ( u C_ X /\ A. y e. u E. r e. RR+ ( y ( ball ` C ) r ) C_ u ) ) )
6 5 simplbda 
 |-  ( ( C e. ( *Met ` X ) /\ u e. J ) -> A. y e. u E. r e. RR+ ( y ( ball ` C ) r ) C_ u )
7 6 adantlr 
 |-  ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ u e. J ) -> A. y e. u E. r e. RR+ ( y ( ball ` C ) r ) C_ u )
8 ssralv 
 |-  ( ( 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 ) )
9 4 7 8 mpsyl 
 |-  ( ( ( 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 )
10 ssrin 
 |-  ( ( y ( ball ` C ) r ) C_ u -> ( ( y ( ball ` C ) r ) i^i Y ) C_ ( u i^i Y ) )
11 10 reximi 
 |-  ( 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 ) )
12 11 ralimi 
 |-  ( 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 ) )
13 9 12 syl 
 |-  ( ( ( 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 ) )
14 inss2 
 |-  ( u i^i Y ) C_ Y
15 13 14 jctil 
 |-  ( ( ( 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 ) ) )
16 sseq1 
 |-  ( x = ( u i^i Y ) -> ( x C_ Y <-> ( u i^i Y ) C_ Y ) )
17 sseq2 
 |-  ( 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 ) ) )
18 17 rexbidv 
 |-  ( 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 ) ) )
19 18 raleqbi1dv 
 |-  ( 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 ) ) )
20 16 19 anbi12d 
 |-  ( 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 ) ) ) )
21 15 20 syl5ibrcom 
 |-  ( ( ( 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 ) ) )
22 21 rexlimdva 
 |-  ( ( 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 ) ) )
23 2 mopntop 
 |-  ( C e. ( *Met ` X ) -> J e. Top )
24 23 ad2antrr 
 |-  ( ( ( 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 )
25 ssel2 
 |-  ( ( x C_ Y /\ y e. x ) -> y e. Y )
26 ssel2 
 |-  ( ( Y C_ X /\ y e. Y ) -> y e. X )
27 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
28 2 blopn 
 |-  ( ( C e. ( *Met ` X ) /\ y e. X /\ r e. RR* ) -> ( y ( ball ` C ) r ) e. J )
29 eleq1a 
 |-  ( ( y ( ball ` C ) r ) e. J -> ( z = ( y ( ball ` C ) r ) -> z e. J ) )
30 28 29 syl 
 |-  ( ( C e. ( *Met ` X ) /\ y e. X /\ r e. RR* ) -> ( z = ( y ( ball ` C ) r ) -> z e. J ) )
31 30 3expa 
 |-  ( ( ( C e. ( *Met ` X ) /\ y e. X ) /\ r e. RR* ) -> ( z = ( y ( ball ` C ) r ) -> z e. J ) )
32 27 31 sylan2 
 |-  ( ( ( C e. ( *Met ` X ) /\ y e. X ) /\ r e. RR+ ) -> ( z = ( y ( ball ` C ) r ) -> z e. J ) )
33 32 rexlimdva 
 |-  ( ( C e. ( *Met ` X ) /\ y e. X ) -> ( E. r e. RR+ z = ( y ( ball ` C ) r ) -> z e. J ) )
34 26 33 sylan2 
 |-  ( ( C e. ( *Met ` X ) /\ ( Y C_ X /\ y e. Y ) ) -> ( E. r e. RR+ z = ( y ( ball ` C ) r ) -> z e. J ) )
35 34 anassrs 
 |-  ( ( ( C e. ( *Met ` X ) /\ Y C_ X ) /\ y e. Y ) -> ( E. r e. RR+ z = ( y ( ball ` C ) r ) -> z e. J ) )
36 25 35 sylan2 
 |-  ( ( ( 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 ) )
37 36 anassrs 
 |-  ( ( ( ( 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 ) )
38 37 rexlimdva 
 |-  ( ( ( 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 ) )
39 38 adantrd 
 |-  ( ( ( 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 ) )
40 39 adantrr 
 |-  ( ( ( 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 ) )
41 40 abssdv 
 |-  ( ( ( 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 )
42 uniopn 
 |-  ( ( 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 )
43 24 41 42 syl2anc 
 |-  ( ( ( 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 )
44 oveq1 
 |-  ( y = u -> ( y ( ball ` C ) r ) = ( u ( ball ` C ) r ) )
45 44 ineq1d 
 |-  ( y = u -> ( ( y ( ball ` C ) r ) i^i Y ) = ( ( u ( ball ` C ) r ) i^i Y ) )
46 45 sseq1d 
 |-  ( y = u -> ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x <-> ( ( u ( ball ` C ) r ) i^i Y ) C_ x ) )
47 46 rexbidv 
 |-  ( 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 ) )
48 47 rspccv 
 |-  ( 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 ) )
49 48 ad2antll 
 |-  ( ( ( 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 ) )
50 ssel 
 |-  ( x C_ Y -> ( u e. x -> u e. Y ) )
51 ssel 
 |-  ( Y C_ X -> ( u e. Y -> u e. X ) )
52 blcntr 
 |-  ( ( C e. ( *Met ` X ) /\ u e. X /\ r e. RR+ ) -> u e. ( u ( ball ` C ) r ) )
53 52 a1d 
 |-  ( ( 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 ) ) )
54 53 ancld 
 |-  ( ( 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 ) ) ) )
55 54 3expa 
 |-  ( ( ( 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 ) ) ) )
56 55 reximdva 
 |-  ( ( 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 ) ) ) )
57 56 ex 
 |-  ( 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 ) ) ) ) )
58 51 57 sylan9r 
 |-  ( ( 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 ) ) ) ) )
59 50 58 sylan9r 
 |-  ( ( ( 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 ) ) ) ) )
60 59 adantrr 
 |-  ( ( ( 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 ) ) ) ) )
61 49 60 mpdd 
 |-  ( ( ( 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 ) ) ) )
62 44 eleq2d 
 |-  ( y = u -> ( u e. ( y ( ball ` C ) r ) <-> u e. ( u ( ball ` C ) r ) ) )
63 46 62 anbi12d 
 |-  ( 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 ) ) ) )
64 63 rexbidv 
 |-  ( 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 ) ) ) )
65 64 rspcev 
 |-  ( ( 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 ) ) )
66 65 ex 
 |-  ( 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 ) ) ) )
67 61 66 sylcom 
 |-  ( ( ( 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 ) ) ) )
68 simprl 
 |-  ( ( ( 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 )
69 68 sseld 
 |-  ( ( ( 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 ) )
70 67 69 jcad 
 |-  ( ( ( 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 ) ) )
71 elin 
 |-  ( u e. ( ( y ( ball ` C ) r ) i^i Y ) <-> ( u e. ( y ( ball ` C ) r ) /\ u e. Y ) )
72 ssel2 
 |-  ( ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( ( y ( ball ` C ) r ) i^i Y ) ) -> u e. x )
73 71 72 sylan2br 
 |-  ( ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ ( u e. ( y ( ball ` C ) r ) /\ u e. Y ) ) -> u e. x )
74 73 expr 
 |-  ( ( ( ( y ( ball ` C ) r ) i^i Y ) C_ x /\ u e. ( y ( ball ` C ) r ) ) -> ( u e. Y -> u e. x ) )
75 74 rexlimivw 
 |-  ( 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 ) )
76 75 rexlimivw 
 |-  ( 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 ) )
77 76 imp 
 |-  ( ( 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 )
78 70 77 impbid1 
 |-  ( ( ( 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 ) ) )
79 elin 
 |-  ( 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 ) )
80 eluniab 
 |-  ( 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 ) ) )
81 ancom 
 |-  ( ( 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 ) )
82 anass 
 |-  ( ( ( 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 
 |-  ( 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 ) ) )
84 83 rexbii 
 |-  ( 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 ) ) )
85 r19.41v 
 |-  ( 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 ) ) )
86 84 85 bitr2i 
 |-  ( ( 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 ) ) )
87 81 82 86 3bitri 
 |-  ( ( 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 ) ) )
88 87 exbii 
 |-  ( 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 ) ) )
89 ovex 
 |-  ( y ( ball ` C ) r ) e. _V
90 ineq1 
 |-  ( z = ( y ( ball ` C ) r ) -> ( z i^i Y ) = ( ( y ( ball ` C ) r ) i^i Y ) )
91 90 sseq1d 
 |-  ( z = ( y ( ball ` C ) r ) -> ( ( z i^i Y ) C_ x <-> ( ( y ( ball ` C ) r ) i^i Y ) C_ x ) )
92 eleq2 
 |-  ( z = ( y ( ball ` C ) r ) -> ( u e. z <-> u e. ( y ( ball ` C ) r ) ) )
93 91 92 anbi12d 
 |-  ( 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 ) ) ) )
94 89 93 ceqsexv 
 |-  ( 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 ) ) )
95 94 rexbii 
 |-  ( 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 ) ) )
96 rexcom4 
 |-  ( 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 ) ) )
97 95 96 bitr3i 
 |-  ( 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 ) ) )
98 97 rexbii 
 |-  ( 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 ) ) )
99 rexcom4 
 |-  ( 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 ) ) )
100 98 99 bitr2i 
 |-  ( 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 ) ) )
101 80 88 100 3bitri 
 |-  ( 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 ) ) )
102 101 anbi1i 
 |-  ( ( 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 ) )
103 79 102 bitr2i 
 |-  ( ( 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 ) )
104 78 103 bitrdi 
 |-  ( ( ( 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 ) ) )
105 104 eqrdv 
 |-  ( ( ( 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 ) )
106 ineq1 
 |-  ( 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 ) )
107 106 rspceeqv 
 |-  ( ( 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 ) )
108 43 105 107 syl2anc 
 |-  ( ( ( 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 ) )
109 108 ex 
 |-  ( ( 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 ) ) )
110 22 109 impbid 
 |-  ( ( 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 ) ) )
111 simpr 
 |-  ( ( Y C_ X /\ y e. Y ) -> y e. Y )
112 26 111 elind 
 |-  ( ( Y C_ X /\ y e. Y ) -> y e. ( X i^i Y ) )
113 1 blres 
 |-  ( ( C e. ( *Met ` X ) /\ y e. ( X i^i Y ) /\ r e. RR* ) -> ( y ( ball ` D ) r ) = ( ( y ( ball ` C ) r ) i^i Y ) )
114 113 sseq1d 
 |-  ( ( 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 ) )
115 114 3expa 
 |-  ( ( ( 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 ) )
116 27 115 sylan2 
 |-  ( ( ( 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 ) )
117 116 rexbidva 
 |-  ( ( 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 ) )
118 112 117 sylan2 
 |-  ( ( 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 ) )
119 118 anassrs 
 |-  ( ( ( 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 ) )
120 25 119 sylan2 
 |-  ( ( ( 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 ) )
121 120 anassrs 
 |-  ( ( ( ( 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 ) )
122 121 ralbidva 
 |-  ( ( ( 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 ) )
123 122 pm5.32da 
 |-  ( ( 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 ) ) )
124 110 123 bitr4d 
 |-  ( ( 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 ) ) )
125 id 
 |-  ( Y C_ X -> Y C_ X )
126 2 mopnm 
 |-  ( C e. ( *Met ` X ) -> X e. J )
127 ssexg 
 |-  ( ( Y C_ X /\ X e. J ) -> Y e. _V )
128 125 126 127 syl2anr 
 |-  ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> Y e. _V )
129 elrest 
 |-  ( ( J e. Top /\ Y e. _V ) -> ( x e. ( J |`t Y ) <-> E. u e. J x = ( u i^i Y ) ) )
130 23 128 129 syl2an2r 
 |-  ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( x e. ( J |`t Y ) <-> E. u e. J x = ( u i^i Y ) ) )
131 xmetres2 
 |-  ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( C |` ( Y X. Y ) ) e. ( *Met ` Y ) )
132 1 131 eqeltrid 
 |-  ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> D e. ( *Met ` Y ) )
133 3 elmopn2 
 |-  ( D e. ( *Met ` Y ) -> ( x e. K <-> ( x C_ Y /\ A. y e. x E. r e. RR+ ( y ( ball ` D ) r ) C_ x ) ) )
134 132 133 syl 
 |-  ( ( 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 ) ) )
135 124 130 134 3bitr4d 
 |-  ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( x e. ( J |`t Y ) <-> x e. K ) )
136 135 eqrdv 
 |-  ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( J |`t Y ) = K )