Step | Hyp | Ref
| Expression |
1 | | cvmlift3.b |
. . . 4
β’ π΅ = βͺ
πΆ |
2 | | cvmlift3.y |
. . . 4
β’ π = βͺ
πΎ |
3 | | cvmlift3lem7.s |
. . . 4
β’ π = (π β π½ β¦ {π β (π« πΆ β {β
}) β£ (βͺ π =
(β‘πΉ β π) β§ βπ β π (βπ β (π β {π})(π β© π) = β
β§ (πΉ βΎ π) β ((πΆ βΎt π)Homeo(π½ βΎt π))))}) |
4 | | cvmlift3.f |
. . . 4
β’ (π β πΉ β (πΆ CovMap π½)) |
5 | | cvmlift3.k |
. . . . 5
β’ (π β πΎ β SConn) |
6 | | cvmlift3.l |
. . . . 5
β’ (π β πΎ β π-Locally
PConn) |
7 | | cvmlift3.o |
. . . . 5
β’ (π β π β π) |
8 | | cvmlift3.g |
. . . . 5
β’ (π β πΊ β (πΎ Cn π½)) |
9 | | cvmlift3.p |
. . . . 5
β’ (π β π β π΅) |
10 | | cvmlift3.e |
. . . . 5
β’ (π β (πΉβπ) = (πΊβπ)) |
11 | | cvmlift3.h |
. . . . 5
β’ π» = (π₯ β π β¦ (β©π§ β π΅ βπ β (II Cn πΎ)((πβ0) = π β§ (πβ1) = π₯ β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = π§))) |
12 | 1, 2, 4, 5, 6, 7, 8, 9, 10, 11 | cvmlift3lem3 33979 |
. . . 4
β’ (π β π»:πβΆπ΅) |
13 | 1, 2, 4, 5, 6, 7, 8, 9, 10, 11 | cvmlift3lem5 33981 |
. . . . 5
β’ (π β (πΉ β π») = πΊ) |
14 | 13, 8 | eqeltrd 2834 |
. . . 4
β’ (π β (πΉ β π») β (πΎ Cn π½)) |
15 | | sconntop 33886 |
. . . . 5
β’ (πΎ β SConn β πΎ β Top) |
16 | 5, 15 | syl 17 |
. . . 4
β’ (π β πΎ β Top) |
17 | | cvmlift3lem7.3 |
. . . . . 6
β’ (π β π β (β‘πΊ β π΄)) |
18 | | cnvimass 6037 |
. . . . . . 7
β’ (β‘πΊ β π΄) β dom πΊ |
19 | | eqid 2733 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ π½ |
20 | 2, 19 | cnf 22620 |
. . . . . . . 8
β’ (πΊ β (πΎ Cn π½) β πΊ:πβΆβͺ π½) |
21 | | fdm 6681 |
. . . . . . . 8
β’ (πΊ:πβΆβͺ π½ β dom πΊ = π) |
22 | 8, 20, 21 | 3syl 18 |
. . . . . . 7
β’ (π β dom πΊ = π) |
23 | 18, 22 | sseqtrid 4000 |
. . . . . 6
β’ (π β (β‘πΊ β π΄) β π) |
24 | 17, 23 | sstrd 3958 |
. . . . 5
β’ (π β π β π) |
25 | | cvmlift3lem7.5 |
. . . . . 6
β’ (π β π β π) |
26 | | cvmlift3lem7.6 |
. . . . . 6
β’ (π β π β π) |
27 | 25, 26 | sseldd 3949 |
. . . . 5
β’ (π β π β π) |
28 | 24, 27 | sseldd 3949 |
. . . 4
β’ (π β π β π) |
29 | | cvmlift3lem7.2 |
. . . 4
β’ (π β π β (πβπ΄)) |
30 | 12, 28 | ffvelcdmd 7040 |
. . . . 5
β’ (π β (π»βπ) β π΅) |
31 | | fvco3 6944 |
. . . . . . . 8
β’ ((π»:πβΆπ΅ β§ π β π) β ((πΉ β π»)βπ) = (πΉβ(π»βπ))) |
32 | 12, 28, 31 | syl2anc 585 |
. . . . . . 7
β’ (π β ((πΉ β π»)βπ) = (πΉβ(π»βπ))) |
33 | 13 | fveq1d 6848 |
. . . . . . 7
β’ (π β ((πΉ β π»)βπ) = (πΊβπ)) |
34 | 32, 33 | eqtr3d 2775 |
. . . . . 6
β’ (π β (πΉβ(π»βπ)) = (πΊβπ)) |
35 | | cvmlift3lem7.1 |
. . . . . 6
β’ (π β (πΊβπ) β π΄) |
36 | 34, 35 | eqeltrd 2834 |
. . . . 5
β’ (π β (πΉβ(π»βπ)) β π΄) |
37 | | cvmlift3lem7.w |
. . . . . 6
β’ π = (β©π β π (π»βπ) β π) |
38 | 3, 1, 37 | cvmsiota 33935 |
. . . . 5
β’ ((πΉ β (πΆ CovMap π½) β§ (π β (πβπ΄) β§ (π»βπ) β π΅ β§ (πΉβ(π»βπ)) β π΄)) β (π β π β§ (π»βπ) β π)) |
39 | 4, 29, 30, 36, 38 | syl13anc 1373 |
. . . 4
β’ (π β (π β π β§ (π»βπ) β π)) |
40 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π»βπ) = (π»βπ) |
41 | 1, 2, 4, 5, 6, 7, 8, 9, 10, 11 | cvmlift3lem4 33980 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β ((π»βπ) = (π»βπ) β βπ β (II Cn πΎ)((πβ0) = π β§ (πβ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = (π»βπ)))) |
42 | 40, 41 | mpbii 232 |
. . . . . . . . . 10
β’ ((π β§ π β π) β βπ β (II Cn πΎ)((πβ0) = π β§ (πβ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = (π»βπ))) |
43 | 28, 42 | mpdan 686 |
. . . . . . . . 9
β’ (π β βπ β (II Cn πΎ)((πβ0) = π β§ (πβ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = (π»βπ))) |
44 | 43 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β βπ β (II Cn πΎ)((πβ0) = π β§ (πβ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = (π»βπ))) |
45 | | fveq1 6845 |
. . . . . . . . . . 11
β’ (π = β β (πβ0) = (ββ0)) |
46 | 45 | eqeq1d 2735 |
. . . . . . . . . 10
β’ (π = β β ((πβ0) = π β (ββ0) = π)) |
47 | | fveq1 6845 |
. . . . . . . . . . 11
β’ (π = β β (πβ1) = (ββ1)) |
48 | 47 | eqeq1d 2735 |
. . . . . . . . . 10
β’ (π = β β ((πβ1) = π β (ββ1) = π)) |
49 | | coeq2 5818 |
. . . . . . . . . . . . . . . 16
β’ (π = β β (πΊ β π) = (πΊ β β)) |
50 | 49 | eqeq2d 2744 |
. . . . . . . . . . . . . . 15
β’ (π = β β ((πΉ β π) = (πΊ β π) β (πΉ β π) = (πΊ β β))) |
51 | 50 | anbi1d 631 |
. . . . . . . . . . . . . 14
β’ (π = β β (((πΉ β π) = (πΊ β π) β§ (πβ0) = π) β ((πΉ β π) = (πΊ β β) β§ (πβ0) = π))) |
52 | 51 | riotabidv 7319 |
. . . . . . . . . . . . 13
β’ (π = β β (β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π)) = (β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))) |
53 | | coeq2 5818 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πΉ β π) = (πΉ β π)) |
54 | 53 | eqeq1d 2735 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πΉ β π) = (πΊ β β) β (πΉ β π) = (πΊ β β))) |
55 | | fveq1 6845 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πβ0) = (πβ0)) |
56 | 55 | eqeq1d 2735 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πβ0) = π β (πβ0) = π)) |
57 | 54, 56 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (π = π β (((πΉ β π) = (πΊ β β) β§ (πβ0) = π) β ((πΉ β π) = (πΊ β β) β§ (πβ0) = π))) |
58 | 57 | cbvriotavw 7327 |
. . . . . . . . . . . . 13
β’
(β©π
β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π)) = (β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π)) |
59 | 52, 58 | eqtr4di 2791 |
. . . . . . . . . . . 12
β’ (π = β β (β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π)) = (β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))) |
60 | 59 | fveq1d 6848 |
. . . . . . . . . . 11
β’ (π = β β ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1)) |
61 | 60 | eqeq1d 2735 |
. . . . . . . . . 10
β’ (π = β β (((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = (π»βπ) β ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ))) |
62 | 46, 48, 61 | 3anbi123d 1437 |
. . . . . . . . 9
β’ (π = β β (((πβ0) = π β§ (πβ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = (π»βπ)) β ((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)))) |
63 | 62 | cbvrexvw 3225 |
. . . . . . . 8
β’
(βπ β (II
Cn πΎ)((πβ0) = π β§ (πβ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = π))β1) = (π»βπ)) β ββ β (II Cn πΎ)((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ))) |
64 | 44, 63 | sylib 217 |
. . . . . . 7
β’ ((π β§ π¦ β π) β ββ β (II Cn πΎ)((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ))) |
65 | | cvmlift3lem7.7 |
. . . . . . . . 9
β’ (π β (πΎ βΎt π) β PConn) |
66 | 65 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β (πΎ βΎt π) β PConn) |
67 | 2 | restuni 22536 |
. . . . . . . . . . 11
β’ ((πΎ β Top β§ π β π) β π = βͺ (πΎ βΎt π)) |
68 | 16, 24, 67 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β π = βͺ (πΎ βΎt π)) |
69 | 27, 68 | eleqtrd 2836 |
. . . . . . . . 9
β’ (π β π β βͺ (πΎ βΎt π)) |
70 | 69 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β π β βͺ (πΎ βΎt π)) |
71 | 68 | eleq2d 2820 |
. . . . . . . . 9
β’ (π β (π¦ β π β π¦ β βͺ (πΎ βΎt π))) |
72 | 71 | biimpa 478 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β π¦ β βͺ (πΎ βΎt π)) |
73 | | eqid 2733 |
. . . . . . . . 9
β’ βͺ (πΎ
βΎt π) =
βͺ (πΎ βΎt π) |
74 | 73 | pconncn 33882 |
. . . . . . . 8
β’ (((πΎ βΎt π) β PConn β§ π β βͺ (πΎ
βΎt π)
β§ π¦ β βͺ (πΎ
βΎt π))
β βπ β (II
Cn (πΎ βΎt
π))((πβ0) = π β§ (πβ1) = π¦)) |
75 | 66, 70, 72, 74 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π¦ β π) β βπ β (II Cn (πΎ βΎt π))((πβ0) = π β§ (πβ1) = π¦)) |
76 | | reeanv 3216 |
. . . . . . . 8
β’
(ββ β (II
Cn πΎ)βπ β (II Cn (πΎ βΎt π))(((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦)) β (ββ β (II Cn πΎ)((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ βπ β (II Cn (πΎ βΎt π))((πβ0) = π β§ (πβ1) = π¦))) |
77 | 4 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β πΉ β (πΆ CovMap π½)) |
78 | 5 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β πΎ β SConn) |
79 | 6 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β πΎ β π-Locally
PConn) |
80 | 7 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β π β π) |
81 | 8 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β πΊ β (πΎ Cn π½)) |
82 | 9 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β π β π΅) |
83 | 10 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β (πΉβπ) = (πΊβπ)) |
84 | 35 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β (πΊβπ) β π΄) |
85 | 29 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β π β (πβπ΄)) |
86 | 17 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β π β (β‘πΊ β π΄)) |
87 | 27 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β π β π) |
88 | | simpllr 775 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β π¦ β π) |
89 | | simplrl 776 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β β β (II Cn πΎ)) |
90 | | simprl 770 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β ((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ))) |
91 | | simplrr 777 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β π β (II Cn (πΎ βΎt π))) |
92 | | simprr 772 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β ((πβ0) = π β§ (πβ1) = π¦)) |
93 | 53 | eqeq1d 2735 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΉ β π) = (πΊ β π) β (πΉ β π) = (πΊ β π))) |
94 | 55 | eqeq1d 2735 |
. . . . . . . . . . . . 13
β’ (π = π β ((πβ0) = (π»βπ) β (πβ0) = (π»βπ))) |
95 | 93, 94 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π = π β (((πΉ β π) = (πΊ β π) β§ (πβ0) = (π»βπ)) β ((πΉ β π) = (πΊ β π) β§ (πβ0) = (π»βπ)))) |
96 | 95 | cbvriotavw 7327 |
. . . . . . . . . . 11
β’
(β©π
β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = (π»βπ))) = (β©π β (II Cn πΆ)((πΉ β π) = (πΊ β π) β§ (πβ0) = (π»βπ))) |
97 | 1, 2, 77, 78, 79, 80, 81, 82, 83, 11, 3, 84, 85, 86, 37, 87, 88, 89, 58, 90, 91, 92, 96 | cvmlift3lem6 33982 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β§ (((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦))) β (π»βπ¦) β π) |
98 | 97 | ex 414 |
. . . . . . . . 9
β’ (((π β§ π¦ β π) β§ (β β (II Cn πΎ) β§ π β (II Cn (πΎ βΎt π)))) β ((((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦)) β (π»βπ¦) β π)) |
99 | 98 | rexlimdvva 3202 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β (ββ β (II Cn πΎ)βπ β (II Cn (πΎ βΎt π))(((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ ((πβ0) = π β§ (πβ1) = π¦)) β (π»βπ¦) β π)) |
100 | 76, 99 | biimtrrid 242 |
. . . . . . 7
β’ ((π β§ π¦ β π) β ((ββ β (II Cn πΎ)((ββ0) = π β§ (ββ1) = π β§ ((β©π β (II Cn πΆ)((πΉ β π) = (πΊ β β) β§ (πβ0) = π))β1) = (π»βπ)) β§ βπ β (II Cn (πΎ βΎt π))((πβ0) = π β§ (πβ1) = π¦)) β (π»βπ¦) β π)) |
101 | 64, 75, 100 | mp2and 698 |
. . . . . 6
β’ ((π β§ π¦ β π) β (π»βπ¦) β π) |
102 | 101 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ¦ β π (π»βπ¦) β π) |
103 | 12 | ffund 6676 |
. . . . . 6
β’ (π β Fun π») |
104 | 12 | fdmd 6683 |
. . . . . . 7
β’ (π β dom π» = π) |
105 | 24, 104 | sseqtrrd 3989 |
. . . . . 6
β’ (π β π β dom π») |
106 | | funimass4 6911 |
. . . . . 6
β’ ((Fun
π» β§ π β dom π») β ((π» β π) β π β βπ¦ β π (π»βπ¦) β π)) |
107 | 103, 105,
106 | syl2anc 585 |
. . . . 5
β’ (π β ((π» β π) β π β βπ¦ β π (π»βπ¦) β π)) |
108 | 102, 107 | mpbird 257 |
. . . 4
β’ (π β (π» β π) β π) |
109 | 1, 2, 3, 4, 12, 14, 16, 28, 29, 39, 24, 108 | cvmlift2lem9a 33961 |
. . 3
β’ (π β (π» βΎ π) β ((πΎ βΎt π) Cn πΆ)) |
110 | 73 | cncnpi 22652 |
. . 3
β’ (((π» βΎ π) β ((πΎ βΎt π) Cn πΆ) β§ π β βͺ (πΎ βΎt π)) β (π» βΎ π) β (((πΎ βΎt π) CnP πΆ)βπ)) |
111 | 109, 69, 110 | syl2anc 585 |
. 2
β’ (π β (π» βΎ π) β (((πΎ βΎt π) CnP πΆ)βπ)) |
112 | | cvmlift3lem7.4 |
. . . . 5
β’ (π β π β πΎ) |
113 | 2 | ssntr 22432 |
. . . . 5
β’ (((πΎ β Top β§ π β π) β§ (π β πΎ β§ π β π)) β π β ((intβπΎ)βπ)) |
114 | 16, 24, 112, 25, 113 | syl22anc 838 |
. . . 4
β’ (π β π β ((intβπΎ)βπ)) |
115 | 114, 26 | sseldd 3949 |
. . 3
β’ (π β π β ((intβπΎ)βπ)) |
116 | 2, 1 | cnprest 22663 |
. . 3
β’ (((πΎ β Top β§ π β π) β§ (π β ((intβπΎ)βπ) β§ π»:πβΆπ΅)) β (π» β ((πΎ CnP πΆ)βπ) β (π» βΎ π) β (((πΎ βΎt π) CnP πΆ)βπ))) |
117 | 16, 24, 115, 12, 116 | syl22anc 838 |
. 2
β’ (π β (π» β ((πΎ CnP πΆ)βπ) β (π» βΎ π) β (((πΎ βΎt π) CnP πΆ)βπ))) |
118 | 111, 117 | mpbird 257 |
1
β’ (π β π» β ((πΎ CnP πΆ)βπ)) |