Metamath Proof Explorer

Theorem ismtyhmeolem

Description: Lemma for ismtyhmeo . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypotheses ismtyhmeo.1 
|- J = ( MetOpen ` M )
ismtyhmeo.2 
|- K = ( MetOpen ` N )
ismtyhmeolem.3 
|- ( ph -> M e. ( *Met ` X ) )
ismtyhmeolem.4 
|- ( ph -> N e. ( *Met ` Y ) )
ismtyhmeolem.5 
|- ( ph -> F e. ( M Ismty N ) )
Assertion ismtyhmeolem 
|- ( ph -> F e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 ismtyhmeo.1 
 |-  J = ( MetOpen ` M )
2 ismtyhmeo.2 
 |-  K = ( MetOpen ` N )
3 ismtyhmeolem.3 
 |-  ( ph -> M e. ( *Met ` X ) )
4 ismtyhmeolem.4 
 |-  ( ph -> N e. ( *Met ` Y ) )
5 ismtyhmeolem.5 
 |-  ( ph -> F e. ( M Ismty N ) )
6 isismty 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( F e. ( M Ismty N ) <-> ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) ) )
7 3 4 6 syl2anc 
 |-  ( ph -> ( F e. ( M Ismty N ) <-> ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) ) )
8 5 7 mpbid 
 |-  ( ph -> ( F : X -1-1-onto-> Y /\ A. x e. X A. y e. X ( x M y ) = ( ( F ` x ) N ( F ` y ) ) ) )
9 8 simpld 
 |-  ( ph -> F : X -1-1-onto-> Y )
10 f1of 
 |-  ( F : X -1-1-onto-> Y -> F : X --> Y )
11 9 10 syl 
 |-  ( ph -> F : X --> Y )
12 4 adantr 
 |-  ( ( ph /\ ( w e. Y /\ r e. RR* ) ) -> N e. ( *Met ` Y ) )
13 3 adantr 
 |-  ( ( ph /\ ( w e. Y /\ r e. RR* ) ) -> M e. ( *Met ` X ) )
14 ismtycnv 
 |-  ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( F e. ( M Ismty N ) -> `' F e. ( N Ismty M ) ) )
15 3 4 14 syl2anc 
 |-  ( ph -> ( F e. ( M Ismty N ) -> `' F e. ( N Ismty M ) ) )
16 5 15 mpd 
 |-  ( ph -> `' F e. ( N Ismty M ) )
17 16 adantr 
 |-  ( ( ph /\ ( w e. Y /\ r e. RR* ) ) -> `' F e. ( N Ismty M ) )
18 simprl 
 |-  ( ( ph /\ ( w e. Y /\ r e. RR* ) ) -> w e. Y )
19 simprr 
 |-  ( ( ph /\ ( w e. Y /\ r e. RR* ) ) -> r e. RR* )
20 ismtyima 
 |-  ( ( ( N e. ( *Met ` Y ) /\ M e. ( *Met ` X ) /\ `' F e. ( N Ismty M ) ) /\ ( w e. Y /\ r e. RR* ) ) -> ( `' F " ( w ( ball ` N ) r ) ) = ( ( `' F ` w ) ( ball ` M ) r ) )
21 12 13 17 18 19 20 syl32anc 
 |-  ( ( ph /\ ( w e. Y /\ r e. RR* ) ) -> ( `' F " ( w ( ball ` N ) r ) ) = ( ( `' F ` w ) ( ball ` M ) r ) )
22 f1ocnv 
 |-  ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )
23 f1of 
 |-  ( `' F : Y -1-1-onto-> X -> `' F : Y --> X )
24 9 22 23 3syl 
 |-  ( ph -> `' F : Y --> X )
25 simpl 
 |-  ( ( w e. Y /\ r e. RR* ) -> w e. Y )
26 ffvelrn 
 |-  ( ( `' F : Y --> X /\ w e. Y ) -> ( `' F ` w ) e. X )
27 24 25 26 syl2an 
 |-  ( ( ph /\ ( w e. Y /\ r e. RR* ) ) -> ( `' F ` w ) e. X )
28 1 blopn 
 |-  ( ( M e. ( *Met ` X ) /\ ( `' F ` w ) e. X /\ r e. RR* ) -> ( ( `' F ` w ) ( ball ` M ) r ) e. J )
29 13 27 19 28 syl3anc 
 |-  ( ( ph /\ ( w e. Y /\ r e. RR* ) ) -> ( ( `' F ` w ) ( ball ` M ) r ) e. J )
30 21 29 eqeltrd 
 |-  ( ( ph /\ ( w e. Y /\ r e. RR* ) ) -> ( `' F " ( w ( ball ` N ) r ) ) e. J )
31 30 ralrimivva 
 |-  ( ph -> A. w e. Y A. r e. RR* ( `' F " ( w ( ball ` N ) r ) ) e. J )
32 fveq2 
 |-  ( z = <. w , r >. -> ( ( ball ` N ) ` z ) = ( ( ball ` N ) ` <. w , r >. ) )
33 df-ov 
 |-  ( w ( ball ` N ) r ) = ( ( ball ` N ) ` <. w , r >. )
34 32 33 eqtr4di 
 |-  ( z = <. w , r >. -> ( ( ball ` N ) ` z ) = ( w ( ball ` N ) r ) )
35 34 imaeq2d 
 |-  ( z = <. w , r >. -> ( `' F " ( ( ball ` N ) ` z ) ) = ( `' F " ( w ( ball ` N ) r ) ) )
36 35 eleq1d 
 |-  ( z = <. w , r >. -> ( ( `' F " ( ( ball ` N ) ` z ) ) e. J <-> ( `' F " ( w ( ball ` N ) r ) ) e. J ) )
37 36 ralxp 
 |-  ( A. z e. ( Y X. RR* ) ( `' F " ( ( ball ` N ) ` z ) ) e. J <-> A. w e. Y A. r e. RR* ( `' F " ( w ( ball ` N ) r ) ) e. J )
38 31 37 sylibr 
 |-  ( ph -> A. z e. ( Y X. RR* ) ( `' F " ( ( ball ` N ) ` z ) ) e. J )
39 blf 
 |-  ( N e. ( *Met ` Y ) -> ( ball ` N ) : ( Y X. RR* ) --> ~P Y )
40 ffn 
 |-  ( ( ball ` N ) : ( Y X. RR* ) --> ~P Y -> ( ball ` N ) Fn ( Y X. RR* ) )
41 imaeq2 
 |-  ( u = ( ( ball ` N ) ` z ) -> ( `' F " u ) = ( `' F " ( ( ball ` N ) ` z ) ) )
42 41 eleq1d 
 |-  ( u = ( ( ball ` N ) ` z ) -> ( ( `' F " u ) e. J <-> ( `' F " ( ( ball ` N ) ` z ) ) e. J ) )
43 42 ralrn 
 |-  ( ( ball ` N ) Fn ( Y X. RR* ) -> ( A. u e. ran ( ball ` N ) ( `' F " u ) e. J <-> A. z e. ( Y X. RR* ) ( `' F " ( ( ball ` N ) ` z ) ) e. J ) )
44 4 39 40 43 4syl 
 |-  ( ph -> ( A. u e. ran ( ball ` N ) ( `' F " u ) e. J <-> A. z e. ( Y X. RR* ) ( `' F " ( ( ball ` N ) ` z ) ) e. J ) )
45 38 44 mpbird 
 |-  ( ph -> A. u e. ran ( ball ` N ) ( `' F " u ) e. J )
46 1 mopntopon 
 |-  ( M e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
47 3 46 syl 
 |-  ( ph -> J e. ( TopOn ` X ) )
48 2 mopnval 
 |-  ( N e. ( *Met ` Y ) -> K = ( topGen ` ran ( ball ` N ) ) )
49 4 48 syl 
 |-  ( ph -> K = ( topGen ` ran ( ball ` N ) ) )
50 2 mopntopon 
 |-  ( N e. ( *Met ` Y ) -> K e. ( TopOn ` Y ) )
51 4 50 syl 
 |-  ( ph -> K e. ( TopOn ` Y ) )
52 47 49 51 tgcn 
 |-  ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. u e. ran ( ball ` N ) ( `' F " u ) e. J ) ) )
53 11 45 52 mpbir2and 
 |-  ( ph -> F e. ( J Cn K ) )