Step | Hyp | Ref
| Expression |
1 | | cvmlift2lem9a.f |
. . . 4
β’ (π β πΉ β (πΆ CovMap π½)) |
2 | | cvmtop1 34320 |
. . . 4
β’ (πΉ β (πΆ CovMap π½) β πΆ β Top) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β πΆ β Top) |
4 | | cnrest2r 22798 |
. . 3
β’ (πΆ β Top β ((πΎ βΎt π) Cn (πΆ βΎt π)) β ((πΎ βΎt π) Cn πΆ)) |
5 | 3, 4 | syl 17 |
. 2
β’ (π β ((πΎ βΎt π) Cn (πΆ βΎt π)) β ((πΎ βΎt π) Cn πΆ)) |
6 | | cvmlift2lem9a.h |
. . . . . 6
β’ (π β π»:πβΆπ΅) |
7 | 6 | ffnd 6718 |
. . . . 5
β’ (π β π» Fn π) |
8 | | cvmlift2lem9a.4 |
. . . . 5
β’ (π β π β π) |
9 | | fnssres 6673 |
. . . . 5
β’ ((π» Fn π β§ π β π) β (π» βΎ π) Fn π) |
10 | 7, 8, 9 | syl2anc 584 |
. . . 4
β’ (π β (π» βΎ π) Fn π) |
11 | | df-ima 5689 |
. . . . 5
β’ (π» β π) = ran (π» βΎ π) |
12 | | cvmlift2lem9a.6 |
. . . . 5
β’ (π β (π» β π) β π) |
13 | 11, 12 | eqsstrrid 4031 |
. . . 4
β’ (π β ran (π» βΎ π) β π) |
14 | | df-f 6547 |
. . . 4
β’ ((π» βΎ π):πβΆπ β ((π» βΎ π) Fn π β§ ran (π» βΎ π) β π)) |
15 | 10, 13, 14 | sylanbrc 583 |
. . 3
β’ (π β (π» βΎ π):πβΆπ) |
16 | | cvmlift2lem9a.2 |
. . . . . . . . . . 11
β’ (π β π β (πβπ΄)) |
17 | | cvmlift2lem9a.3 |
. . . . . . . . . . . 12
β’ (π β (π β π β§ (π»βπ) β π)) |
18 | 17 | simpld 495 |
. . . . . . . . . . 11
β’ (π β π β π) |
19 | | cvmlift2lem9a.s |
. . . . . . . . . . . 12
β’ π = (π β π½ β¦ {π β (π« πΆ β {β
}) β£ (βͺ π =
(β‘πΉ β π) β§ βπ β π (βπ β (π β {π})(π β© π) = β
β§ (πΉ βΎ π) β ((πΆ βΎt π)Homeo(π½ βΎt π))))}) |
20 | 19 | cvmsf1o 34332 |
. . . . . . . . . . 11
β’ ((πΉ β (πΆ CovMap π½) β§ π β (πβπ΄) β§ π β π) β (πΉ βΎ π):πβ1-1-ontoβπ΄) |
21 | 1, 16, 18, 20 | syl3anc 1371 |
. . . . . . . . . 10
β’ (π β (πΉ βΎ π):πβ1-1-ontoβπ΄) |
22 | 21 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΆ βΎt π)) β (πΉ βΎ π):πβ1-1-ontoβπ΄) |
23 | | f1of1 6832 |
. . . . . . . . 9
β’ ((πΉ βΎ π):πβ1-1-ontoβπ΄ β (πΉ βΎ π):πβ1-1βπ΄) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΆ βΎt π)) β (πΉ βΎ π):πβ1-1βπ΄) |
25 | | cvmlift2lem9a.b |
. . . . . . . . . . . 12
β’ π΅ = βͺ
πΆ |
26 | 25 | toptopon 22426 |
. . . . . . . . . . 11
β’ (πΆ β Top β πΆ β (TopOnβπ΅)) |
27 | 3, 26 | sylib 217 |
. . . . . . . . . 10
β’ (π β πΆ β (TopOnβπ΅)) |
28 | 19 | cvmsss 34327 |
. . . . . . . . . . . . 13
β’ (π β (πβπ΄) β π β πΆ) |
29 | 16, 28 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β πΆ) |
30 | 29, 18 | sseldd 3983 |
. . . . . . . . . . 11
β’ (π β π β πΆ) |
31 | | toponss 22436 |
. . . . . . . . . . 11
β’ ((πΆ β (TopOnβπ΅) β§ π β πΆ) β π β π΅) |
32 | 27, 30, 31 | syl2anc 584 |
. . . . . . . . . 10
β’ (π β π β π΅) |
33 | | resttopon 22672 |
. . . . . . . . . 10
β’ ((πΆ β (TopOnβπ΅) β§ π β π΅) β (πΆ βΎt π) β (TopOnβπ)) |
34 | 27, 32, 33 | syl2anc 584 |
. . . . . . . . 9
β’ (π β (πΆ βΎt π) β (TopOnβπ)) |
35 | | toponss 22436 |
. . . . . . . . 9
β’ (((πΆ βΎt π) β (TopOnβπ) β§ π₯ β (πΆ βΎt π)) β π₯ β π) |
36 | 34, 35 | sylan 580 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΆ βΎt π)) β π₯ β π) |
37 | | f1imacnv 6849 |
. . . . . . . 8
β’ (((πΉ βΎ π):πβ1-1βπ΄ β§ π₯ β π) β (β‘(πΉ βΎ π) β ((πΉ βΎ π) β π₯)) = π₯) |
38 | 24, 36, 37 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ π₯ β (πΆ βΎt π)) β (β‘(πΉ βΎ π) β ((πΉ βΎ π) β π₯)) = π₯) |
39 | 38 | imaeq2d 6059 |
. . . . . 6
β’ ((π β§ π₯ β (πΆ βΎt π)) β (β‘(π» βΎ π) β (β‘(πΉ βΎ π) β ((πΉ βΎ π) β π₯))) = (β‘(π» βΎ π) β π₯)) |
40 | | imaco 6250 |
. . . . . . 7
β’ ((β‘(π» βΎ π) β β‘(πΉ βΎ π)) β ((πΉ βΎ π) β π₯)) = (β‘(π» βΎ π) β (β‘(πΉ βΎ π) β ((πΉ βΎ π) β π₯))) |
41 | | cnvco 5885 |
. . . . . . . . 9
β’ β‘((πΉ βΎ π) β (π» βΎ π)) = (β‘(π» βΎ π) β β‘(πΉ βΎ π)) |
42 | | cores 6248 |
. . . . . . . . . . . . 13
β’ (ran
(π» βΎ π) β π β ((πΉ βΎ π) β (π» βΎ π)) = (πΉ β (π» βΎ π))) |
43 | 13, 42 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((πΉ βΎ π) β (π» βΎ π)) = (πΉ β (π» βΎ π))) |
44 | | resco 6249 |
. . . . . . . . . . . 12
β’ ((πΉ β π») βΎ π) = (πΉ β (π» βΎ π)) |
45 | 43, 44 | eqtr4di 2790 |
. . . . . . . . . . 11
β’ (π β ((πΉ βΎ π) β (π» βΎ π)) = ((πΉ β π») βΎ π)) |
46 | 45 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (πΆ βΎt π)) β ((πΉ βΎ π) β (π» βΎ π)) = ((πΉ β π») βΎ π)) |
47 | 46 | cnveqd 5875 |
. . . . . . . . 9
β’ ((π β§ π₯ β (πΆ βΎt π)) β β‘((πΉ βΎ π) β (π» βΎ π)) = β‘((πΉ β π») βΎ π)) |
48 | 41, 47 | eqtr3id 2786 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΆ βΎt π)) β (β‘(π» βΎ π) β β‘(πΉ βΎ π)) = β‘((πΉ β π») βΎ π)) |
49 | 48 | imaeq1d 6058 |
. . . . . . 7
β’ ((π β§ π₯ β (πΆ βΎt π)) β ((β‘(π» βΎ π) β β‘(πΉ βΎ π)) β ((πΉ βΎ π) β π₯)) = (β‘((πΉ β π») βΎ π) β ((πΉ βΎ π) β π₯))) |
50 | 40, 49 | eqtr3id 2786 |
. . . . . 6
β’ ((π β§ π₯ β (πΆ βΎt π)) β (β‘(π» βΎ π) β (β‘(πΉ βΎ π) β ((πΉ βΎ π) β π₯))) = (β‘((πΉ β π») βΎ π) β ((πΉ βΎ π) β π₯))) |
51 | 39, 50 | eqtr3d 2774 |
. . . . 5
β’ ((π β§ π₯ β (πΆ βΎt π)) β (β‘(π» βΎ π) β π₯) = (β‘((πΉ β π») βΎ π) β ((πΉ βΎ π) β π₯))) |
52 | | cvmlift2lem9a.g |
. . . . . . . 8
β’ (π β (πΉ β π») β (πΎ Cn π½)) |
53 | | cvmlift2lem9a.y |
. . . . . . . . 9
β’ π = βͺ
πΎ |
54 | 53 | cnrest 22796 |
. . . . . . . 8
β’ (((πΉ β π») β (πΎ Cn π½) β§ π β π) β ((πΉ β π») βΎ π) β ((πΎ βΎt π) Cn π½)) |
55 | 52, 8, 54 | syl2anc 584 |
. . . . . . 7
β’ (π β ((πΉ β π») βΎ π) β ((πΎ βΎt π) Cn π½)) |
56 | 55 | adantr 481 |
. . . . . 6
β’ ((π β§ π₯ β (πΆ βΎt π)) β ((πΉ β π») βΎ π) β ((πΎ βΎt π) Cn π½)) |
57 | | resima2 6016 |
. . . . . . . 8
β’ (π₯ β π β ((πΉ βΎ π) β π₯) = (πΉ β π₯)) |
58 | 36, 57 | syl 17 |
. . . . . . 7
β’ ((π β§ π₯ β (πΆ βΎt π)) β ((πΉ βΎ π) β π₯) = (πΉ β π₯)) |
59 | 1 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΆ βΎt π)) β πΉ β (πΆ CovMap π½)) |
60 | | restopn2 22688 |
. . . . . . . . . 10
β’ ((πΆ β Top β§ π β πΆ) β (π₯ β (πΆ βΎt π) β (π₯ β πΆ β§ π₯ β π))) |
61 | 3, 30, 60 | syl2anc 584 |
. . . . . . . . 9
β’ (π β (π₯ β (πΆ βΎt π) β (π₯ β πΆ β§ π₯ β π))) |
62 | 61 | simprbda 499 |
. . . . . . . 8
β’ ((π β§ π₯ β (πΆ βΎt π)) β π₯ β πΆ) |
63 | | cvmopn 34340 |
. . . . . . . 8
β’ ((πΉ β (πΆ CovMap π½) β§ π₯ β πΆ) β (πΉ β π₯) β π½) |
64 | 59, 62, 63 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ π₯ β (πΆ βΎt π)) β (πΉ β π₯) β π½) |
65 | 58, 64 | eqeltrd 2833 |
. . . . . 6
β’ ((π β§ π₯ β (πΆ βΎt π)) β ((πΉ βΎ π) β π₯) β π½) |
66 | | cnima 22776 |
. . . . . 6
β’ ((((πΉ β π») βΎ π) β ((πΎ βΎt π) Cn π½) β§ ((πΉ βΎ π) β π₯) β π½) β (β‘((πΉ β π») βΎ π) β ((πΉ βΎ π) β π₯)) β (πΎ βΎt π)) |
67 | 56, 65, 66 | syl2anc 584 |
. . . . 5
β’ ((π β§ π₯ β (πΆ βΎt π)) β (β‘((πΉ β π») βΎ π) β ((πΉ βΎ π) β π₯)) β (πΎ βΎt π)) |
68 | 51, 67 | eqeltrd 2833 |
. . . 4
β’ ((π β§ π₯ β (πΆ βΎt π)) β (β‘(π» βΎ π) β π₯) β (πΎ βΎt π)) |
69 | 68 | ralrimiva 3146 |
. . 3
β’ (π β βπ₯ β (πΆ βΎt π)(β‘(π» βΎ π) β π₯) β (πΎ βΎt π)) |
70 | | cvmlift2lem9a.k |
. . . . . 6
β’ (π β πΎ β Top) |
71 | 53 | toptopon 22426 |
. . . . . 6
β’ (πΎ β Top β πΎ β (TopOnβπ)) |
72 | 70, 71 | sylib 217 |
. . . . 5
β’ (π β πΎ β (TopOnβπ)) |
73 | | resttopon 22672 |
. . . . 5
β’ ((πΎ β (TopOnβπ) β§ π β π) β (πΎ βΎt π) β (TopOnβπ)) |
74 | 72, 8, 73 | syl2anc 584 |
. . . 4
β’ (π β (πΎ βΎt π) β (TopOnβπ)) |
75 | | iscn 22746 |
. . . 4
β’ (((πΎ βΎt π) β (TopOnβπ) β§ (πΆ βΎt π) β (TopOnβπ)) β ((π» βΎ π) β ((πΎ βΎt π) Cn (πΆ βΎt π)) β ((π» βΎ π):πβΆπ β§ βπ₯ β (πΆ βΎt π)(β‘(π» βΎ π) β π₯) β (πΎ βΎt π)))) |
76 | 74, 34, 75 | syl2anc 584 |
. . 3
β’ (π β ((π» βΎ π) β ((πΎ βΎt π) Cn (πΆ βΎt π)) β ((π» βΎ π):πβΆπ β§ βπ₯ β (πΆ βΎt π)(β‘(π» βΎ π) β π₯) β (πΎ βΎt π)))) |
77 | 15, 69, 76 | mpbir2and 711 |
. 2
β’ (π β (π» βΎ π) β ((πΎ βΎt π) Cn (πΆ βΎt π))) |
78 | 5, 77 | sseldd 3983 |
1
β’ (π β (π» βΎ π) β ((πΎ βΎt π) Cn πΆ)) |