Metamath Proof Explorer

Theorem tmdcn2

Description: Write out the definition of continuity of +g explicitly. (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses tmdcn2.1 
|- B = ( Base ` G )
tmdcn2.2 
|- J = ( TopOpen ` G )
tmdcn2.3 
|- .+ = ( +g ` G )
Assertion tmdcn2 
|- ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> E. u e. J E. v e. J ( X e. u /\ Y e. v /\ A. x e. u A. y e. v ( x .+ y ) e. U ) )

Proof

Step Hyp Ref Expression
1 tmdcn2.1 
 |-  B = ( Base ` G )
2 tmdcn2.2 
 |-  J = ( TopOpen ` G )
3 tmdcn2.3 
 |-  .+ = ( +g ` G )
4 2 1 tmdtopon 
 |-  ( G e. TopMnd -> J e. ( TopOn ` B ) )
5 4 ad2antrr 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> J e. ( TopOn ` B ) )
6 eqid 
 |-  ( +f ` G ) = ( +f ` G )
7 2 6 tmdcn 
 |-  ( G e. TopMnd -> ( +f ` G ) e. ( ( J tX J ) Cn J ) )
8 7 ad2antrr 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> ( +f ` G ) e. ( ( J tX J ) Cn J ) )
9 simpr1 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> X e. B )
10 simpr2 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> Y e. B )
11 9 10 opelxpd 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> <. X , Y >. e. ( B X. B ) )
12 txtopon 
 |-  ( ( J e. ( TopOn ` B ) /\ J e. ( TopOn ` B ) ) -> ( J tX J ) e. ( TopOn ` ( B X. B ) ) )
13 5 5 12 syl2anc 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> ( J tX J ) e. ( TopOn ` ( B X. B ) ) )
14 toponuni 
 |-  ( ( J tX J ) e. ( TopOn ` ( B X. B ) ) -> ( B X. B ) = U. ( J tX J ) )
15 13 14 syl 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> ( B X. B ) = U. ( J tX J ) )
16 11 15 eleqtrd 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> <. X , Y >. e. U. ( J tX J ) )
17 eqid 
 |-  U. ( J tX J ) = U. ( J tX J )
18 17 cncnpi 
 |-  ( ( ( +f ` G ) e. ( ( J tX J ) Cn J ) /\ <. X , Y >. e. U. ( J tX J ) ) -> ( +f ` G ) e. ( ( ( J tX J ) CnP J ) ` <. X , Y >. ) )
19 8 16 18 syl2anc 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> ( +f ` G ) e. ( ( ( J tX J ) CnP J ) ` <. X , Y >. ) )
20 simplr 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> U e. J )
21 1 3 6 plusfval 
 |-  ( ( X e. B /\ Y e. B ) -> ( X ( +f ` G ) Y ) = ( X .+ Y ) )
22 9 10 21 syl2anc 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> ( X ( +f ` G ) Y ) = ( X .+ Y ) )
23 simpr3 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> ( X .+ Y ) e. U )
24 22 23 eqeltrd 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> ( X ( +f ` G ) Y ) e. U )
25 5 5 19 20 9 10 24 txcnpi 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> E. u e. J E. v e. J ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' ( +f ` G ) " U ) ) )
26 dfss3 
 |-  ( ( u X. v ) C_ ( `' ( +f ` G ) " U ) <-> A. z e. ( u X. v ) z e. ( `' ( +f ` G ) " U ) )
27 eleq1 
 |-  ( z = <. x , y >. -> ( z e. ( `' ( +f ` G ) " U ) <-> <. x , y >. e. ( `' ( +f ` G ) " U ) ) )
28 1 6 plusffn 
 |-  ( +f ` G ) Fn ( B X. B )
29 elpreima 
 |-  ( ( +f ` G ) Fn ( B X. B ) -> ( <. x , y >. e. ( `' ( +f ` G ) " U ) <-> ( <. x , y >. e. ( B X. B ) /\ ( ( +f ` G ) ` <. x , y >. ) e. U ) ) )
30 28 29 ax-mp 
 |-  ( <. x , y >. e. ( `' ( +f ` G ) " U ) <-> ( <. x , y >. e. ( B X. B ) /\ ( ( +f ` G ) ` <. x , y >. ) e. U ) )
31 27 30 bitrdi 
 |-  ( z = <. x , y >. -> ( z e. ( `' ( +f ` G ) " U ) <-> ( <. x , y >. e. ( B X. B ) /\ ( ( +f ` G ) ` <. x , y >. ) e. U ) ) )
32 31 ralxp 
 |-  ( A. z e. ( u X. v ) z e. ( `' ( +f ` G ) " U ) <-> A. x e. u A. y e. v ( <. x , y >. e. ( B X. B ) /\ ( ( +f ` G ) ` <. x , y >. ) e. U ) )
33 26 32 bitri 
 |-  ( ( u X. v ) C_ ( `' ( +f ` G ) " U ) <-> A. x e. u A. y e. v ( <. x , y >. e. ( B X. B ) /\ ( ( +f ` G ) ` <. x , y >. ) e. U ) )
34 opelxp 
 |-  ( <. x , y >. e. ( B X. B ) <-> ( x e. B /\ y e. B ) )
35 df-ov 
 |-  ( x ( +f ` G ) y ) = ( ( +f ` G ) ` <. x , y >. )
36 1 3 6 plusfval 
 |-  ( ( x e. B /\ y e. B ) -> ( x ( +f ` G ) y ) = ( x .+ y ) )
37 35 36 eqtr3id 
 |-  ( ( x e. B /\ y e. B ) -> ( ( +f ` G ) ` <. x , y >. ) = ( x .+ y ) )
38 34 37 sylbi 
 |-  ( <. x , y >. e. ( B X. B ) -> ( ( +f ` G ) ` <. x , y >. ) = ( x .+ y ) )
39 38 eleq1d 
 |-  ( <. x , y >. e. ( B X. B ) -> ( ( ( +f ` G ) ` <. x , y >. ) e. U <-> ( x .+ y ) e. U ) )
40 39 biimpa 
 |-  ( ( <. x , y >. e. ( B X. B ) /\ ( ( +f ` G ) ` <. x , y >. ) e. U ) -> ( x .+ y ) e. U )
41 40 2ralimi 
 |-  ( A. x e. u A. y e. v ( <. x , y >. e. ( B X. B ) /\ ( ( +f ` G ) ` <. x , y >. ) e. U ) -> A. x e. u A. y e. v ( x .+ y ) e. U )
42 33 41 sylbi 
 |-  ( ( u X. v ) C_ ( `' ( +f ` G ) " U ) -> A. x e. u A. y e. v ( x .+ y ) e. U )
43 42 3anim3i 
 |-  ( ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' ( +f ` G ) " U ) ) -> ( X e. u /\ Y e. v /\ A. x e. u A. y e. v ( x .+ y ) e. U ) )
44 43 reximi 
 |-  ( E. v e. J ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' ( +f ` G ) " U ) ) -> E. v e. J ( X e. u /\ Y e. v /\ A. x e. u A. y e. v ( x .+ y ) e. U ) )
45 44 reximi 
 |-  ( E. u e. J E. v e. J ( X e. u /\ Y e. v /\ ( u X. v ) C_ ( `' ( +f ` G ) " U ) ) -> E. u e. J E. v e. J ( X e. u /\ Y e. v /\ A. x e. u A. y e. v ( x .+ y ) e. U ) )
46 25 45 syl 
 |-  ( ( ( G e. TopMnd /\ U e. J ) /\ ( X e. B /\ Y e. B /\ ( X .+ Y ) e. U ) ) -> E. u e. J E. v e. J ( X e. u /\ Y e. v /\ A. x e. u A. y e. v ( x .+ y ) e. U ) )