Step | Hyp | Ref
| Expression |
1 | | cvmlift2.b |
. . . 4
β’ π΅ = βͺ
πΆ |
2 | | cvmlift2.f |
. . . 4
β’ (π β πΉ β (πΆ CovMap π½)) |
3 | | cvmlift2.g |
. . . 4
β’ (π β πΊ β ((II Γt II) Cn
π½)) |
4 | | cvmlift2.p |
. . . 4
β’ (π β π β π΅) |
5 | | cvmlift2.i |
. . . 4
β’ (π β (πΉβπ) = (0πΊ0)) |
6 | | cvmlift2.h |
. . . 4
β’ π» = (β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (πβ0) = π)) |
7 | | cvmlift2.k |
. . . 4
β’ πΎ = (π₯ β (0[,]1), π¦ β (0[,]1) β¦ ((β©π β (II Cn πΆ)((πΉ β π) = (π§ β (0[,]1) β¦ (π₯πΊπ§)) β§ (πβ0) = (π»βπ₯)))βπ¦)) |
8 | | fveq2 6891 |
. . . . . 6
β’ (π = π§ β (((II Γt II) CnP
πΆ)βπ) = (((II Γt II) CnP πΆ)βπ§)) |
9 | 8 | eleq2d 2818 |
. . . . 5
β’ (π = π§ β (πΎ β (((II Γt II) CnP
πΆ)βπ) β πΎ β (((II Γt II) CnP
πΆ)βπ§))) |
10 | 9 | cbvrabv 3441 |
. . . 4
β’ {π β ((0[,]1) Γ
(0[,]1)) β£ πΎ β
(((II Γt II) CnP πΆ)βπ)} = {π§ β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ§)} |
11 | | sneq 4638 |
. . . . . . 7
β’ (π§ = π β {π§} = {π}) |
12 | 11 | xpeq2d 5706 |
. . . . . 6
β’ (π§ = π β ((0[,]1) Γ {π§}) = ((0[,]1) Γ {π})) |
13 | 12 | sseq1d 4013 |
. . . . 5
β’ (π§ = π β (((0[,]1) Γ {π§}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β ((0[,]1) Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)})) |
14 | 13 | cbvrabv 3441 |
. . . 4
β’ {π§ β (0[,]1) β£ ((0[,]1)
Γ {π§}) β {π β ((0[,]1) Γ
(0[,]1)) β£ πΎ β
(((II Γt II) CnP πΆ)βπ)}} = {π β (0[,]1) β£ ((0[,]1) Γ
{π}) β {π β ((0[,]1) Γ
(0[,]1)) β£ πΎ β
(((II Γt II) CnP πΆ)βπ)}} |
15 | | simpr 484 |
. . . . . . 7
β’ ((π = π β§ π = π‘) β π = π‘) |
16 | 15 | eleq1d 2817 |
. . . . . 6
β’ ((π = π β§ π = π‘) β (π β (0[,]1) β π‘ β (0[,]1))) |
17 | | xpeq1 5690 |
. . . . . . . . . 10
β’ (π£ = π’ β (π£ Γ {π}) = (π’ Γ {π})) |
18 | 17 | sseq1d 4013 |
. . . . . . . . 9
β’ (π£ = π’ β ((π£ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)})) |
19 | | xpeq1 5690 |
. . . . . . . . . 10
β’ (π£ = π’ β (π£ Γ {π}) = (π’ Γ {π})) |
20 | 19 | sseq1d 4013 |
. . . . . . . . 9
β’ (π£ = π’ β ((π£ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)})) |
21 | 18, 20 | bibi12d 345 |
. . . . . . . 8
β’ (π£ = π’ β (((π£ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π£ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)}) β ((π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)}))) |
22 | 21 | cbvrexvw 3234 |
. . . . . . 7
β’
(βπ£ β
((neiβII)β{π})((π£ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π£ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)}) β βπ’ β ((neiβII)β{π})((π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)})) |
23 | | simpl 482 |
. . . . . . . . . 10
β’ ((π = π β§ π = π‘) β π = π) |
24 | 23 | sneqd 4640 |
. . . . . . . . 9
β’ ((π = π β§ π = π‘) β {π} = {π}) |
25 | 24 | fveq2d 6895 |
. . . . . . . 8
β’ ((π = π β§ π = π‘) β ((neiβII)β{π}) =
((neiβII)β{π})) |
26 | 15 | sneqd 4640 |
. . . . . . . . . . 11
β’ ((π = π β§ π = π‘) β {π} = {π‘}) |
27 | 26 | xpeq2d 5706 |
. . . . . . . . . 10
β’ ((π = π β§ π = π‘) β (π’ Γ {π}) = (π’ Γ {π‘})) |
28 | 27 | sseq1d 4013 |
. . . . . . . . 9
β’ ((π = π β§ π = π‘) β ((π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π’ Γ {π‘}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)})) |
29 | 28 | bibi2d 342 |
. . . . . . . 8
β’ ((π = π β§ π = π‘) β (((π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)}) β ((π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π’ Γ {π‘}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)}))) |
30 | 25, 29 | rexeqbidv 3342 |
. . . . . . 7
β’ ((π = π β§ π = π‘) β (βπ’ β ((neiβII)β{π})((π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)}) β βπ’ β ((neiβII)β{π})((π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π’ Γ {π‘}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)}))) |
31 | 22, 30 | bitrid 283 |
. . . . . 6
β’ ((π = π β§ π = π‘) β (βπ£ β ((neiβII)β{π})((π£ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π£ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)}) β βπ’ β ((neiβII)β{π})((π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π’ Γ {π‘}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)}))) |
32 | 16, 31 | anbi12d 630 |
. . . . 5
β’ ((π = π β§ π = π‘) β ((π β (0[,]1) β§ βπ£ β
((neiβII)β{π})((π£ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π£ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)})) β (π‘ β (0[,]1) β§ βπ’ β
((neiβII)β{π})((π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π’ Γ {π‘}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)})))) |
33 | 32 | cbvopabv 5221 |
. . . 4
β’
{β¨π, πβ© β£ (π β (0[,]1) β§
βπ£ β
((neiβII)β{π})((π£ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π£ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)}))} = {β¨π, π‘β© β£ (π‘ β (0[,]1) β§ βπ’ β
((neiβII)β{π})((π’ Γ {π}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)} β (π’ Γ {π‘}) β {π β ((0[,]1) Γ (0[,]1)) β£
πΎ β (((II
Γt II) CnP πΆ)βπ)}))} |
34 | 1, 2, 3, 4, 5, 6, 7, 10, 14, 33 | cvmlift2lem12 34604 |
. . 3
β’ (π β πΎ β ((II Γt II) Cn
πΆ)) |
35 | 1, 2, 3, 4, 5, 6, 7 | cvmlift2lem7 34599 |
. . 3
β’ (π β (πΉ β πΎ) = πΊ) |
36 | | 0elunit 13451 |
. . . . 5
β’ 0 β
(0[,]1) |
37 | 1, 2, 3, 4, 5, 6, 7 | cvmlift2lem8 34600 |
. . . . 5
β’ ((π β§ 0 β (0[,]1)) β
(0πΎ0) = (π»β0)) |
38 | 36, 37 | mpan2 688 |
. . . 4
β’ (π β (0πΎ0) = (π»β0)) |
39 | 1, 2, 3, 4, 5, 6 | cvmlift2lem2 34594 |
. . . . 5
β’ (π β (π» β (II Cn πΆ) β§ (πΉ β π») = (π§ β (0[,]1) β¦ (π§πΊ0)) β§ (π»β0) = π)) |
40 | 39 | simp3d 1143 |
. . . 4
β’ (π β (π»β0) = π) |
41 | 38, 40 | eqtrd 2771 |
. . 3
β’ (π β (0πΎ0) = π) |
42 | | coeq2 5858 |
. . . . . 6
β’ (π = πΎ β (πΉ β π) = (πΉ β πΎ)) |
43 | 42 | eqeq1d 2733 |
. . . . 5
β’ (π = πΎ β ((πΉ β π) = πΊ β (πΉ β πΎ) = πΊ)) |
44 | | oveq 7418 |
. . . . . 6
β’ (π = πΎ β (0π0) = (0πΎ0)) |
45 | 44 | eqeq1d 2733 |
. . . . 5
β’ (π = πΎ β ((0π0) = π β (0πΎ0) = π)) |
46 | 43, 45 | anbi12d 630 |
. . . 4
β’ (π = πΎ β (((πΉ β π) = πΊ β§ (0π0) = π) β ((πΉ β πΎ) = πΊ β§ (0πΎ0) = π))) |
47 | 46 | rspcev 3612 |
. . 3
β’ ((πΎ β ((II Γt
II) Cn πΆ) β§ ((πΉ β πΎ) = πΊ β§ (0πΎ0) = π)) β βπ β ((II Γt II) Cn πΆ)((πΉ β π) = πΊ β§ (0π0) = π)) |
48 | 34, 35, 41, 47 | syl12anc 834 |
. 2
β’ (π β βπ β ((II Γt II) Cn πΆ)((πΉ β π) = πΊ β§ (0π0) = π)) |
49 | | iitop 24621 |
. . . . 5
β’ II β
Top |
50 | | iiuni 24622 |
. . . . 5
β’ (0[,]1) =
βͺ II |
51 | 49, 49, 50, 50 | txunii 23318 |
. . . 4
β’ ((0[,]1)
Γ (0[,]1)) = βͺ (II Γt
II) |
52 | | iiconn 24628 |
. . . . . 6
β’ II β
Conn |
53 | | txconn 23414 |
. . . . . 6
β’ ((II
β Conn β§ II β Conn) β (II Γt II) β
Conn) |
54 | 52, 52, 53 | mp2an 689 |
. . . . 5
β’ (II
Γt II) β Conn |
55 | 54 | a1i 11 |
. . . 4
β’ (π β (II Γt
II) β Conn) |
56 | | iinllyconn 34544 |
. . . . . 6
β’ II β
π-Locally Conn |
57 | | txconn 23414 |
. . . . . . 7
β’ ((π₯ β Conn β§ π¦ β Conn) β (π₯ Γt π¦) β Conn) |
58 | 57 | txnlly 23362 |
. . . . . 6
β’ ((II
β π-Locally Conn β§ II β π-Locally Conn) β
(II Γt II) β π-Locally Conn) |
59 | 56, 56, 58 | mp2an 689 |
. . . . 5
β’ (II
Γt II) β π-Locally Conn |
60 | 59 | a1i 11 |
. . . 4
β’ (π β (II Γt
II) β π-Locally Conn) |
61 | | opelxpi 5713 |
. . . . . 6
β’ ((0
β (0[,]1) β§ 0 β (0[,]1)) β β¨0, 0β© β ((0[,]1)
Γ (0[,]1))) |
62 | 36, 36, 61 | mp2an 689 |
. . . . 5
β’ β¨0,
0β© β ((0[,]1) Γ (0[,]1)) |
63 | 62 | a1i 11 |
. . . 4
β’ (π β β¨0, 0β© β
((0[,]1) Γ (0[,]1))) |
64 | | df-ov 7415 |
. . . . 5
β’ (0πΊ0) = (πΊββ¨0, 0β©) |
65 | 5, 64 | eqtrdi 2787 |
. . . 4
β’ (π β (πΉβπ) = (πΊββ¨0, 0β©)) |
66 | 1, 51, 2, 55, 60, 63, 3, 4, 65 | cvmliftmo 34574 |
. . 3
β’ (π β β*π β ((II Γt II) Cn πΆ)((πΉ β π) = πΊ β§ (πββ¨0, 0β©) = π)) |
67 | | df-ov 7415 |
. . . . . 6
β’ (0π0) = (πββ¨0, 0β©) |
68 | 67 | eqeq1i 2736 |
. . . . 5
β’ ((0π0) = π β (πββ¨0, 0β©) = π) |
69 | 68 | anbi2i 622 |
. . . 4
β’ (((πΉ β π) = πΊ β§ (0π0) = π) β ((πΉ β π) = πΊ β§ (πββ¨0, 0β©) = π)) |
70 | 69 | rmobii 3383 |
. . 3
β’
(β*π β
((II Γt II) Cn πΆ)((πΉ β π) = πΊ β§ (0π0) = π) β β*π β ((II Γt II) Cn πΆ)((πΉ β π) = πΊ β§ (πββ¨0, 0β©) = π)) |
71 | 66, 70 | sylibr 233 |
. 2
β’ (π β β*π β ((II Γt II) Cn πΆ)((πΉ β π) = πΊ β§ (0π0) = π)) |
72 | | reu5 3377 |
. 2
β’
(β!π β
((II Γt II) Cn πΆ)((πΉ β π) = πΊ β§ (0π0) = π) β (βπ β ((II Γt II) Cn πΆ)((πΉ β π) = πΊ β§ (0π0) = π) β§ β*π β ((II Γt II) Cn πΆ)((πΉ β π) = πΊ β§ (0π0) = π))) |
73 | 48, 71, 72 | sylanbrc 582 |
1
β’ (π β β!π β ((II Γt II) Cn πΆ)((πΉ β π) = πΊ β§ (0π0) = π)) |