Step | Hyp | Ref
| Expression |
1 | | dvf 25423 |
. . . . 5
β’ (β
D πΊ):dom (β D πΊ)βΆβ |
2 | 1 | a1i 11 |
. . . 4
β’ (π β (β D πΊ):dom (β D πΊ)βΆβ) |
3 | 2 | ffund 6721 |
. . 3
β’ (π β Fun (β D πΊ)) |
4 | | ax-resscn 11166 |
. . . . . . 7
β’ β
β β |
5 | 4 | a1i 11 |
. . . . . 6
β’ (π β β β
β) |
6 | | ftc1cn.g |
. . . . . . 7
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) |
7 | | ftc1cn.a |
. . . . . . 7
β’ (π β π΄ β β) |
8 | | ftc1cn.b |
. . . . . . 7
β’ (π β π΅ β β) |
9 | | ftc1cn.le |
. . . . . . 7
β’ (π β π΄ β€ π΅) |
10 | | ssidd 4005 |
. . . . . . 7
β’ (π β (π΄(,)π΅) β (π΄(,)π΅)) |
11 | | ioossre 13384 |
. . . . . . . 8
β’ (π΄(,)π΅) β β |
12 | 11 | a1i 11 |
. . . . . . 7
β’ (π β (π΄(,)π΅) β β) |
13 | | ftc1cn.i |
. . . . . . 7
β’ (π β πΉ β
πΏ1) |
14 | | ftc1cn.f |
. . . . . . . 8
β’ (π β πΉ β ((π΄(,)π΅)βcnββ)) |
15 | | cncff 24408 |
. . . . . . . 8
β’ (πΉ β ((π΄(,)π΅)βcnββ) β πΉ:(π΄(,)π΅)βΆβ) |
16 | 14, 15 | syl 17 |
. . . . . . 7
β’ (π β πΉ:(π΄(,)π΅)βΆβ) |
17 | 6, 7, 8, 9, 10, 12, 13, 16 | ftc1lem2 25552 |
. . . . . 6
β’ (π β πΊ:(π΄[,]π΅)βΆβ) |
18 | | iccssre 13405 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
19 | 7, 8, 18 | syl2anc 584 |
. . . . . 6
β’ (π β (π΄[,]π΅) β β) |
20 | | eqid 2732 |
. . . . . . 7
β’
(TopOpenββfld) =
(TopOpenββfld) |
21 | 20 | tgioo2 24318 |
. . . . . 6
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
22 | 5, 17, 19, 21, 20 | dvbssntr 25416 |
. . . . 5
β’ (π β dom (β D πΊ) β
((intβ(topGenβran (,)))β(π΄[,]π΅))) |
23 | | iccntr 24336 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β) β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
24 | 7, 8, 23 | syl2anc 584 |
. . . . 5
β’ (π β
((intβ(topGenβran (,)))β(π΄[,]π΅)) = (π΄(,)π΅)) |
25 | 22, 24 | sseqtrd 4022 |
. . . 4
β’ (π β dom (β D πΊ) β (π΄(,)π΅)) |
26 | 7 | adantr 481 |
. . . . . 6
β’ ((π β§ π¦ β (π΄(,)π΅)) β π΄ β β) |
27 | 8 | adantr 481 |
. . . . . 6
β’ ((π β§ π¦ β (π΄(,)π΅)) β π΅ β β) |
28 | 9 | adantr 481 |
. . . . . 6
β’ ((π β§ π¦ β (π΄(,)π΅)) β π΄ β€ π΅) |
29 | | ssidd 4005 |
. . . . . 6
β’ ((π β§ π¦ β (π΄(,)π΅)) β (π΄(,)π΅) β (π΄(,)π΅)) |
30 | 11 | a1i 11 |
. . . . . 6
β’ ((π β§ π¦ β (π΄(,)π΅)) β (π΄(,)π΅) β β) |
31 | 13 | adantr 481 |
. . . . . 6
β’ ((π β§ π¦ β (π΄(,)π΅)) β πΉ β
πΏ1) |
32 | | simpr 485 |
. . . . . 6
β’ ((π β§ π¦ β (π΄(,)π΅)) β π¦ β (π΄(,)π΅)) |
33 | 11, 4 | sstri 3991 |
. . . . . . . . . 10
β’ (π΄(,)π΅) β β |
34 | | ssid 4004 |
. . . . . . . . . 10
β’ β
β β |
35 | | eqid 2732 |
. . . . . . . . . . 11
β’
((TopOpenββfld) βΎt (π΄(,)π΅)) = ((TopOpenββfld)
βΎt (π΄(,)π΅)) |
36 | 20 | cnfldtopon 24298 |
. . . . . . . . . . . 12
β’
(TopOpenββfld) β
(TopOnββ) |
37 | 36 | toponrestid 22422 |
. . . . . . . . . . 11
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
38 | 20, 35, 37 | cncfcn 24425 |
. . . . . . . . . 10
β’ (((π΄(,)π΅) β β β§ β β
β) β ((π΄(,)π΅)βcnββ) =
(((TopOpenββfld) βΎt (π΄(,)π΅)) Cn
(TopOpenββfld))) |
39 | 33, 34, 38 | mp2an 690 |
. . . . . . . . 9
β’ ((π΄(,)π΅)βcnββ) =
(((TopOpenββfld) βΎt (π΄(,)π΅)) Cn
(TopOpenββfld)) |
40 | 14, 39 | eleqtrdi 2843 |
. . . . . . . 8
β’ (π β πΉ β
(((TopOpenββfld) βΎt (π΄(,)π΅)) Cn
(TopOpenββfld))) |
41 | 40 | adantr 481 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄(,)π΅)) β πΉ β
(((TopOpenββfld) βΎt (π΄(,)π΅)) Cn
(TopOpenββfld))) |
42 | 33 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (π΄(,)π΅) β β) |
43 | | resttopon 22664 |
. . . . . . . . . . 11
β’
(((TopOpenββfld) β (TopOnββ)
β§ (π΄(,)π΅) β β) β
((TopOpenββfld) βΎt (π΄(,)π΅)) β (TopOnβ(π΄(,)π΅))) |
44 | 36, 42, 43 | sylancr 587 |
. . . . . . . . . 10
β’ (π β
((TopOpenββfld) βΎt (π΄(,)π΅)) β (TopOnβ(π΄(,)π΅))) |
45 | | toponuni 22415 |
. . . . . . . . . 10
β’
(((TopOpenββfld) βΎt (π΄(,)π΅)) β (TopOnβ(π΄(,)π΅)) β (π΄(,)π΅) = βͺ
((TopOpenββfld) βΎt (π΄(,)π΅))) |
46 | 44, 45 | syl 17 |
. . . . . . . . 9
β’ (π β (π΄(,)π΅) = βͺ
((TopOpenββfld) βΎt (π΄(,)π΅))) |
47 | 46 | eleq2d 2819 |
. . . . . . . 8
β’ (π β (π¦ β (π΄(,)π΅) β π¦ β βͺ
((TopOpenββfld) βΎt (π΄(,)π΅)))) |
48 | 47 | biimpa 477 |
. . . . . . 7
β’ ((π β§ π¦ β (π΄(,)π΅)) β π¦ β βͺ
((TopOpenββfld) βΎt (π΄(,)π΅))) |
49 | | eqid 2732 |
. . . . . . . 8
β’ βͺ ((TopOpenββfld)
βΎt (π΄(,)π΅)) = βͺ
((TopOpenββfld) βΎt (π΄(,)π΅)) |
50 | 49 | cncnpi 22781 |
. . . . . . 7
β’ ((πΉ β
(((TopOpenββfld) βΎt (π΄(,)π΅)) Cn (TopOpenββfld))
β§ π¦ β βͺ ((TopOpenββfld)
βΎt (π΄(,)π΅))) β πΉ β
((((TopOpenββfld) βΎt (π΄(,)π΅)) CnP
(TopOpenββfld))βπ¦)) |
51 | 41, 48, 50 | syl2anc 584 |
. . . . . 6
β’ ((π β§ π¦ β (π΄(,)π΅)) β πΉ β
((((TopOpenββfld) βΎt (π΄(,)π΅)) CnP
(TopOpenββfld))βπ¦)) |
52 | 6, 26, 27, 28, 29, 30, 31, 32, 51, 21, 35, 20 | ftc1 25558 |
. . . . 5
β’ ((π β§ π¦ β (π΄(,)π΅)) β π¦(β D πΊ)(πΉβπ¦)) |
53 | | vex 3478 |
. . . . . 6
β’ π¦ β V |
54 | | fvex 6904 |
. . . . . 6
β’ (πΉβπ¦) β V |
55 | 53, 54 | breldm 5908 |
. . . . 5
β’ (π¦(β D πΊ)(πΉβπ¦) β π¦ β dom (β D πΊ)) |
56 | 52, 55 | syl 17 |
. . . 4
β’ ((π β§ π¦ β (π΄(,)π΅)) β π¦ β dom (β D πΊ)) |
57 | 25, 56 | eqelssd 4003 |
. . 3
β’ (π β dom (β D πΊ) = (π΄(,)π΅)) |
58 | | df-fn 6546 |
. . 3
β’ ((β
D πΊ) Fn (π΄(,)π΅) β (Fun (β D πΊ) β§ dom (β D πΊ) = (π΄(,)π΅))) |
59 | 3, 57, 58 | sylanbrc 583 |
. 2
β’ (π β (β D πΊ) Fn (π΄(,)π΅)) |
60 | 16 | ffnd 6718 |
. 2
β’ (π β πΉ Fn (π΄(,)π΅)) |
61 | 3 | adantr 481 |
. . 3
β’ ((π β§ π¦ β (π΄(,)π΅)) β Fun (β D πΊ)) |
62 | | funbrfv 6942 |
. . 3
β’ (Fun
(β D πΊ) β (π¦(β D πΊ)(πΉβπ¦) β ((β D πΊ)βπ¦) = (πΉβπ¦))) |
63 | 61, 52, 62 | sylc 65 |
. 2
β’ ((π β§ π¦ β (π΄(,)π΅)) β ((β D πΊ)βπ¦) = (πΉβπ¦)) |
64 | 59, 60, 63 | eqfnfvd 7035 |
1
β’ (π β (β D πΊ) = πΉ) |