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