Step | Hyp | Ref
| Expression |
1 | | cncff 24401 |
. . 3
β’ (πΉ β (π΄βcnββ) β πΉ:π΄βΆβ) |
2 | | mblss 25040 |
. . 3
β’ (π΄ β dom vol β π΄ β
β) |
3 | | cnex 11188 |
. . . 4
β’ β
β V |
4 | | reex 11198 |
. . . 4
β’ β
β V |
5 | | elpm2r 8836 |
. . . 4
β’
(((β β V β§ β β V) β§ (πΉ:π΄βΆβ β§ π΄ β β)) β πΉ β (β βpm
β)) |
6 | 3, 4, 5 | mpanl12 701 |
. . 3
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β πΉ β (β βpm
β)) |
7 | 1, 2, 6 | syl2anr 598 |
. 2
β’ ((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β πΉ β (β βpm
β)) |
8 | | simpll 766 |
. . . . 5
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β π΄ β dom vol) |
9 | | simplr 768 |
. . . . . . . 8
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β πΉ β (π΄βcnββ)) |
10 | | recncf 24410 |
. . . . . . . . 9
β’ β
β (ββcnββ) |
11 | 10 | a1i 11 |
. . . . . . . 8
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β β β
(ββcnββ)) |
12 | 9, 11 | cncfco 24415 |
. . . . . . 7
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β (β β πΉ) β (π΄βcnββ)) |
13 | 2 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β π΄ β β) |
14 | | ax-resscn 11164 |
. . . . . . . . . 10
β’ β
β β |
15 | 13, 14 | sstrdi 3994 |
. . . . . . . . 9
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β π΄ β β) |
16 | | eqid 2733 |
. . . . . . . . . 10
β’
(TopOpenββfld) =
(TopOpenββfld) |
17 | | eqid 2733 |
. . . . . . . . . 10
β’
((TopOpenββfld) βΎt π΄) =
((TopOpenββfld) βΎt π΄) |
18 | 16 | tgioo2 24311 |
. . . . . . . . . 10
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
19 | 16, 17, 18 | cncfcn 24418 |
. . . . . . . . 9
β’ ((π΄ β β β§ β
β β) β (π΄βcnββ) =
(((TopOpenββfld) βΎt π΄) Cn (topGenβran
(,)))) |
20 | 15, 14, 19 | sylancl 587 |
. . . . . . . 8
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β (π΄βcnββ) =
(((TopOpenββfld) βΎt π΄) Cn (topGenβran
(,)))) |
21 | | eqid 2733 |
. . . . . . . . . . 11
β’
(topGenβran (,)) = (topGenβran (,)) |
22 | 16, 21 | rerest 24312 |
. . . . . . . . . 10
β’ (π΄ β β β
((TopOpenββfld) βΎt π΄) = ((topGenβran (,))
βΎt π΄)) |
23 | 13, 22 | syl 17 |
. . . . . . . . 9
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β
((TopOpenββfld) βΎt π΄) = ((topGenβran (,))
βΎt π΄)) |
24 | 23 | oveq1d 7421 |
. . . . . . . 8
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β
(((TopOpenββfld) βΎt π΄) Cn (topGenβran (,))) =
(((topGenβran (,)) βΎt π΄) Cn (topGenβran
(,)))) |
25 | 20, 24 | eqtrd 2773 |
. . . . . . 7
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β (π΄βcnββ) = (((topGenβran (,))
βΎt π΄) Cn
(topGenβran (,)))) |
26 | 12, 25 | eleqtrd 2836 |
. . . . . 6
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β (β β πΉ) β (((topGenβran
(,)) βΎt π΄)
Cn (topGenβran (,)))) |
27 | | retopbas 24269 |
. . . . . . . 8
β’ ran (,)
β TopBases |
28 | | bastg 22461 |
. . . . . . . 8
β’ (ran (,)
β TopBases β ran (,) β (topGenβran (,))) |
29 | 27, 28 | ax-mp 5 |
. . . . . . 7
β’ ran (,)
β (topGenβran (,)) |
30 | | simpr 486 |
. . . . . . 7
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β π₯ β ran (,)) |
31 | 29, 30 | sselid 3980 |
. . . . . 6
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β π₯ β (topGenβran
(,))) |
32 | | cnima 22761 |
. . . . . 6
β’ (((β
β πΉ) β
(((topGenβran (,)) βΎt π΄) Cn (topGenβran (,))) β§ π₯ β (topGenβran (,)))
β (β‘(β β πΉ) β π₯) β ((topGenβran (,))
βΎt π΄)) |
33 | 26, 31, 32 | syl2anc 585 |
. . . . 5
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β (β‘(β β πΉ) β π₯) β ((topGenβran (,))
βΎt π΄)) |
34 | | eqid 2733 |
. . . . . 6
β’
((topGenβran (,)) βΎt π΄) = ((topGenβran (,))
βΎt π΄) |
35 | 34 | subopnmbl 25113 |
. . . . 5
β’ ((π΄ β dom vol β§ (β‘(β β πΉ) β π₯) β ((topGenβran (,))
βΎt π΄))
β (β‘(β β πΉ) β π₯) β dom vol) |
36 | 8, 33, 35 | syl2anc 585 |
. . . 4
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β (β‘(β β πΉ) β π₯) β dom vol) |
37 | | imcncf 24411 |
. . . . . . . . 9
β’ β
β (ββcnββ) |
38 | 37 | a1i 11 |
. . . . . . . 8
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β β β
(ββcnββ)) |
39 | 9, 38 | cncfco 24415 |
. . . . . . 7
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β (β β
πΉ) β (π΄βcnββ)) |
40 | 39, 25 | eleqtrd 2836 |
. . . . . 6
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β (β β
πΉ) β
(((topGenβran (,)) βΎt π΄) Cn (topGenβran
(,)))) |
41 | | cnima 22761 |
. . . . . 6
β’
(((β β πΉ) β (((topGenβran (,))
βΎt π΄) Cn
(topGenβran (,))) β§ π₯ β (topGenβran (,))) β (β‘(β β πΉ) β π₯) β ((topGenβran (,))
βΎt π΄)) |
42 | 40, 31, 41 | syl2anc 585 |
. . . . 5
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β (β‘(β β πΉ) β π₯) β ((topGenβran (,))
βΎt π΄)) |
43 | 34 | subopnmbl 25113 |
. . . . 5
β’ ((π΄ β dom vol β§ (β‘(β β πΉ) β π₯) β ((topGenβran (,))
βΎt π΄))
β (β‘(β β πΉ) β π₯) β dom vol) |
44 | 8, 42, 43 | syl2anc 585 |
. . . 4
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β (β‘(β β πΉ) β π₯) β dom vol) |
45 | 36, 44 | jca 513 |
. . 3
β’ (((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β§ π₯ β ran (,)) β ((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol)) |
46 | 45 | ralrimiva 3147 |
. 2
β’ ((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β βπ₯ β ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol)) |
47 | | ismbf1 25133 |
. 2
β’ (πΉ β MblFn β (πΉ β (β
βpm β) β§ βπ₯ β ran (,)((β‘(β β πΉ) β π₯) β dom vol β§ (β‘(β β πΉ) β π₯) β dom vol))) |
48 | 7, 46, 47 | sylanbrc 584 |
1
β’ ((π΄ β dom vol β§ πΉ β (π΄βcnββ)) β πΉ β MblFn) |