Step | Hyp | Ref
| Expression |
1 | | limccl 25255 |
. . . 4
β’ (πΉ limβ πΆ) β
β |
2 | | limcresi 25265 |
. . . . . 6
β’ (πΉ limβ πΆ) β ((πΉ βΎ π΅) limβ πΆ) |
3 | 2 | rgenw 3069 |
. . . . 5
β’
βπ₯ β
π΄ (πΉ limβ πΆ) β ((πΉ βΎ π΅) limβ πΆ) |
4 | | ssiin 5020 |
. . . . 5
β’ ((πΉ limβ πΆ) β β© π₯ β π΄ ((πΉ βΎ π΅) limβ πΆ) β βπ₯ β π΄ (πΉ limβ πΆ) β ((πΉ βΎ π΅) limβ πΆ)) |
5 | 3, 4 | mpbir 230 |
. . . 4
β’ (πΉ limβ πΆ) β β© π₯ β π΄ ((πΉ βΎ π΅) limβ πΆ) |
6 | 1, 5 | ssini 4196 |
. . 3
β’ (πΉ limβ πΆ) β (β β©
β© π₯ β π΄ ((πΉ βΎ π΅) limβ πΆ)) |
7 | 6 | a1i 11 |
. 2
β’ (π β (πΉ limβ πΆ) β (β β© β© π₯ β π΄ ((πΉ βΎ π΅) limβ πΆ))) |
8 | | elriin 5046 |
. . . 4
β’ (π¦ β (β β© β© π₯ β π΄ ((πΉ βΎ π΅) limβ πΆ)) β (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) |
9 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β π¦ β β) |
10 | | limciun.1 |
. . . . . . . . . . 11
β’ (π β π΄ β Fin) |
11 | 10 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β π΄ β Fin) |
12 | | simplrr 777 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ)) |
13 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯πΉ |
14 | | nfcsb1v 3885 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯β¦π / π₯β¦π΅ |
15 | 13, 14 | nfres 5944 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯(πΉ βΎ β¦π / π₯β¦π΅) |
16 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯
limβ |
17 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯πΆ |
18 | 15, 16, 17 | nfov 7392 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯((πΉ βΎ β¦π / π₯β¦π΅) limβ πΆ) |
19 | 18 | nfcri 2895 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯ π¦ β ((πΉ βΎ β¦π / π₯β¦π΅) limβ πΆ) |
20 | | csbeq1a 3874 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π β π΅ = β¦π / π₯β¦π΅) |
21 | 20 | reseq2d 5942 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π β (πΉ βΎ π΅) = (πΉ βΎ β¦π / π₯β¦π΅)) |
22 | 21 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π β ((πΉ βΎ π΅) limβ πΆ) = ((πΉ βΎ β¦π / π₯β¦π΅) limβ πΆ)) |
23 | 22 | eleq2d 2824 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (π¦ β ((πΉ βΎ π΅) limβ πΆ) β π¦ β ((πΉ βΎ β¦π / π₯β¦π΅) limβ πΆ))) |
24 | 19, 23 | rspc 3572 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β (βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ) β π¦ β ((πΉ βΎ β¦π / π₯β¦π΅) limβ πΆ))) |
25 | 12, 24 | mpan9 508 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ π β π΄) β π¦ β ((πΉ βΎ β¦π / π₯β¦π΅) limβ πΆ)) |
26 | | limciun.3 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ:βͺ π₯ β π΄ π΅βΆβ) |
27 | 26 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ π β π΄) β πΉ:βͺ π₯ β π΄ π΅βΆβ) |
28 | | ssiun2 5012 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΄ β β¦π / π₯β¦π΅ β βͺ
π β π΄ β¦π / π₯β¦π΅) |
29 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²ππ΅ |
30 | 29, 14, 20 | cbviun 5001 |
. . . . . . . . . . . . . . . . . . . 20
β’ βͺ π₯ β π΄ π΅ = βͺ π β π΄ β¦π / π₯β¦π΅ |
31 | 28, 30 | sseqtrrdi 4000 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΄ β β¦π / π₯β¦π΅ β βͺ
π₯ β π΄ π΅) |
32 | 31 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ π β π΄) β β¦π / π₯β¦π΅ β βͺ
π₯ β π΄ π΅) |
33 | 27, 32 | fssresd 6714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ π β π΄) β (πΉ βΎ β¦π / π₯β¦π΅):β¦π / π₯β¦π΅βΆβ) |
34 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ π β π΄) β π β π΄) |
35 | | limciun.2 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β βπ₯ β π΄ π΅ β β) |
36 | 35 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ π β π΄) β βπ₯ β π΄ π΅ β β) |
37 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯β |
38 | 14, 37 | nfss 3941 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯β¦π / π₯β¦π΅ β β |
39 | 20 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π β (π΅ β β β β¦π / π₯β¦π΅ β β)) |
40 | 38, 39 | rspc 3572 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΄ β (βπ₯ β π΄ π΅ β β β β¦π / π₯β¦π΅ β β)) |
41 | 34, 36, 40 | sylc 65 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ π β π΄) β β¦π / π₯β¦π΅ β β) |
42 | | limciun.4 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΆ β β) |
43 | 42 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ π β π΄) β πΆ β β) |
44 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(TopOpenββfld) =
(TopOpenββfld) |
45 | 33, 41, 43, 44 | ellimc2 25257 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ π β π΄) β (π¦ β ((πΉ βΎ β¦π / π₯β¦π΅) limβ πΆ) β (π¦ β β β§ βπ’ β
(TopOpenββfld)(π¦ β π’ β βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’))))) |
46 | 45 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ π β π΄) β (π¦ β ((πΉ βΎ β¦π / π₯β¦π΅) limβ πΆ) β (π¦ β β β§ βπ’ β
(TopOpenββfld)(π¦ β π’ β βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’))))) |
47 | 25, 46 | mpbid 231 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ π β π΄) β (π¦ β β β§ βπ’ β
(TopOpenββfld)(π¦ β π’ β βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’)))) |
48 | 47 | simprd 497 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ π β π΄) β βπ’ β
(TopOpenββfld)(π¦ β π’ β βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’))) |
49 | | simplrl 776 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ π β π΄) β π’ β
(TopOpenββfld)) |
50 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ π β π΄) β π¦ β π’) |
51 | | rsp 3233 |
. . . . . . . . . . . . 13
β’
(βπ’ β
(TopOpenββfld)(π¦ β π’ β βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’)) β (π’ β (TopOpenββfld)
β (π¦ β π’ β βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’)))) |
52 | 48, 49, 50, 51 | syl3c 66 |
. . . . . . . . . . . 12
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ π β π΄) β βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’)) |
53 | 52 | ralrimiva 3144 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β βπ β π΄ βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’)) |
54 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²πβπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ π΅) β (π β© (π΅ β {πΆ}))) β π’) |
55 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²π₯(TopOpenββfld) |
56 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²π₯ πΆ β π |
57 | | nfcv 2908 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯π |
58 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯{πΆ} |
59 | 14, 58 | nfdif 4090 |
. . . . . . . . . . . . . . . . 17
β’
β²π₯(β¦π / π₯β¦π΅ β {πΆ}) |
60 | 57, 59 | nfin 4181 |
. . . . . . . . . . . . . . . 16
β’
β²π₯(π β© (β¦π / π₯β¦π΅ β {πΆ})) |
61 | 15, 60 | nfima 6026 |
. . . . . . . . . . . . . . 15
β’
β²π₯((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) |
62 | | nfcv 2908 |
. . . . . . . . . . . . . . 15
β’
β²π₯π’ |
63 | 61, 62 | nfss 3941 |
. . . . . . . . . . . . . 14
β’
β²π₯((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’ |
64 | 56, 63 | nfan 1903 |
. . . . . . . . . . . . 13
β’
β²π₯(πΆ β π β§ ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’) |
65 | 55, 64 | nfrexw 3299 |
. . . . . . . . . . . 12
β’
β²π₯βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’) |
66 | 20 | difeq1d 4086 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (π΅ β {πΆ}) = (β¦π / π₯β¦π΅ β {πΆ})) |
67 | 66 | ineq2d 4177 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β (π β© (π΅ β {πΆ})) = (π β© (β¦π / π₯β¦π΅ β {πΆ}))) |
68 | 21, 67 | imaeq12d 6019 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π β ((πΉ βΎ π΅) β (π β© (π΅ β {πΆ}))) = ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ})))) |
69 | 68 | sseq1d 3980 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (((πΉ βΎ π΅) β (π β© (π΅ β {πΆ}))) β π’ β ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’)) |
70 | 69 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((πΆ β π β§ ((πΉ βΎ π΅) β (π β© (π΅ β {πΆ}))) β π’) β (πΆ β π β§ ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’))) |
71 | 70 | rexbidv 3176 |
. . . . . . . . . . . 12
β’ (π₯ = π β (βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ π΅) β (π β© (π΅ β {πΆ}))) β π’) β βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’))) |
72 | 54, 65, 71 | cbvralw 3292 |
. . . . . . . . . . 11
β’
(βπ₯ β
π΄ βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ π΅) β (π β© (π΅ β {πΆ}))) β π’) β βπ β π΄ βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ β¦π / π₯β¦π΅) β (π β© (β¦π / π₯β¦π΅ β {πΆ}))) β π’)) |
73 | 53, 72 | sylibr 233 |
. . . . . . . . . 10
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β βπ₯ β π΄ βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ π΅) β (π β© (π΅ β {πΆ}))) β π’)) |
74 | | eleq2 2827 |
. . . . . . . . . . . 12
β’ (π = (πβπ₯) β (πΆ β π β πΆ β (πβπ₯))) |
75 | | ineq1 4170 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ₯) β (π β© (π΅ β {πΆ})) = ((πβπ₯) β© (π΅ β {πΆ}))) |
76 | 75 | imaeq2d 6018 |
. . . . . . . . . . . . 13
β’ (π = (πβπ₯) β ((πΉ βΎ π΅) β (π β© (π΅ β {πΆ}))) = ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ})))) |
77 | 76 | sseq1d 3980 |
. . . . . . . . . . . 12
β’ (π = (πβπ₯) β (((πΉ βΎ π΅) β (π β© (π΅ β {πΆ}))) β π’ β ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’)) |
78 | 74, 77 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π = (πβπ₯) β ((πΆ β π β§ ((πΉ βΎ π΅) β (π β© (π΅ β {πΆ}))) β π’) β (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) |
79 | 78 | ac6sfi 9238 |
. . . . . . . . . 10
β’ ((π΄ β Fin β§ βπ₯ β π΄ βπ β
(TopOpenββfld)(πΆ β π β§ ((πΉ βΎ π΅) β (π β© (π΅ β {πΆ}))) β π’)) β βπ(π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) |
80 | 11, 73, 79 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β βπ(π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) |
81 | 44 | cnfldtop 24163 |
. . . . . . . . . . 11
β’
(TopOpenββfld) β Top |
82 | | frn 6680 |
. . . . . . . . . . . 12
β’ (π:π΄βΆ(TopOpenββfld)
β ran π β
(TopOpenββfld)) |
83 | 82 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β ran π β
(TopOpenββfld)) |
84 | 11 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β π΄ β Fin) |
85 | | ffn 6673 |
. . . . . . . . . . . . . 14
β’ (π:π΄βΆ(TopOpenββfld)
β π Fn π΄) |
86 | 85 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β π Fn π΄) |
87 | | dffn4 6767 |
. . . . . . . . . . . . 13
β’ (π Fn π΄ β π:π΄βontoβran π) |
88 | 86, 87 | sylib 217 |
. . . . . . . . . . . 12
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β π:π΄βontoβran π) |
89 | | fofi 9289 |
. . . . . . . . . . . 12
β’ ((π΄ β Fin β§ π:π΄βontoβran π) β ran π β Fin) |
90 | 84, 88, 89 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β ran π β Fin) |
91 | | unicntop 24165 |
. . . . . . . . . . . 12
β’ β =
βͺ
(TopOpenββfld) |
92 | 91 | rintopn 22274 |
. . . . . . . . . . 11
β’
(((TopOpenββfld) β Top β§ ran π β
(TopOpenββfld) β§ ran π β Fin) β (β β© β© ran π) β
(TopOpenββfld)) |
93 | 81, 83, 90, 92 | mp3an2i 1467 |
. . . . . . . . . 10
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β (β β© β© ran π) β
(TopOpenββfld)) |
94 | 42 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β πΆ β β) |
95 | 94 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β πΆ β β) |
96 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’) β πΆ β (πβπ₯)) |
97 | 96 | ralimi 3087 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’) β βπ₯ β π΄ πΆ β (πβπ₯)) |
98 | 97 | ad2antll 728 |
. . . . . . . . . . . 12
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β βπ₯ β π΄ πΆ β (πβπ₯)) |
99 | | eleq2 2827 |
. . . . . . . . . . . . . 14
β’ (π§ = (πβπ₯) β (πΆ β π§ β πΆ β (πβπ₯))) |
100 | 99 | ralrn 7043 |
. . . . . . . . . . . . 13
β’ (π Fn π΄ β (βπ§ β ran π πΆ β π§ β βπ₯ β π΄ πΆ β (πβπ₯))) |
101 | 86, 100 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β (βπ§ β ran π πΆ β π§ β βπ₯ β π΄ πΆ β (πβπ₯))) |
102 | 98, 101 | mpbird 257 |
. . . . . . . . . . 11
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β βπ§ β ran π πΆ β π§) |
103 | | elrint 4957 |
. . . . . . . . . . 11
β’ (πΆ β (β β© β© ran π) β (πΆ β β β§ βπ§ β ran π πΆ β π§)) |
104 | 95, 102, 103 | sylanbrc 584 |
. . . . . . . . . 10
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β πΆ β (β β© β© ran π)) |
105 | | indifcom 4237 |
. . . . . . . . . . . . . 14
β’ ((β
β© β© ran π) β© (βͺ
π₯ β π΄ π΅ β {πΆ})) = (βͺ
π₯ β π΄ π΅ β© ((β β© β© ran π) β {πΆ})) |
106 | | iunin1 5037 |
. . . . . . . . . . . . . 14
β’ βͺ π₯ β π΄ (π΅ β© ((β β© β© ran π) β {πΆ})) = (βͺ
π₯ β π΄ π΅ β© ((β β© β© ran π) β {πΆ})) |
107 | 105, 106 | eqtr4i 2768 |
. . . . . . . . . . . . 13
β’ ((β
β© β© ran π) β© (βͺ
π₯ β π΄ π΅ β {πΆ})) = βͺ
π₯ β π΄ (π΅ β© ((β β© β© ran π) β {πΆ})) |
108 | 107 | imaeq2i 6016 |
. . . . . . . . . . . 12
β’ (πΉ β ((β β© β© ran π) β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) = (πΉ β βͺ
π₯ β π΄ (π΅ β© ((β β© β© ran π) β {πΆ}))) |
109 | | imaiun 7197 |
. . . . . . . . . . . 12
β’ (πΉ β βͺ π₯ β π΄ (π΅ β© ((β β© β© ran π) β {πΆ}))) = βͺ
π₯ β π΄ (πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) |
110 | 108, 109 | eqtri 2765 |
. . . . . . . . . . 11
β’ (πΉ β ((β β© β© ran π) β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) = βͺ
π₯ β π΄ (πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) |
111 | | inss2 4194 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β
β© β© ran π) β β© ran
π |
112 | | fnfvelrn 7036 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π Fn π΄ β§ π₯ β π΄) β (πβπ₯) β ran π) |
113 | 85, 112 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π:π΄βΆ(TopOpenββfld)
β§ π₯ β π΄) β (πβπ₯) β ran π) |
114 | | intss1 4929 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πβπ₯) β ran π β β© ran
π β (πβπ₯)) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π:π΄βΆ(TopOpenββfld)
β§ π₯ β π΄) β β© ran π
β (πβπ₯)) |
116 | 111, 115 | sstrid 3960 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π:π΄βΆ(TopOpenββfld)
β§ π₯ β π΄) β (β β© β© ran π) β (πβπ₯)) |
117 | 116 | ssdifd 4105 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π:π΄βΆ(TopOpenββfld)
β§ π₯ β π΄) β ((β β© β© ran π) β {πΆ}) β ((πβπ₯) β {πΆ})) |
118 | | sslin 4199 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β β© β© ran π) β {πΆ}) β ((πβπ₯) β {πΆ}) β (π΅ β© ((β β© β© ran π) β {πΆ})) β (π΅ β© ((πβπ₯) β {πΆ}))) |
119 | | imass2 6059 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΅ β© ((β β© β© ran π) β {πΆ})) β (π΅ β© ((πβπ₯) β {πΆ})) β (πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) β (πΉ β (π΅ β© ((πβπ₯) β {πΆ})))) |
120 | 117, 118,
119 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ ((π:π΄βΆ(TopOpenββfld)
β§ π₯ β π΄) β (πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) β (πΉ β (π΅ β© ((πβπ₯) β {πΆ})))) |
121 | | indifcom 4237 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πβπ₯) β© (π΅ β {πΆ})) = (π΅ β© ((πβπ₯) β {πΆ})) |
122 | 121 | imaeq2i 6016 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) = ((πΉ βΎ π΅) β (π΅ β© ((πβπ₯) β {πΆ}))) |
123 | | inss1 4193 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π΅ β© ((πβπ₯) β {πΆ})) β π΅ |
124 | | resima2 5977 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΅ β© ((πβπ₯) β {πΆ})) β π΅ β ((πΉ βΎ π΅) β (π΅ β© ((πβπ₯) β {πΆ}))) = (πΉ β (π΅ β© ((πβπ₯) β {πΆ})))) |
125 | 123, 124 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ βΎ π΅) β (π΅ β© ((πβπ₯) β {πΆ}))) = (πΉ β (π΅ β© ((πβπ₯) β {πΆ}))) |
126 | 122, 125 | eqtri 2765 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) = (πΉ β (π΅ β© ((πβπ₯) β {πΆ}))) |
127 | 120, 126 | sseqtrrdi 4000 |
. . . . . . . . . . . . . . . . 17
β’ ((π:π΄βΆ(TopOpenββfld)
β§ π₯ β π΄) β (πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) β ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ})))) |
128 | | sstr2 3956 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) β ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β (((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’ β (πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) β π’)) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π:π΄βΆ(TopOpenββfld)
β§ π₯ β π΄) β (((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’ β (πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) β π’)) |
130 | 129 | adantld 492 |
. . . . . . . . . . . . . . 15
β’ ((π:π΄βΆ(TopOpenββfld)
β§ π₯ β π΄) β ((πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’) β (πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) β π’)) |
131 | 130 | ralimdva 3165 |
. . . . . . . . . . . . . 14
β’ (π:π΄βΆ(TopOpenββfld)
β (βπ₯ β
π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’) β βπ₯ β π΄ (πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) β π’)) |
132 | 131 | imp 408 |
. . . . . . . . . . . . 13
β’ ((π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’)) β βπ₯ β π΄ (πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) β π’) |
133 | 132 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β βπ₯ β π΄ (πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) β π’) |
134 | | iunss 5010 |
. . . . . . . . . . . 12
β’ (βͺ π₯ β π΄ (πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) β π’ β βπ₯ β π΄ (πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) β π’) |
135 | 133, 134 | sylibr 233 |
. . . . . . . . . . 11
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β βͺ
π₯ β π΄ (πΉ β (π΅ β© ((β β© β© ran π) β {πΆ}))) β π’) |
136 | 110, 135 | eqsstrid 3997 |
. . . . . . . . . 10
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β (πΉ β ((β β© β© ran π) β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) β π’) |
137 | | eleq2 2827 |
. . . . . . . . . . . 12
β’ (π£ = (β β© β© ran π) β (πΆ β π£ β πΆ β (β β© β© ran π))) |
138 | | ineq1 4170 |
. . . . . . . . . . . . . 14
β’ (π£ = (β β© β© ran π) β (π£ β© (βͺ
π₯ β π΄ π΅ β {πΆ})) = ((β β© β© ran π) β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) |
139 | 138 | imaeq2d 6018 |
. . . . . . . . . . . . 13
β’ (π£ = (β β© β© ran π) β (πΉ β (π£ β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) = (πΉ β ((β β© β© ran π) β© (βͺ
π₯ β π΄ π΅ β {πΆ})))) |
140 | 139 | sseq1d 3980 |
. . . . . . . . . . . 12
β’ (π£ = (β β© β© ran π) β ((πΉ β (π£ β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) β π’ β (πΉ β ((β β© β© ran π) β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) β π’)) |
141 | 137, 140 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π£ = (β β© β© ran π) β ((πΆ β π£ β§ (πΉ β (π£ β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) β π’) β (πΆ β (β β© β© ran π) β§ (πΉ β ((β β© β© ran π) β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) β π’))) |
142 | 141 | rspcev 3584 |
. . . . . . . . . 10
β’
(((β β© β© ran π) β
(TopOpenββfld) β§ (πΆ β (β β© β© ran π) β§ (πΉ β ((β β© β© ran π) β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) β π’)) β βπ£ β
(TopOpenββfld)(πΆ β π£ β§ (πΉ β (π£ β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) β π’)) |
143 | 93, 104, 136, 142 | syl12anc 836 |
. . . . . . . . 9
β’ ((((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β§ (π:π΄βΆ(TopOpenββfld)
β§ βπ₯ β π΄ (πΆ β (πβπ₯) β§ ((πΉ βΎ π΅) β ((πβπ₯) β© (π΅ β {πΆ}))) β π’))) β βπ£ β
(TopOpenββfld)(πΆ β π£ β§ (πΉ β (π£ β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) β π’)) |
144 | 80, 143 | exlimddv 1939 |
. . . . . . . 8
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ (π’ β (TopOpenββfld)
β§ π¦ β π’)) β βπ£ β
(TopOpenββfld)(πΆ β π£ β§ (πΉ β (π£ β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) β π’)) |
145 | 144 | expr 458 |
. . . . . . 7
β’ (((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β§ π’ β
(TopOpenββfld)) β (π¦ β π’ β βπ£ β
(TopOpenββfld)(πΆ β π£ β§ (πΉ β (π£ β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) β π’))) |
146 | 145 | ralrimiva 3144 |
. . . . . 6
β’ ((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β βπ’ β
(TopOpenββfld)(π¦ β π’ β βπ£ β
(TopOpenββfld)(πΆ β π£ β§ (πΉ β (π£ β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) β π’))) |
147 | 26 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β πΉ:βͺ π₯ β π΄ π΅βΆβ) |
148 | | iunss 5010 |
. . . . . . . . 9
β’ (βͺ π₯ β π΄ π΅ β β β βπ₯ β π΄ π΅ β β) |
149 | 35, 148 | sylibr 233 |
. . . . . . . 8
β’ (π β βͺ π₯ β π΄ π΅ β β) |
150 | 149 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β βͺ π₯ β π΄ π΅ β β) |
151 | 147, 150,
94, 44 | ellimc2 25257 |
. . . . . 6
β’ ((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β (π¦ β (πΉ limβ πΆ) β (π¦ β β β§ βπ’ β
(TopOpenββfld)(π¦ β π’ β βπ£ β
(TopOpenββfld)(πΆ β π£ β§ (πΉ β (π£ β© (βͺ
π₯ β π΄ π΅ β {πΆ}))) β π’))))) |
152 | 9, 146, 151 | mpbir2and 712 |
. . . . 5
β’ ((π β§ (π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ))) β π¦ β (πΉ limβ πΆ)) |
153 | 152 | ex 414 |
. . . 4
β’ (π β ((π¦ β β β§ βπ₯ β π΄ π¦ β ((πΉ βΎ π΅) limβ πΆ)) β π¦ β (πΉ limβ πΆ))) |
154 | 8, 153 | biimtrid 241 |
. . 3
β’ (π β (π¦ β (β β© β© π₯ β π΄ ((πΉ βΎ π΅) limβ πΆ)) β π¦ β (πΉ limβ πΆ))) |
155 | 154 | ssrdv 3955 |
. 2
β’ (π β (β β© β© π₯ β π΄ ((πΉ βΎ π΅) limβ πΆ)) β (πΉ limβ πΆ)) |
156 | 7, 155 | eqssd 3966 |
1
β’ (π β (πΉ limβ πΆ) = (β β© β© π₯ β π΄ ((πΉ βΎ π΅) limβ πΆ))) |