Metamath Proof Explorer

Theorem txmetcn

Description: Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses metcn.2 
|- J = ( MetOpen ` C )
metcn.4 
|- K = ( MetOpen ` D )
txmetcnp.4 
|- L = ( MetOpen ` E )
Assertion txmetcn 
|- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> ( F e. ( ( J tX K ) Cn L ) <-> ( F : ( X X. Y ) --> Z /\ A. x e. X A. y e. Y A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) ) )

Proof

Step Hyp Ref Expression
1 metcn.2 
 |-  J = ( MetOpen ` C )
2 metcn.4 
 |-  K = ( MetOpen ` D )
3 txmetcnp.4 
 |-  L = ( MetOpen ` E )
4 1 mopntopon 
 |-  ( C e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
5 2 mopntopon 
 |-  ( D e. ( *Met ` Y ) -> K e. ( TopOn ` Y ) )
6 txtopon 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
7 4 5 6 syl2an 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
8 7 3adant3 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
9 3 mopntopon 
 |-  ( E e. ( *Met ` Z ) -> L e. ( TopOn ` Z ) )
10 9 3ad2ant3 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> L e. ( TopOn ` Z ) )
11 cncnp 
 |-  ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ L e. ( TopOn ` Z ) ) -> ( F e. ( ( J tX K ) Cn L ) <-> ( F : ( X X. Y ) --> Z /\ A. t e. ( X X. Y ) F e. ( ( ( J tX K ) CnP L ) ` t ) ) ) )
12 8 10 11 syl2anc 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> ( F e. ( ( J tX K ) Cn L ) <-> ( F : ( X X. Y ) --> Z /\ A. t e. ( X X. Y ) F e. ( ( ( J tX K ) CnP L ) ` t ) ) ) )
13 fveq2 
 |-  ( t = <. x , y >. -> ( ( ( J tX K ) CnP L ) ` t ) = ( ( ( J tX K ) CnP L ) ` <. x , y >. ) )
14 13 eleq2d 
 |-  ( t = <. x , y >. -> ( F e. ( ( ( J tX K ) CnP L ) ` t ) <-> F e. ( ( ( J tX K ) CnP L ) ` <. x , y >. ) ) )
15 14 ralxp 
 |-  ( A. t e. ( X X. Y ) F e. ( ( ( J tX K ) CnP L ) ` t ) <-> A. x e. X A. y e. Y F e. ( ( ( J tX K ) CnP L ) ` <. x , y >. ) )
16 simplr 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ F : ( X X. Y ) --> Z ) /\ ( x e. X /\ y e. Y ) ) -> F : ( X X. Y ) --> Z )
17 1 2 3 txmetcnp 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( x e. X /\ y e. Y ) ) -> ( F e. ( ( ( J tX K ) CnP L ) ` <. x , y >. ) <-> ( F : ( X X. Y ) --> Z /\ A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) ) )
18 17 adantlr 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ F : ( X X. Y ) --> Z ) /\ ( x e. X /\ y e. Y ) ) -> ( F e. ( ( ( J tX K ) CnP L ) ` <. x , y >. ) <-> ( F : ( X X. Y ) --> Z /\ A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) ) )
19 16 18 mpbirand 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ F : ( X X. Y ) --> Z ) /\ ( x e. X /\ y e. Y ) ) -> ( F e. ( ( ( J tX K ) CnP L ) ` <. x , y >. ) <-> A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) )
20 19 2ralbidva 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ F : ( X X. Y ) --> Z ) -> ( A. x e. X A. y e. Y F e. ( ( ( J tX K ) CnP L ) ` <. x , y >. ) <-> A. x e. X A. y e. Y A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) )
21 15 20 syl5bb 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ F : ( X X. Y ) --> Z ) -> ( A. t e. ( X X. Y ) F e. ( ( ( J tX K ) CnP L ) ` t ) <-> A. x e. X A. y e. Y A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) )
22 21 pm5.32da 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> ( ( F : ( X X. Y ) --> Z /\ A. t e. ( X X. Y ) F e. ( ( ( J tX K ) CnP L ) ` t ) ) <-> ( F : ( X X. Y ) --> Z /\ A. x e. X A. y e. Y A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) ) )
23 12 22 bitrd 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> ( F e. ( ( J tX K ) Cn L ) <-> ( F : ( X X. Y ) --> Z /\ A. x e. X A. y e. Y A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) ) )