Step | Hyp | Ref
| Expression |
1 | | n0 4311 |
. 2
β’ ((πβπ) β β
β βπ₯ π₯ β (πβπ)) |
2 | | simpl2 1193 |
. . . . . 6
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β π β π½) |
3 | | simpl1 1192 |
. . . . . . . . . . . 12
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β πΉ β (πΆ CovMap π½)) |
4 | | cvmtop1 33894 |
. . . . . . . . . . . 12
β’ (πΉ β (πΆ CovMap π½) β πΆ β Top) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β πΆ β Top) |
6 | 5 | adantr 482 |
. . . . . . . . . 10
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π¦ β π₯) β πΆ β Top) |
7 | | cvmcov.1 |
. . . . . . . . . . . . 13
β’ π = (π β π½ β¦ {π β (π« πΆ β {β
}) β£ (βͺ π =
(β‘πΉ β π) β§ βπ’ β π (βπ£ β (π β {π’})(π’ β© π£) = β
β§ (πΉ βΎ π’) β ((πΆ βΎt π’)Homeo(π½ βΎt π))))}) |
8 | 7 | cvmsss 33901 |
. . . . . . . . . . . 12
β’ (π₯ β (πβπ) β π₯ β πΆ) |
9 | 8 | adantl 483 |
. . . . . . . . . . 11
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β π₯ β πΆ) |
10 | 9 | sselda 3949 |
. . . . . . . . . 10
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π¦ β π₯) β π¦ β πΆ) |
11 | | cvmcn 33896 |
. . . . . . . . . . . . 13
β’ (πΉ β (πΆ CovMap π½) β πΉ β (πΆ Cn π½)) |
12 | 3, 11 | syl 17 |
. . . . . . . . . . . 12
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β πΉ β (πΆ Cn π½)) |
13 | | cnima 22632 |
. . . . . . . . . . . 12
β’ ((πΉ β (πΆ Cn π½) β§ π β π½) β (β‘πΉ β π) β πΆ) |
14 | 12, 2, 13 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β (β‘πΉ β π) β πΆ) |
15 | 14 | adantr 482 |
. . . . . . . . . 10
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π¦ β π₯) β (β‘πΉ β π) β πΆ) |
16 | | inopn 22264 |
. . . . . . . . . 10
β’ ((πΆ β Top β§ π¦ β πΆ β§ (β‘πΉ β π) β πΆ) β (π¦ β© (β‘πΉ β π)) β πΆ) |
17 | 6, 10, 15, 16 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π¦ β π₯) β (π¦ β© (β‘πΉ β π)) β πΆ) |
18 | 17 | fmpttd 7068 |
. . . . . . . 8
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))):π₯βΆπΆ) |
19 | 18 | frnd 6681 |
. . . . . . 7
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β πΆ) |
20 | 7 | cvmsn0 33902 |
. . . . . . . . 9
β’ (π₯ β (πβπ) β π₯ β β
) |
21 | 20 | adantl 483 |
. . . . . . . 8
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β π₯ β β
) |
22 | | dmmptg 6199 |
. . . . . . . . . . . 12
β’
(βπ¦ β
π₯ (π¦ β© (β‘πΉ β π)) β V β dom (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) = π₯) |
23 | | inex1g 5281 |
. . . . . . . . . . . 12
β’ (π¦ β π₯ β (π¦ β© (β‘πΉ β π)) β V) |
24 | 22, 23 | mprg 3071 |
. . . . . . . . . . 11
β’ dom
(π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) = π₯ |
25 | 24 | eqeq1i 2742 |
. . . . . . . . . 10
β’ (dom
(π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) = β
β π₯ = β
) |
26 | | dm0rn0 5885 |
. . . . . . . . . 10
β’ (dom
(π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) = β
β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) = β
) |
27 | 25, 26 | bitr3i 277 |
. . . . . . . . 9
β’ (π₯ = β
β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) = β
) |
28 | 27 | necon3bii 2997 |
. . . . . . . 8
β’ (π₯ β β
β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β β
) |
29 | 21, 28 | sylib 217 |
. . . . . . 7
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β β
) |
30 | 19, 29 | jca 513 |
. . . . . 6
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β πΆ β§ ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β β
)) |
31 | | inss2 4194 |
. . . . . . . . . . . 12
β’ (π¦ β© (β‘πΉ β π)) β (β‘πΉ β π) |
32 | | elpw2g 5306 |
. . . . . . . . . . . . 13
β’ ((β‘πΉ β π) β πΆ β ((π¦ β© (β‘πΉ β π)) β π« (β‘πΉ β π) β (π¦ β© (β‘πΉ β π)) β (β‘πΉ β π))) |
33 | 15, 32 | syl 17 |
. . . . . . . . . . . 12
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π¦ β π₯) β ((π¦ β© (β‘πΉ β π)) β π« (β‘πΉ β π) β (π¦ β© (β‘πΉ β π)) β (β‘πΉ β π))) |
34 | 31, 33 | mpbiri 258 |
. . . . . . . . . . 11
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π¦ β π₯) β (π¦ β© (β‘πΉ β π)) β π« (β‘πΉ β π)) |
35 | 34 | fmpttd 7068 |
. . . . . . . . . 10
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))):π₯βΆπ« (β‘πΉ β π)) |
36 | 35 | frnd 6681 |
. . . . . . . . 9
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β π« (β‘πΉ β π)) |
37 | | sspwuni 5065 |
. . . . . . . . 9
β’ (ran
(π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β π« (β‘πΉ β π) β βͺ ran
(π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β (β‘πΉ β π)) |
38 | 36, 37 | sylib 217 |
. . . . . . . 8
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β βͺ ran
(π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β (β‘πΉ β π)) |
39 | | simpl3 1194 |
. . . . . . . . . . . 12
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β π β π) |
40 | | imass2 6059 |
. . . . . . . . . . . 12
β’ (π β π β (β‘πΉ β π) β (β‘πΉ β π)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β (β‘πΉ β π) β (β‘πΉ β π)) |
42 | 7 | cvmsuni 33903 |
. . . . . . . . . . . 12
β’ (π₯ β (πβπ) β βͺ π₯ = (β‘πΉ β π)) |
43 | 42 | adantl 483 |
. . . . . . . . . . 11
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β βͺ π₯ = (β‘πΉ β π)) |
44 | 41, 43 | sseqtrrd 3990 |
. . . . . . . . . 10
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β (β‘πΉ β π) β βͺ π₯) |
45 | 44 | sselda 3949 |
. . . . . . . . 9
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π§ β (β‘πΉ β π)) β π§ β βͺ π₯) |
46 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ (π‘ β© (β‘πΉ β π)) = (π‘ β© (β‘πΉ β π)) |
47 | | ineq1 4170 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π‘ β (π¦ β© (β‘πΉ β π)) = (π‘ β© (β‘πΉ β π))) |
48 | 47 | rspceeqv 3600 |
. . . . . . . . . . . . . . 15
β’ ((π‘ β π₯ β§ (π‘ β© (β‘πΉ β π)) = (π‘ β© (β‘πΉ β π))) β βπ¦ β π₯ (π‘ β© (β‘πΉ β π)) = (π¦ β© (β‘πΉ β π))) |
49 | 46, 48 | mpan2 690 |
. . . . . . . . . . . . . 14
β’ (π‘ β π₯ β βπ¦ β π₯ (π‘ β© (β‘πΉ β π)) = (π¦ β© (β‘πΉ β π))) |
50 | 49 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’
(((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π§ β (β‘πΉ β π)) β§ (π‘ β π₯ β§ π§ β π‘)) β βπ¦ β π₯ (π‘ β© (β‘πΉ β π)) = (π¦ β© (β‘πΉ β π))) |
51 | | vex 3452 |
. . . . . . . . . . . . . . 15
β’ π‘ β V |
52 | 51 | inex1 5279 |
. . . . . . . . . . . . . 14
β’ (π‘ β© (β‘πΉ β π)) β V |
53 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) = (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) |
54 | 53 | elrnmpt 5916 |
. . . . . . . . . . . . . 14
β’ ((π‘ β© (β‘πΉ β π)) β V β ((π‘ β© (β‘πΉ β π)) β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β βπ¦ β π₯ (π‘ β© (β‘πΉ β π)) = (π¦ β© (β‘πΉ β π)))) |
55 | 52, 54 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ ((π‘ β© (β‘πΉ β π)) β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β βπ¦ β π₯ (π‘ β© (β‘πΉ β π)) = (π¦ β© (β‘πΉ β π))) |
56 | 50, 55 | sylibr 233 |
. . . . . . . . . . . 12
β’
(((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π§ β (β‘πΉ β π)) β§ (π‘ β π₯ β§ π§ β π‘)) β (π‘ β© (β‘πΉ β π)) β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π)))) |
57 | | simprr 772 |
. . . . . . . . . . . . 13
β’
(((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π§ β (β‘πΉ β π)) β§ (π‘ β π₯ β§ π§ β π‘)) β π§ β π‘) |
58 | | simplr 768 |
. . . . . . . . . . . . 13
β’
(((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π§ β (β‘πΉ β π)) β§ (π‘ β π₯ β§ π§ β π‘)) β π§ β (β‘πΉ β π)) |
59 | 57, 58 | elind 4159 |
. . . . . . . . . . . 12
β’
(((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π§ β (β‘πΉ β π)) β§ (π‘ β π₯ β§ π§ β π‘)) β π§ β (π‘ β© (β‘πΉ β π))) |
60 | | eleq2 2827 |
. . . . . . . . . . . . 13
β’ (π€ = (π‘ β© (β‘πΉ β π)) β (π§ β π€ β π§ β (π‘ β© (β‘πΉ β π)))) |
61 | 60 | rspcev 3584 |
. . . . . . . . . . . 12
β’ (((π‘ β© (β‘πΉ β π)) β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β§ π§ β (π‘ β© (β‘πΉ β π))) β βπ€ β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π)))π§ β π€) |
62 | 56, 59, 61 | syl2anc 585 |
. . . . . . . . . . 11
β’
(((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π§ β (β‘πΉ β π)) β§ (π‘ β π₯ β§ π§ β π‘)) β βπ€ β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π)))π§ β π€) |
63 | 62 | rexlimdvaa 3154 |
. . . . . . . . . 10
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π§ β (β‘πΉ β π)) β (βπ‘ β π₯ π§ β π‘ β βπ€ β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π)))π§ β π€)) |
64 | | eluni2 4874 |
. . . . . . . . . 10
β’ (π§ β βͺ π₯
β βπ‘ β
π₯ π§ β π‘) |
65 | | eluni2 4874 |
. . . . . . . . . 10
β’ (π§ β βͺ ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β βπ€ β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π)))π§ β π€) |
66 | 63, 64, 65 | 3imtr4g 296 |
. . . . . . . . 9
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π§ β (β‘πΉ β π)) β (π§ β βͺ π₯ β π§ β βͺ ran
(π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))))) |
67 | 45, 66 | mpd 15 |
. . . . . . . 8
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π§ β (β‘πΉ β π)) β π§ β βͺ ran
(π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π)))) |
68 | 38, 67 | eqelssd 3970 |
. . . . . . 7
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β βͺ ran
(π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) = (β‘πΉ β π)) |
69 | | eldifsn 4752 |
. . . . . . . . . . . 12
β’ (π§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {(π‘ β© (β‘πΉ β π))}) β (π§ β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β§ π§ β (π‘ β© (β‘πΉ β π)))) |
70 | | vex 3452 |
. . . . . . . . . . . . . . 15
β’ π§ β V |
71 | 53 | elrnmpt 5916 |
. . . . . . . . . . . . . . 15
β’ (π§ β V β (π§ β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β βπ¦ β π₯ π§ = (π¦ β© (β‘πΉ β π)))) |
72 | 70, 71 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ (π§ β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β βπ¦ β π₯ π§ = (π¦ β© (β‘πΉ β π))) |
73 | 47 | equcoms 2024 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ = π¦ β (π¦ β© (β‘πΉ β π)) = (π‘ β© (β‘πΉ β π))) |
74 | 73 | necon3ai 2969 |
. . . . . . . . . . . . . . . . 17
β’ ((π¦ β© (β‘πΉ β π)) β (π‘ β© (β‘πΉ β π)) β Β¬ π‘ = π¦) |
75 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β§ π¦ β π₯) β π₯ β (πβπ)) |
76 | | simplr 768 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β§ π¦ β π₯) β π‘ β π₯) |
77 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β§ π¦ β π₯) β π¦ β π₯) |
78 | 7 | cvmsdisj 33904 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β (πβπ) β§ π‘ β π₯ β§ π¦ β π₯) β (π‘ = π¦ β¨ (π‘ β© π¦) = β
)) |
79 | 75, 76, 77, 78 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’
(((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β§ π¦ β π₯) β (π‘ = π¦ β¨ (π‘ β© π¦) = β
)) |
80 | 79 | ord 863 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β§ π¦ β π₯) β (Β¬ π‘ = π¦ β (π‘ β© π¦) = β
)) |
81 | | inss1 4193 |
. . . . . . . . . . . . . . . . . 18
β’ ((π‘ β© π¦) β© (β‘πΉ β π)) β (π‘ β© π¦) |
82 | | sseq0 4364 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π‘ β© π¦) β© (β‘πΉ β π)) β (π‘ β© π¦) β§ (π‘ β© π¦) = β
) β ((π‘ β© π¦) β© (β‘πΉ β π)) = β
) |
83 | 81, 82 | mpan 689 |
. . . . . . . . . . . . . . . . 17
β’ ((π‘ β© π¦) = β
β ((π‘ β© π¦) β© (β‘πΉ β π)) = β
) |
84 | 74, 80, 83 | syl56 36 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β§ π¦ β π₯) β ((π¦ β© (β‘πΉ β π)) β (π‘ β© (β‘πΉ β π)) β ((π‘ β© π¦) β© (β‘πΉ β π)) = β
)) |
85 | | neeq1 3007 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (π¦ β© (β‘πΉ β π)) β (π§ β (π‘ β© (β‘πΉ β π)) β (π¦ β© (β‘πΉ β π)) β (π‘ β© (β‘πΉ β π)))) |
86 | | ineq2 4171 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ = (π¦ β© (β‘πΉ β π)) β ((π‘ β© (β‘πΉ β π)) β© π§) = ((π‘ β© (β‘πΉ β π)) β© (π¦ β© (β‘πΉ β π)))) |
87 | | inindir 4192 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π‘ β© π¦) β© (β‘πΉ β π)) = ((π‘ β© (β‘πΉ β π)) β© (π¦ β© (β‘πΉ β π))) |
88 | 86, 87 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = (π¦ β© (β‘πΉ β π)) β ((π‘ β© (β‘πΉ β π)) β© π§) = ((π‘ β© π¦) β© (β‘πΉ β π))) |
89 | 88 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = (π¦ β© (β‘πΉ β π)) β (((π‘ β© (β‘πΉ β π)) β© π§) = β
β ((π‘ β© π¦) β© (β‘πΉ β π)) = β
)) |
90 | 85, 89 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (π¦ β© (β‘πΉ β π)) β ((π§ β (π‘ β© (β‘πΉ β π)) β ((π‘ β© (β‘πΉ β π)) β© π§) = β
) β ((π¦ β© (β‘πΉ β π)) β (π‘ β© (β‘πΉ β π)) β ((π‘ β© π¦) β© (β‘πΉ β π)) = β
))) |
91 | 84, 90 | syl5ibrcom 247 |
. . . . . . . . . . . . . . 15
β’
(((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β§ π¦ β π₯) β (π§ = (π¦ β© (β‘πΉ β π)) β (π§ β (π‘ β© (β‘πΉ β π)) β ((π‘ β© (β‘πΉ β π)) β© π§) = β
))) |
92 | 91 | rexlimdva 3153 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β (βπ¦ β π₯ π§ = (π¦ β© (β‘πΉ β π)) β (π§ β (π‘ β© (β‘πΉ β π)) β ((π‘ β© (β‘πΉ β π)) β© π§) = β
))) |
93 | 72, 92 | biimtrid 241 |
. . . . . . . . . . . . 13
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β (π§ β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β (π§ β (π‘ β© (β‘πΉ β π)) β ((π‘ β© (β‘πΉ β π)) β© π§) = β
))) |
94 | 93 | impd 412 |
. . . . . . . . . . . 12
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β ((π§ β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β§ π§ β (π‘ β© (β‘πΉ β π))) β ((π‘ β© (β‘πΉ β π)) β© π§) = β
)) |
95 | 69, 94 | biimtrid 241 |
. . . . . . . . . . 11
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β (π§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {(π‘ β© (β‘πΉ β π))}) β ((π‘ β© (β‘πΉ β π)) β© π§) = β
)) |
96 | 95 | ralrimiv 3143 |
. . . . . . . . . 10
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {(π‘ β© (β‘πΉ β π))})((π‘ β© (β‘πΉ β π)) β© π§) = β
) |
97 | | inss1 4193 |
. . . . . . . . . . . . 13
β’ (π‘ β© (β‘πΉ β π)) β π‘ |
98 | | resabs1 5972 |
. . . . . . . . . . . . 13
β’ ((π‘ β© (β‘πΉ β π)) β π‘ β ((πΉ βΎ π‘) βΎ (π‘ β© (β‘πΉ β π))) = (πΉ βΎ (π‘ β© (β‘πΉ β π)))) |
99 | 97, 98 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((πΉ βΎ π‘) βΎ (π‘ β© (β‘πΉ β π))) = (πΉ βΎ (π‘ β© (β‘πΉ β π))) |
100 | 7 | cvmshmeo 33905 |
. . . . . . . . . . . . . 14
β’ ((π₯ β (πβπ) β§ π‘ β π₯) β (πΉ βΎ π‘) β ((πΆ βΎt π‘)Homeo(π½ βΎt π))) |
101 | 100 | adantll 713 |
. . . . . . . . . . . . 13
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β (πΉ βΎ π‘) β ((πΆ βΎt π‘)Homeo(π½ βΎt π))) |
102 | 5 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β πΆ β Top) |
103 | 9 | sselda 3949 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β π‘ β πΆ) |
104 | | elssuni 4903 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β πΆ β π‘ β βͺ πΆ) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β π‘ β βͺ πΆ) |
106 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’ βͺ πΆ =
βͺ πΆ |
107 | 106 | restuni 22529 |
. . . . . . . . . . . . . . 15
β’ ((πΆ β Top β§ π‘ β βͺ πΆ)
β π‘ = βͺ (πΆ
βΎt π‘)) |
108 | 102, 105,
107 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β π‘ = βͺ (πΆ βΎt π‘)) |
109 | 97, 108 | sseqtrid 4001 |
. . . . . . . . . . . . 13
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β (π‘ β© (β‘πΉ β π)) β βͺ
(πΆ βΎt
π‘)) |
110 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ βͺ (πΆ
βΎt π‘) =
βͺ (πΆ βΎt π‘) |
111 | 110 | hmeores 23138 |
. . . . . . . . . . . . 13
β’ (((πΉ βΎ π‘) β ((πΆ βΎt π‘)Homeo(π½ βΎt π)) β§ (π‘ β© (β‘πΉ β π)) β βͺ
(πΆ βΎt
π‘)) β ((πΉ βΎ π‘) βΎ (π‘ β© (β‘πΉ β π))) β (((πΆ βΎt π‘) βΎt (π‘ β© (β‘πΉ β π)))Homeo((π½ βΎt π) βΎt ((πΉ βΎ π‘) β (π‘ β© (β‘πΉ β π)))))) |
112 | 101, 109,
111 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β ((πΉ βΎ π‘) βΎ (π‘ β© (β‘πΉ β π))) β (((πΆ βΎt π‘) βΎt (π‘ β© (β‘πΉ β π)))Homeo((π½ βΎt π) βΎt ((πΉ βΎ π‘) β (π‘ β© (β‘πΉ β π)))))) |
113 | 99, 112 | eqeltrrid 2843 |
. . . . . . . . . . 11
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β (πΉ βΎ (π‘ β© (β‘πΉ β π))) β (((πΆ βΎt π‘) βΎt (π‘ β© (β‘πΉ β π)))Homeo((π½ βΎt π) βΎt ((πΉ βΎ π‘) β (π‘ β© (β‘πΉ β π)))))) |
114 | 97 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β (π‘ β© (β‘πΉ β π)) β π‘) |
115 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β π‘ β π₯) |
116 | | restabs 22532 |
. . . . . . . . . . . . 13
β’ ((πΆ β Top β§ (π‘ β© (β‘πΉ β π)) β π‘ β§ π‘ β π₯) β ((πΆ βΎt π‘) βΎt (π‘ β© (β‘πΉ β π))) = (πΆ βΎt (π‘ β© (β‘πΉ β π)))) |
117 | 102, 114,
115, 116 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β ((πΆ βΎt π‘) βΎt (π‘ β© (β‘πΉ β π))) = (πΆ βΎt (π‘ β© (β‘πΉ β π)))) |
118 | | incom 4166 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ β© (β‘πΉ β π)) = ((β‘πΉ β π) β© π‘) |
119 | | cnvresima 6187 |
. . . . . . . . . . . . . . . . 17
β’ (β‘(πΉ βΎ π‘) β π) = ((β‘πΉ β π) β© π‘) |
120 | 118, 119 | eqtr4i 2768 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β© (β‘πΉ β π)) = (β‘(πΉ βΎ π‘) β π) |
121 | 120 | imaeq2i 6016 |
. . . . . . . . . . . . . . 15
β’ ((πΉ βΎ π‘) β (π‘ β© (β‘πΉ β π))) = ((πΉ βΎ π‘) β (β‘(πΉ βΎ π‘) β π)) |
122 | 3 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β πΉ β (πΆ CovMap π½)) |
123 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β π₯ β (πβπ)) |
124 | 7 | cvmsf1o 33906 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ β (πΆ CovMap π½) β§ π₯ β (πβπ) β§ π‘ β π₯) β (πΉ βΎ π‘):π‘β1-1-ontoβπ) |
125 | 122, 123,
115, 124 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β (πΉ βΎ π‘):π‘β1-1-ontoβπ) |
126 | | f1ofo 6796 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ βΎ π‘):π‘β1-1-ontoβπ β (πΉ βΎ π‘):π‘βontoβπ) |
127 | 125, 126 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β (πΉ βΎ π‘):π‘βontoβπ) |
128 | 39 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β π β π) |
129 | | foimacnv 6806 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ βΎ π‘):π‘βontoβπ β§ π β π) β ((πΉ βΎ π‘) β (β‘(πΉ βΎ π‘) β π)) = π) |
130 | 127, 128,
129 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β ((πΉ βΎ π‘) β (β‘(πΉ βΎ π‘) β π)) = π) |
131 | 121, 130 | eqtrid 2789 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β ((πΉ βΎ π‘) β (π‘ β© (β‘πΉ β π))) = π) |
132 | 131 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β ((π½ βΎt π) βΎt ((πΉ βΎ π‘) β (π‘ β© (β‘πΉ β π)))) = ((π½ βΎt π) βΎt π)) |
133 | | cvmtop2 33895 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β (πΆ CovMap π½) β π½ β Top) |
134 | 3, 133 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β π½ β Top) |
135 | 7 | cvmsrcl 33898 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (πβπ) β π β π½) |
136 | 135 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β π β π½) |
137 | | restabs 22532 |
. . . . . . . . . . . . . . 15
β’ ((π½ β Top β§ π β π β§ π β π½) β ((π½ βΎt π) βΎt π) = (π½ βΎt π)) |
138 | 134, 39, 136, 137 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β ((π½ βΎt π) βΎt π) = (π½ βΎt π)) |
139 | 138 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β ((π½ βΎt π) βΎt π) = (π½ βΎt π)) |
140 | 132, 139 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β ((π½ βΎt π) βΎt ((πΉ βΎ π‘) β (π‘ β© (β‘πΉ β π)))) = (π½ βΎt π)) |
141 | 117, 140 | oveq12d 7380 |
. . . . . . . . . . 11
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β (((πΆ βΎt π‘) βΎt (π‘ β© (β‘πΉ β π)))Homeo((π½ βΎt π) βΎt ((πΉ βΎ π‘) β (π‘ β© (β‘πΉ β π))))) = ((πΆ βΎt (π‘ β© (β‘πΉ β π)))Homeo(π½ βΎt π))) |
142 | 113, 141 | eleqtrd 2840 |
. . . . . . . . . 10
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β (πΉ βΎ (π‘ β© (β‘πΉ β π))) β ((πΆ βΎt (π‘ β© (β‘πΉ β π)))Homeo(π½ βΎt π))) |
143 | 96, 142 | jca 513 |
. . . . . . . . 9
β’ ((((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β§ π‘ β π₯) β (βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {(π‘ β© (β‘πΉ β π))})((π‘ β© (β‘πΉ β π)) β© π§) = β
β§ (πΉ βΎ (π‘ β© (β‘πΉ β π))) β ((πΆ βΎt (π‘ β© (β‘πΉ β π)))Homeo(π½ βΎt π)))) |
144 | 143 | ralrimiva 3144 |
. . . . . . . 8
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β βπ‘ β π₯ (βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {(π‘ β© (β‘πΉ β π))})((π‘ β© (β‘πΉ β π)) β© π§) = β
β§ (πΉ βΎ (π‘ β© (β‘πΉ β π))) β ((πΆ βΎt (π‘ β© (β‘πΉ β π)))Homeo(π½ βΎt π)))) |
145 | 52 | rgenw 3069 |
. . . . . . . . 9
β’
βπ‘ β
π₯ (π‘ β© (β‘πΉ β π)) β V |
146 | 47 | cbvmptv 5223 |
. . . . . . . . . 10
β’ (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) = (π‘ β π₯ β¦ (π‘ β© (β‘πΉ β π))) |
147 | | sneq 4601 |
. . . . . . . . . . . . 13
β’ (π€ = (π‘ β© (β‘πΉ β π)) β {π€} = {(π‘ β© (β‘πΉ β π))}) |
148 | 147 | difeq2d 4087 |
. . . . . . . . . . . 12
β’ (π€ = (π‘ β© (β‘πΉ β π)) β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {π€}) = (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {(π‘ β© (β‘πΉ β π))})) |
149 | | ineq1 4170 |
. . . . . . . . . . . . 13
β’ (π€ = (π‘ β© (β‘πΉ β π)) β (π€ β© π§) = ((π‘ β© (β‘πΉ β π)) β© π§)) |
150 | 149 | eqeq1d 2739 |
. . . . . . . . . . . 12
β’ (π€ = (π‘ β© (β‘πΉ β π)) β ((π€ β© π§) = β
β ((π‘ β© (β‘πΉ β π)) β© π§) = β
)) |
151 | 148, 150 | raleqbidv 3322 |
. . . . . . . . . . 11
β’ (π€ = (π‘ β© (β‘πΉ β π)) β (βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {π€})(π€ β© π§) = β
β βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {(π‘ β© (β‘πΉ β π))})((π‘ β© (β‘πΉ β π)) β© π§) = β
)) |
152 | | reseq2 5937 |
. . . . . . . . . . . 12
β’ (π€ = (π‘ β© (β‘πΉ β π)) β (πΉ βΎ π€) = (πΉ βΎ (π‘ β© (β‘πΉ β π)))) |
153 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π€ = (π‘ β© (β‘πΉ β π)) β (πΆ βΎt π€) = (πΆ βΎt (π‘ β© (β‘πΉ β π)))) |
154 | 153 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (π€ = (π‘ β© (β‘πΉ β π)) β ((πΆ βΎt π€)Homeo(π½ βΎt π)) = ((πΆ βΎt (π‘ β© (β‘πΉ β π)))Homeo(π½ βΎt π))) |
155 | 152, 154 | eleq12d 2832 |
. . . . . . . . . . 11
β’ (π€ = (π‘ β© (β‘πΉ β π)) β ((πΉ βΎ π€) β ((πΆ βΎt π€)Homeo(π½ βΎt π)) β (πΉ βΎ (π‘ β© (β‘πΉ β π))) β ((πΆ βΎt (π‘ β© (β‘πΉ β π)))Homeo(π½ βΎt π)))) |
156 | 151, 155 | anbi12d 632 |
. . . . . . . . . 10
β’ (π€ = (π‘ β© (β‘πΉ β π)) β ((βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {π€})(π€ β© π§) = β
β§ (πΉ βΎ π€) β ((πΆ βΎt π€)Homeo(π½ βΎt π))) β (βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {(π‘ β© (β‘πΉ β π))})((π‘ β© (β‘πΉ β π)) β© π§) = β
β§ (πΉ βΎ (π‘ β© (β‘πΉ β π))) β ((πΆ βΎt (π‘ β© (β‘πΉ β π)))Homeo(π½ βΎt π))))) |
157 | 146, 156 | ralrnmptw 7049 |
. . . . . . . . 9
β’
(βπ‘ β
π₯ (π‘ β© (β‘πΉ β π)) β V β (βπ€ β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π)))(βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {π€})(π€ β© π§) = β
β§ (πΉ βΎ π€) β ((πΆ βΎt π€)Homeo(π½ βΎt π))) β βπ‘ β π₯ (βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {(π‘ β© (β‘πΉ β π))})((π‘ β© (β‘πΉ β π)) β© π§) = β
β§ (πΉ βΎ (π‘ β© (β‘πΉ β π))) β ((πΆ βΎt (π‘ β© (β‘πΉ β π)))Homeo(π½ βΎt π))))) |
158 | 145, 157 | ax-mp 5 |
. . . . . . . 8
β’
(βπ€ β
ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π)))(βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {π€})(π€ β© π§) = β
β§ (πΉ βΎ π€) β ((πΆ βΎt π€)Homeo(π½ βΎt π))) β βπ‘ β π₯ (βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {(π‘ β© (β‘πΉ β π))})((π‘ β© (β‘πΉ β π)) β© π§) = β
β§ (πΉ βΎ (π‘ β© (β‘πΉ β π))) β ((πΆ βΎt (π‘ β© (β‘πΉ β π)))Homeo(π½ βΎt π)))) |
159 | 144, 158 | sylibr 233 |
. . . . . . 7
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β βπ€ β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π)))(βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {π€})(π€ β© π§) = β
β§ (πΉ βΎ π€) β ((πΆ βΎt π€)Homeo(π½ βΎt π)))) |
160 | 68, 159 | jca 513 |
. . . . . 6
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β (βͺ ran
(π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) = (β‘πΉ β π) β§ βπ€ β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π)))(βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {π€})(π€ β© π§) = β
β§ (πΉ βΎ π€) β ((πΆ βΎt π€)Homeo(π½ βΎt π))))) |
161 | 7 | cvmscbv 33892 |
. . . . . . . 8
β’ π = (π β π½ β¦ {π β (π« πΆ β {β
}) β£ (βͺ π =
(β‘πΉ β π) β§ βπ€ β π (βπ§ β (π β {π€})(π€ β© π§) = β
β§ (πΉ βΎ π€) β ((πΆ βΎt π€)Homeo(π½ βΎt π))))}) |
162 | 161 | cvmsval 33900 |
. . . . . . 7
β’ (πΆ β Top β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β (πβπ) β (π β π½ β§ (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β πΆ β§ ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β β
) β§ (βͺ ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) = (β‘πΉ β π) β§ βπ€ β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π)))(βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {π€})(π€ β© π§) = β
β§ (πΉ βΎ π€) β ((πΆ βΎt π€)Homeo(π½ βΎt π))))))) |
163 | 5, 162 | syl 17 |
. . . . . 6
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β (πβπ) β (π β π½ β§ (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β πΆ β§ ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β β
) β§ (βͺ ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) = (β‘πΉ β π) β§ βπ€ β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π)))(βπ§ β (ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β {π€})(π€ β© π§) = β
β§ (πΉ βΎ π€) β ((πΆ βΎt π€)Homeo(π½ βΎt π))))))) |
164 | 2, 30, 160, 163 | mpbir3and 1343 |
. . . . 5
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β ran (π¦ β π₯ β¦ (π¦ β© (β‘πΉ β π))) β (πβπ)) |
165 | 164 | ne0d 4300 |
. . . 4
β’ (((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β§ π₯ β (πβπ)) β (πβπ) β β
) |
166 | 165 | ex 414 |
. . 3
β’ ((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β (π₯ β (πβπ) β (πβπ) β β
)) |
167 | 166 | exlimdv 1937 |
. 2
β’ ((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β (βπ₯ π₯ β (πβπ) β (πβπ) β β
)) |
168 | 1, 167 | biimtrid 241 |
1
β’ ((πΉ β (πΆ CovMap π½) β§ π β π½ β§ π β π) β ((πβπ) β β
β (πβπ) β β
)) |