Metamath Proof Explorer

Theorem cnheiborlem

Description: Lemma for cnheibor . (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses cnheibor.2 โŠข ๐ฝ = ( TopOpen โ€˜ โ„‚fld )
cnheibor.3 โŠข ๐‘‡ = ( ๐ฝ โ†พt ๐‘‹ )
cnheibor.4 โŠข ๐น = ( ๐‘ฅ โˆˆ โ„ , ๐‘ฆ โˆˆ โ„ โ†ฆ ( ๐‘ฅ + ( i ยท ๐‘ฆ ) ) )
cnheibor.5 โŠข ๐‘Œ = ( ๐น โ€œ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) )
Assertion cnheiborlem ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ๐‘‡ โˆˆ Comp )

Proof

Step Hyp Ref Expression
1 cnheibor.2 โŠข ๐ฝ = ( TopOpen โ€˜ โ„‚fld )
2 cnheibor.3 โŠข ๐‘‡ = ( ๐ฝ โ†พt ๐‘‹ )
3 cnheibor.4 โŠข ๐น = ( ๐‘ฅ โˆˆ โ„ , ๐‘ฆ โˆˆ โ„ โ†ฆ ( ๐‘ฅ + ( i ยท ๐‘ฆ ) ) )
4 cnheibor.5 โŠข ๐‘Œ = ( ๐น โ€œ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) )
5 1 cnfldtop โŠข ๐ฝ โˆˆ Top
6 3 cnref1o โŠข ๐น : ( โ„ ร— โ„ ) โ€“1-1-ontoโ†’ โ„‚
7 f1ofn โŠข ( ๐น : ( โ„ ร— โ„ ) โ€“1-1-ontoโ†’ โ„‚ โ†’ ๐น Fn ( โ„ ร— โ„ ) )
8 elpreima โŠข ( ๐น Fn ( โ„ ร— โ„ ) โ†’ ( ๐‘ข โˆˆ ( โ—ก ๐น โ€œ ๐‘‹ ) โ†” ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) )
9 6 7 8 mp2b โŠข ( ๐‘ข โˆˆ ( โ—ก ๐น โ€œ ๐‘‹ ) โ†” ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) )
10 1st2nd2 โŠข ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โ†’ ๐‘ข = โŸจ ( 1st โ€˜ ๐‘ข ) , ( 2nd โ€˜ ๐‘ข ) โŸฉ )
11 10 ad2antrl โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ๐‘ข = โŸจ ( 1st โ€˜ ๐‘ข ) , ( 2nd โ€˜ ๐‘ข ) โŸฉ )
12 xp1st โŠข ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โ†’ ( 1st โ€˜ ๐‘ข ) โˆˆ โ„ )
13 12 ad2antrl โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( 1st โ€˜ ๐‘ข ) โˆˆ โ„ )
14 13 recnd โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( 1st โ€˜ ๐‘ข ) โˆˆ โ„‚ )
15 14 abscld โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( abs โ€˜ ( 1st โ€˜ ๐‘ข ) ) โˆˆ โ„ )
16 1 cnfldtopon โŠข ๐ฝ โˆˆ ( TopOn โ€˜ โ„‚ )
17 16 toponunii โŠข โ„‚ = โˆช ๐ฝ
18 17 cldss โŠข ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โ†’ ๐‘‹ โŠ† โ„‚ )
19 18 adantr โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ๐‘‹ โŠ† โ„‚ )
20 19 adantr โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ๐‘‹ โŠ† โ„‚ )
21 simprr โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ )
22 20 21 sseldd โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( ๐น โ€˜ ๐‘ข ) โˆˆ โ„‚ )
23 22 abscld โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( abs โ€˜ ( ๐น โ€˜ ๐‘ข ) ) โˆˆ โ„ )
24 simplrl โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ๐‘… โˆˆ โ„ )
25 simprl โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ๐‘ข โˆˆ ( โ„ ร— โ„ ) )
26 f1ocnvfv1 โŠข ( ( ๐น : ( โ„ ร— โ„ ) โ€“1-1-ontoโ†’ โ„‚ โˆง ๐‘ข โˆˆ ( โ„ ร— โ„ ) ) โ†’ ( โ—ก ๐น โ€˜ ( ๐น โ€˜ ๐‘ข ) ) = ๐‘ข )
27 6 25 26 sylancr โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( โ—ก ๐น โ€˜ ( ๐น โ€˜ ๐‘ข ) ) = ๐‘ข )
28 fveq2 โŠข ( ๐‘ง = ( ๐น โ€˜ ๐‘ข ) โ†’ ( โ„œ โ€˜ ๐‘ง ) = ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) )
29 fveq2 โŠข ( ๐‘ง = ( ๐น โ€˜ ๐‘ข ) โ†’ ( โ„‘ โ€˜ ๐‘ง ) = ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) )
30 28 29 opeq12d โŠข ( ๐‘ง = ( ๐น โ€˜ ๐‘ข ) โ†’ โŸจ ( โ„œ โ€˜ ๐‘ง ) , ( โ„‘ โ€˜ ๐‘ง ) โŸฉ = โŸจ ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) , ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) โŸฉ )
31 3 cnrecnv โŠข โ—ก ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ โŸจ ( โ„œ โ€˜ ๐‘ง ) , ( โ„‘ โ€˜ ๐‘ง ) โŸฉ )
32 opex โŠข โŸจ ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) , ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) โŸฉ โˆˆ V
33 30 31 32 fvmpt โŠข ( ( ๐น โ€˜ ๐‘ข ) โˆˆ โ„‚ โ†’ ( โ—ก ๐น โ€˜ ( ๐น โ€˜ ๐‘ข ) ) = โŸจ ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) , ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) โŸฉ )
34 22 33 syl โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( โ—ก ๐น โ€˜ ( ๐น โ€˜ ๐‘ข ) ) = โŸจ ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) , ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) โŸฉ )
35 27 34 eqtr3d โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ๐‘ข = โŸจ ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) , ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) โŸฉ )
36 35 fveq2d โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( 1st โ€˜ ๐‘ข ) = ( 1st โ€˜ โŸจ ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) , ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) โŸฉ ) )
37 fvex โŠข ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) โˆˆ V
38 fvex โŠข ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) โˆˆ V
39 37 38 op1st โŠข ( 1st โ€˜ โŸจ ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) , ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) โŸฉ ) = ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) )
40 36 39 eqtrdi โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( 1st โ€˜ ๐‘ข ) = ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) )
41 40 fveq2d โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( abs โ€˜ ( 1st โ€˜ ๐‘ข ) ) = ( abs โ€˜ ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) ) )
42 absrele โŠข ( ( ๐น โ€˜ ๐‘ข ) โˆˆ โ„‚ โ†’ ( abs โ€˜ ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) ) โ‰ค ( abs โ€˜ ( ๐น โ€˜ ๐‘ข ) ) )
43 22 42 syl โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( abs โ€˜ ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) ) โ‰ค ( abs โ€˜ ( ๐น โ€˜ ๐‘ข ) ) )
44 41 43 eqbrtrd โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( abs โ€˜ ( 1st โ€˜ ๐‘ข ) ) โ‰ค ( abs โ€˜ ( ๐น โ€˜ ๐‘ข ) ) )
45 fveq2 โŠข ( ๐‘ง = ( ๐น โ€˜ ๐‘ข ) โ†’ ( abs โ€˜ ๐‘ง ) = ( abs โ€˜ ( ๐น โ€˜ ๐‘ข ) ) )
46 45 breq1d โŠข ( ๐‘ง = ( ๐น โ€˜ ๐‘ข ) โ†’ ( ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… โ†” ( abs โ€˜ ( ๐น โ€˜ ๐‘ข ) ) โ‰ค ๐‘… ) )
47 simplrr โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… )
48 46 47 21 rspcdva โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( abs โ€˜ ( ๐น โ€˜ ๐‘ข ) ) โ‰ค ๐‘… )
49 15 23 24 44 48 letrd โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( abs โ€˜ ( 1st โ€˜ ๐‘ข ) ) โ‰ค ๐‘… )
50 13 24 absled โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( ( abs โ€˜ ( 1st โ€˜ ๐‘ข ) ) โ‰ค ๐‘… โ†” ( - ๐‘… โ‰ค ( 1st โ€˜ ๐‘ข ) โˆง ( 1st โ€˜ ๐‘ข ) โ‰ค ๐‘… ) ) )
51 49 50 mpbid โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( - ๐‘… โ‰ค ( 1st โ€˜ ๐‘ข ) โˆง ( 1st โ€˜ ๐‘ข ) โ‰ค ๐‘… ) )
52 51 simpld โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ - ๐‘… โ‰ค ( 1st โ€˜ ๐‘ข ) )
53 51 simprd โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( 1st โ€˜ ๐‘ข ) โ‰ค ๐‘… )
54 renegcl โŠข ( ๐‘… โˆˆ โ„ โ†’ - ๐‘… โˆˆ โ„ )
55 24 54 syl โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ - ๐‘… โˆˆ โ„ )
56 elicc2 โŠข ( ( - ๐‘… โˆˆ โ„ โˆง ๐‘… โˆˆ โ„ ) โ†’ ( ( 1st โ€˜ ๐‘ข ) โˆˆ ( - ๐‘… [,] ๐‘… ) โ†” ( ( 1st โ€˜ ๐‘ข ) โˆˆ โ„ โˆง - ๐‘… โ‰ค ( 1st โ€˜ ๐‘ข ) โˆง ( 1st โ€˜ ๐‘ข ) โ‰ค ๐‘… ) ) )
57 55 24 56 syl2anc โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( ( 1st โ€˜ ๐‘ข ) โˆˆ ( - ๐‘… [,] ๐‘… ) โ†” ( ( 1st โ€˜ ๐‘ข ) โˆˆ โ„ โˆง - ๐‘… โ‰ค ( 1st โ€˜ ๐‘ข ) โˆง ( 1st โ€˜ ๐‘ข ) โ‰ค ๐‘… ) ) )
58 13 52 53 57 mpbir3and โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( 1st โ€˜ ๐‘ข ) โˆˆ ( - ๐‘… [,] ๐‘… ) )
59 xp2nd โŠข ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โ†’ ( 2nd โ€˜ ๐‘ข ) โˆˆ โ„ )
60 59 ad2antrl โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( 2nd โ€˜ ๐‘ข ) โˆˆ โ„ )
61 60 recnd โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( 2nd โ€˜ ๐‘ข ) โˆˆ โ„‚ )
62 61 abscld โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( abs โ€˜ ( 2nd โ€˜ ๐‘ข ) ) โˆˆ โ„ )
63 35 fveq2d โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( 2nd โ€˜ ๐‘ข ) = ( 2nd โ€˜ โŸจ ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) , ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) โŸฉ ) )
64 37 38 op2nd โŠข ( 2nd โ€˜ โŸจ ( โ„œ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) , ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) โŸฉ ) = ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) )
65 63 64 eqtrdi โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( 2nd โ€˜ ๐‘ข ) = ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) )
66 65 fveq2d โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( abs โ€˜ ( 2nd โ€˜ ๐‘ข ) ) = ( abs โ€˜ ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) ) )
67 absimle โŠข ( ( ๐น โ€˜ ๐‘ข ) โˆˆ โ„‚ โ†’ ( abs โ€˜ ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) ) โ‰ค ( abs โ€˜ ( ๐น โ€˜ ๐‘ข ) ) )
68 22 67 syl โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( abs โ€˜ ( โ„‘ โ€˜ ( ๐น โ€˜ ๐‘ข ) ) ) โ‰ค ( abs โ€˜ ( ๐น โ€˜ ๐‘ข ) ) )
69 66 68 eqbrtrd โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( abs โ€˜ ( 2nd โ€˜ ๐‘ข ) ) โ‰ค ( abs โ€˜ ( ๐น โ€˜ ๐‘ข ) ) )
70 62 23 24 69 48 letrd โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( abs โ€˜ ( 2nd โ€˜ ๐‘ข ) ) โ‰ค ๐‘… )
71 60 24 absled โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( ( abs โ€˜ ( 2nd โ€˜ ๐‘ข ) ) โ‰ค ๐‘… โ†” ( - ๐‘… โ‰ค ( 2nd โ€˜ ๐‘ข ) โˆง ( 2nd โ€˜ ๐‘ข ) โ‰ค ๐‘… ) ) )
72 70 71 mpbid โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( - ๐‘… โ‰ค ( 2nd โ€˜ ๐‘ข ) โˆง ( 2nd โ€˜ ๐‘ข ) โ‰ค ๐‘… ) )
73 72 simpld โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ - ๐‘… โ‰ค ( 2nd โ€˜ ๐‘ข ) )
74 72 simprd โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( 2nd โ€˜ ๐‘ข ) โ‰ค ๐‘… )
75 elicc2 โŠข ( ( - ๐‘… โˆˆ โ„ โˆง ๐‘… โˆˆ โ„ ) โ†’ ( ( 2nd โ€˜ ๐‘ข ) โˆˆ ( - ๐‘… [,] ๐‘… ) โ†” ( ( 2nd โ€˜ ๐‘ข ) โˆˆ โ„ โˆง - ๐‘… โ‰ค ( 2nd โ€˜ ๐‘ข ) โˆง ( 2nd โ€˜ ๐‘ข ) โ‰ค ๐‘… ) ) )
76 55 24 75 syl2anc โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( ( 2nd โ€˜ ๐‘ข ) โˆˆ ( - ๐‘… [,] ๐‘… ) โ†” ( ( 2nd โ€˜ ๐‘ข ) โˆˆ โ„ โˆง - ๐‘… โ‰ค ( 2nd โ€˜ ๐‘ข ) โˆง ( 2nd โ€˜ ๐‘ข ) โ‰ค ๐‘… ) ) )
77 60 73 74 76 mpbir3and โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ( 2nd โ€˜ ๐‘ข ) โˆˆ ( - ๐‘… [,] ๐‘… ) )
78 58 77 opelxpd โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ โŸจ ( 1st โ€˜ ๐‘ข ) , ( 2nd โ€˜ ๐‘ข ) โŸฉ โˆˆ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) )
79 11 78 eqeltrd โŠข ( ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โˆง ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) ) โ†’ ๐‘ข โˆˆ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) )
80 79 ex โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ( ( ๐‘ข โˆˆ ( โ„ ร— โ„ ) โˆง ( ๐น โ€˜ ๐‘ข ) โˆˆ ๐‘‹ ) โ†’ ๐‘ข โˆˆ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) )
81 9 80 biimtrid โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ( ๐‘ข โˆˆ ( โ—ก ๐น โ€œ ๐‘‹ ) โ†’ ๐‘ข โˆˆ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) )
82 81 ssrdv โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ( โ—ก ๐น โ€œ ๐‘‹ ) โŠ† ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) )
83 f1ofun โŠข ( ๐น : ( โ„ ร— โ„ ) โ€“1-1-ontoโ†’ โ„‚ โ†’ Fun ๐น )
84 6 83 ax-mp โŠข Fun ๐น
85 f1ofo โŠข ( ๐น : ( โ„ ร— โ„ ) โ€“1-1-ontoโ†’ โ„‚ โ†’ ๐น : ( โ„ ร— โ„ ) โ€“ontoโ†’ โ„‚ )
86 forn โŠข ( ๐น : ( โ„ ร— โ„ ) โ€“ontoโ†’ โ„‚ โ†’ ran ๐น = โ„‚ )
87 6 85 86 mp2b โŠข ran ๐น = โ„‚
88 19 87 sseqtrrdi โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ๐‘‹ โŠ† ran ๐น )
89 funimass1 โŠข ( ( Fun ๐น โˆง ๐‘‹ โŠ† ran ๐น ) โ†’ ( ( โ—ก ๐น โ€œ ๐‘‹ ) โŠ† ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) โ†’ ๐‘‹ โŠ† ( ๐น โ€œ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) ) )
90 84 88 89 sylancr โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ( ( โ—ก ๐น โ€œ ๐‘‹ ) โŠ† ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) โ†’ ๐‘‹ โŠ† ( ๐น โ€œ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) ) )
91 82 90 mpd โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ๐‘‹ โŠ† ( ๐น โ€œ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) )
92 91 4 sseqtrrdi โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ๐‘‹ โŠ† ๐‘Œ )
93 eqid โŠข ( topGen โ€˜ ran (,) ) = ( topGen โ€˜ ran (,) )
94 3 93 1 cnrehmeo โŠข ๐น โˆˆ ( ( ( topGen โ€˜ ran (,) ) ร—t ( topGen โ€˜ ran (,) ) ) Homeo ๐ฝ )
95 imaexg โŠข ( ๐น โˆˆ ( ( ( topGen โ€˜ ran (,) ) ร—t ( topGen โ€˜ ran (,) ) ) Homeo ๐ฝ ) โ†’ ( ๐น โ€œ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) โˆˆ V )
96 94 95 ax-mp โŠข ( ๐น โ€œ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) โˆˆ V
97 4 96 eqeltri โŠข ๐‘Œ โˆˆ V
98 97 a1i โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ๐‘Œ โˆˆ V )
99 restabs โŠข ( ( ๐ฝ โˆˆ Top โˆง ๐‘‹ โŠ† ๐‘Œ โˆง ๐‘Œ โˆˆ V ) โ†’ ( ( ๐ฝ โ†พt ๐‘Œ ) โ†พt ๐‘‹ ) = ( ๐ฝ โ†พt ๐‘‹ ) )
100 5 92 98 99 mp3an2i โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ( ( ๐ฝ โ†พt ๐‘Œ ) โ†พt ๐‘‹ ) = ( ๐ฝ โ†พt ๐‘‹ ) )
101 100 2 eqtr4di โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ( ( ๐ฝ โ†พt ๐‘Œ ) โ†พt ๐‘‹ ) = ๐‘‡ )
102 4 oveq2i โŠข ( ๐ฝ โ†พt ๐‘Œ ) = ( ๐ฝ โ†พt ( ๐น โ€œ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) )
103 ishmeo โŠข ( ๐น โˆˆ ( ( ( topGen โ€˜ ran (,) ) ร—t ( topGen โ€˜ ran (,) ) ) Homeo ๐ฝ ) โ†” ( ๐น โˆˆ ( ( ( topGen โ€˜ ran (,) ) ร—t ( topGen โ€˜ ran (,) ) ) Cn ๐ฝ ) โˆง โ—ก ๐น โˆˆ ( ๐ฝ Cn ( ( topGen โ€˜ ran (,) ) ร—t ( topGen โ€˜ ran (,) ) ) ) ) )
104 94 103 mpbi โŠข ( ๐น โˆˆ ( ( ( topGen โ€˜ ran (,) ) ร—t ( topGen โ€˜ ran (,) ) ) Cn ๐ฝ ) โˆง โ—ก ๐น โˆˆ ( ๐ฝ Cn ( ( topGen โ€˜ ran (,) ) ร—t ( topGen โ€˜ ran (,) ) ) ) )
105 104 simpli โŠข ๐น โˆˆ ( ( ( topGen โ€˜ ran (,) ) ร—t ( topGen โ€˜ ran (,) ) ) Cn ๐ฝ )
106 iccssre โŠข ( ( - ๐‘… โˆˆ โ„ โˆง ๐‘… โˆˆ โ„ ) โ†’ ( - ๐‘… [,] ๐‘… ) โŠ† โ„ )
107 54 106 mpancom โŠข ( ๐‘… โˆˆ โ„ โ†’ ( - ๐‘… [,] ๐‘… ) โŠ† โ„ )
108 1 93 rerest โŠข ( ( - ๐‘… [,] ๐‘… ) โŠ† โ„ โ†’ ( ๐ฝ โ†พt ( - ๐‘… [,] ๐‘… ) ) = ( ( topGen โ€˜ ran (,) ) โ†พt ( - ๐‘… [,] ๐‘… ) ) )
109 107 108 syl โŠข ( ๐‘… โˆˆ โ„ โ†’ ( ๐ฝ โ†พt ( - ๐‘… [,] ๐‘… ) ) = ( ( topGen โ€˜ ran (,) ) โ†พt ( - ๐‘… [,] ๐‘… ) ) )
110 109 109 oveq12d โŠข ( ๐‘… โˆˆ โ„ โ†’ ( ( ๐ฝ โ†พt ( - ๐‘… [,] ๐‘… ) ) ร—t ( ๐ฝ โ†พt ( - ๐‘… [,] ๐‘… ) ) ) = ( ( ( topGen โ€˜ ran (,) ) โ†พt ( - ๐‘… [,] ๐‘… ) ) ร—t ( ( topGen โ€˜ ran (,) ) โ†พt ( - ๐‘… [,] ๐‘… ) ) ) )
111 retop โŠข ( topGen โ€˜ ran (,) ) โˆˆ Top
112 ovex โŠข ( - ๐‘… [,] ๐‘… ) โˆˆ V
113 txrest โŠข ( ( ( ( topGen โ€˜ ran (,) ) โˆˆ Top โˆง ( topGen โ€˜ ran (,) ) โˆˆ Top ) โˆง ( ( - ๐‘… [,] ๐‘… ) โˆˆ V โˆง ( - ๐‘… [,] ๐‘… ) โˆˆ V ) ) โ†’ ( ( ( topGen โ€˜ ran (,) ) ร—t ( topGen โ€˜ ran (,) ) ) โ†พt ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) = ( ( ( topGen โ€˜ ran (,) ) โ†พt ( - ๐‘… [,] ๐‘… ) ) ร—t ( ( topGen โ€˜ ran (,) ) โ†พt ( - ๐‘… [,] ๐‘… ) ) ) )
114 111 111 112 112 113 mp4an โŠข ( ( ( topGen โ€˜ ran (,) ) ร—t ( topGen โ€˜ ran (,) ) ) โ†พt ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) = ( ( ( topGen โ€˜ ran (,) ) โ†พt ( - ๐‘… [,] ๐‘… ) ) ร—t ( ( topGen โ€˜ ran (,) ) โ†พt ( - ๐‘… [,] ๐‘… ) ) )
115 110 114 eqtr4di โŠข ( ๐‘… โˆˆ โ„ โ†’ ( ( ๐ฝ โ†พt ( - ๐‘… [,] ๐‘… ) ) ร—t ( ๐ฝ โ†พt ( - ๐‘… [,] ๐‘… ) ) ) = ( ( ( topGen โ€˜ ran (,) ) ร—t ( topGen โ€˜ ran (,) ) ) โ†พt ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) )
116 eqid โŠข ( ( topGen โ€˜ ran (,) ) โ†พt ( - ๐‘… [,] ๐‘… ) ) = ( ( topGen โ€˜ ran (,) ) โ†พt ( - ๐‘… [,] ๐‘… ) )
117 93 116 icccmp โŠข ( ( - ๐‘… โˆˆ โ„ โˆง ๐‘… โˆˆ โ„ ) โ†’ ( ( topGen โ€˜ ran (,) ) โ†พt ( - ๐‘… [,] ๐‘… ) ) โˆˆ Comp )
118 54 117 mpancom โŠข ( ๐‘… โˆˆ โ„ โ†’ ( ( topGen โ€˜ ran (,) ) โ†พt ( - ๐‘… [,] ๐‘… ) ) โˆˆ Comp )
119 109 118 eqeltrd โŠข ( ๐‘… โˆˆ โ„ โ†’ ( ๐ฝ โ†พt ( - ๐‘… [,] ๐‘… ) ) โˆˆ Comp )
120 txcmp โŠข ( ( ( ๐ฝ โ†พt ( - ๐‘… [,] ๐‘… ) ) โˆˆ Comp โˆง ( ๐ฝ โ†พt ( - ๐‘… [,] ๐‘… ) ) โˆˆ Comp ) โ†’ ( ( ๐ฝ โ†พt ( - ๐‘… [,] ๐‘… ) ) ร—t ( ๐ฝ โ†พt ( - ๐‘… [,] ๐‘… ) ) ) โˆˆ Comp )
121 119 119 120 syl2anc โŠข ( ๐‘… โˆˆ โ„ โ†’ ( ( ๐ฝ โ†พt ( - ๐‘… [,] ๐‘… ) ) ร—t ( ๐ฝ โ†พt ( - ๐‘… [,] ๐‘… ) ) ) โˆˆ Comp )
122 115 121 eqeltrrd โŠข ( ๐‘… โˆˆ โ„ โ†’ ( ( ( topGen โ€˜ ran (,) ) ร—t ( topGen โ€˜ ran (,) ) ) โ†พt ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) โˆˆ Comp )
123 imacmp โŠข ( ( ๐น โˆˆ ( ( ( topGen โ€˜ ran (,) ) ร—t ( topGen โ€˜ ran (,) ) ) Cn ๐ฝ ) โˆง ( ( ( topGen โ€˜ ran (,) ) ร—t ( topGen โ€˜ ran (,) ) ) โ†พt ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) โˆˆ Comp ) โ†’ ( ๐ฝ โ†พt ( ๐น โ€œ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) ) โˆˆ Comp )
124 105 122 123 sylancr โŠข ( ๐‘… โˆˆ โ„ โ†’ ( ๐ฝ โ†พt ( ๐น โ€œ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) ) โˆˆ Comp )
125 102 124 eqeltrid โŠข ( ๐‘… โˆˆ โ„ โ†’ ( ๐ฝ โ†พt ๐‘Œ ) โˆˆ Comp )
126 125 ad2antrl โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ( ๐ฝ โ†พt ๐‘Œ ) โˆˆ Comp )
127 imassrn โŠข ( ๐น โ€œ ( ( - ๐‘… [,] ๐‘… ) ร— ( - ๐‘… [,] ๐‘… ) ) ) โŠ† ran ๐น
128 4 127 eqsstri โŠข ๐‘Œ โŠ† ran ๐น
129 f1of โŠข ( ๐น : ( โ„ ร— โ„ ) โ€“1-1-ontoโ†’ โ„‚ โ†’ ๐น : ( โ„ ร— โ„ ) โŸถ โ„‚ )
130 frn โŠข ( ๐น : ( โ„ ร— โ„ ) โŸถ โ„‚ โ†’ ran ๐น โŠ† โ„‚ )
131 6 129 130 mp2b โŠข ran ๐น โŠ† โ„‚
132 128 131 sstri โŠข ๐‘Œ โŠ† โ„‚
133 simpl โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) )
134 17 restcldi โŠข ( ( ๐‘Œ โŠ† โ„‚ โˆง ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ๐‘‹ โŠ† ๐‘Œ ) โ†’ ๐‘‹ โˆˆ ( Clsd โ€˜ ( ๐ฝ โ†พt ๐‘Œ ) ) )
135 132 133 92 134 mp3an2i โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ๐‘‹ โˆˆ ( Clsd โ€˜ ( ๐ฝ โ†พt ๐‘Œ ) ) )
136 cmpcld โŠข ( ( ( ๐ฝ โ†พt ๐‘Œ ) โˆˆ Comp โˆง ๐‘‹ โˆˆ ( Clsd โ€˜ ( ๐ฝ โ†พt ๐‘Œ ) ) ) โ†’ ( ( ๐ฝ โ†พt ๐‘Œ ) โ†พt ๐‘‹ ) โˆˆ Comp )
137 126 135 136 syl2anc โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ( ( ๐ฝ โ†พt ๐‘Œ ) โ†พt ๐‘‹ ) โˆˆ Comp )
138 101 137 eqeltrrd โŠข ( ( ๐‘‹ โˆˆ ( Clsd โ€˜ ๐ฝ ) โˆง ( ๐‘… โˆˆ โ„ โˆง โˆ€ ๐‘ง โˆˆ ๐‘‹ ( abs โ€˜ ๐‘ง ) โ‰ค ๐‘… ) ) โ†’ ๐‘‡ โˆˆ Comp )