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 ) )