Step | Hyp | Ref
| Expression |
1 | | sconntop 34219 |
. . . . . . . . 9
β’ (π½ β SConn β π½ β Top) |
2 | 1 | adantl 483 |
. . . . . . . 8
β’ ((π β π β§ π½ β SConn) β π½ β Top) |
3 | | simpl 484 |
. . . . . . . 8
β’ ((π β π β§ π½ β SConn) β π β π) |
4 | | eqid 2733 |
. . . . . . . . 9
β’ (π½ Ο1 π) = (π½ Ο1 π) |
5 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβ(π½
Ο1 π)) =
(Baseβ(π½
Ο1 π)) |
6 | | simpl 484 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π β π) β π½ β Top) |
7 | | sconnpi1.1 |
. . . . . . . . . . 11
β’ π = βͺ
π½ |
8 | 7 | toptopon 22419 |
. . . . . . . . . 10
β’ (π½ β Top β π½ β (TopOnβπ)) |
9 | 6, 8 | sylib 217 |
. . . . . . . . 9
β’ ((π½ β Top β§ π β π) β π½ β (TopOnβπ)) |
10 | | simpr 486 |
. . . . . . . . 9
β’ ((π½ β Top β§ π β π) β π β π) |
11 | 4, 5, 9, 10 | elpi1 24561 |
. . . . . . . 8
β’ ((π½ β Top β§ π β π) β (π₯ β (Baseβ(π½ Ο1 π)) β βπ β (II Cn π½)(((πβ0) = π β§ (πβ1) = π) β§ π₯ = [π]( βphβπ½)))) |
12 | 2, 3, 11 | syl2anc 585 |
. . . . . . 7
β’ ((π β π β§ π½ β SConn) β (π₯ β (Baseβ(π½ Ο1 π)) β βπ β (II Cn π½)(((πβ0) = π β§ (πβ1) = π) β§ π₯ = [π]( βphβπ½)))) |
13 | | phtpcer 24511 |
. . . . . . . . . . . . 13
β’ (
βphβπ½) Er (II Cn π½) |
14 | 13 | a1i 11 |
. . . . . . . . . . . 12
β’ ((((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β§ ((πβ0) = π β§ (πβ1) = π)) β (
βphβπ½) Er (II Cn π½)) |
15 | | simpllr 775 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β§ ((πβ0) = π β§ (πβ1) = π)) β π½ β SConn) |
16 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β§ ((πβ0) = π β§ (πβ1) = π)) β π β (II Cn π½)) |
17 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ ((((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β§ ((πβ0) = π β§ (πβ1) = π)) β (πβ0) = π) |
18 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ ((((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β§ ((πβ0) = π β§ (πβ1) = π)) β (πβ1) = π) |
19 | 17, 18 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β§ ((πβ0) = π β§ (πβ1) = π)) β (πβ0) = (πβ1)) |
20 | | sconnpht 34220 |
. . . . . . . . . . . . . 14
β’ ((π½ β SConn β§ π β (II Cn π½) β§ (πβ0) = (πβ1)) β π( βphβπ½)((0[,]1) Γ {(πβ0)})) |
21 | 15, 16, 19, 20 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β§ ((πβ0) = π β§ (πβ1) = π)) β π( βphβπ½)((0[,]1) Γ {(πβ0)})) |
22 | 17 | sneqd 4641 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β§ ((πβ0) = π β§ (πβ1) = π)) β {(πβ0)} = {π}) |
23 | 22 | xpeq2d 5707 |
. . . . . . . . . . . . 13
β’ ((((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β§ ((πβ0) = π β§ (πβ1) = π)) β ((0[,]1) Γ {(πβ0)}) = ((0[,]1) Γ
{π})) |
24 | 21, 23 | breqtrd 5175 |
. . . . . . . . . . . 12
β’ ((((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β§ ((πβ0) = π β§ (πβ1) = π)) β π( βphβπ½)((0[,]1) Γ {π})) |
25 | 14, 24 | erthi 8754 |
. . . . . . . . . . 11
β’ ((((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β§ ((πβ0) = π β§ (πβ1) = π)) β [π]( βphβπ½) = [((0[,]1) Γ {π})](
βphβπ½)) |
26 | 2, 8 | sylib 217 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π½ β SConn) β π½ β (TopOnβπ)) |
27 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ ((0[,]1)
Γ {π}) = ((0[,]1)
Γ {π}) |
28 | 4, 27 | pi1id 24567 |
. . . . . . . . . . . . 13
β’ ((π½ β (TopOnβπ) β§ π β π) β [((0[,]1) Γ {π})](
βphβπ½) = (0gβ(π½ Ο1 π))) |
29 | 26, 3, 28 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β π β§ π½ β SConn) β [((0[,]1) Γ
{π})](
βphβπ½) = (0gβ(π½ Ο1 π))) |
30 | 29 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β§ ((πβ0) = π β§ (πβ1) = π)) β [((0[,]1) Γ {π})](
βphβπ½) = (0gβ(π½ Ο1 π))) |
31 | 25, 30 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β§ ((πβ0) = π β§ (πβ1) = π)) β [π]( βphβπ½) = (0gβ(π½ Ο1 π))) |
32 | | velsn 4645 |
. . . . . . . . . . 11
β’ (π₯ β
{(0gβ(π½
Ο1 π))}
β π₯ =
(0gβ(π½
Ο1 π))) |
33 | | eqeq1 2737 |
. . . . . . . . . . 11
β’ (π₯ = [π]( βphβπ½) β (π₯ = (0gβ(π½ Ο1 π)) β [π]( βphβπ½) = (0gβ(π½ Ο1 π)))) |
34 | 32, 33 | bitrid 283 |
. . . . . . . . . 10
β’ (π₯ = [π]( βphβπ½) β (π₯ β {(0gβ(π½ Ο1 π))} β [π]( βphβπ½) = (0gβ(π½ Ο1 π)))) |
35 | 31, 34 | syl5ibrcom 246 |
. . . . . . . . 9
β’ ((((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β§ ((πβ0) = π β§ (πβ1) = π)) β (π₯ = [π]( βphβπ½) β π₯ β {(0gβ(π½ Ο1 π))})) |
36 | 35 | expimpd 455 |
. . . . . . . 8
β’ (((π β π β§ π½ β SConn) β§ π β (II Cn π½)) β ((((πβ0) = π β§ (πβ1) = π) β§ π₯ = [π]( βphβπ½)) β π₯ β {(0gβ(π½ Ο1 π))})) |
37 | 36 | rexlimdva 3156 |
. . . . . . 7
β’ ((π β π β§ π½ β SConn) β (βπ β (II Cn π½)(((πβ0) = π β§ (πβ1) = π) β§ π₯ = [π]( βphβπ½)) β π₯ β {(0gβ(π½ Ο1 π))})) |
38 | 12, 37 | sylbid 239 |
. . . . . 6
β’ ((π β π β§ π½ β SConn) β (π₯ β (Baseβ(π½ Ο1 π)) β π₯ β {(0gβ(π½ Ο1 π))})) |
39 | 38 | ssrdv 3989 |
. . . . 5
β’ ((π β π β§ π½ β SConn) β (Baseβ(π½ Ο1 π)) β
{(0gβ(π½
Ο1 π))}) |
40 | 4 | pi1grp 24566 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π β π) β (π½ Ο1 π) β Grp) |
41 | 26, 3, 40 | syl2anc 585 |
. . . . . . 7
β’ ((π β π β§ π½ β SConn) β (π½ Ο1 π) β Grp) |
42 | | eqid 2733 |
. . . . . . . 8
β’
(0gβ(π½ Ο1 π)) = (0gβ(π½ Ο1 π)) |
43 | 5, 42 | grpidcl 18850 |
. . . . . . 7
β’ ((π½ Ο1 π) β Grp β
(0gβ(π½
Ο1 π)) β
(Baseβ(π½
Ο1 π))) |
44 | 41, 43 | syl 17 |
. . . . . 6
β’ ((π β π β§ π½ β SConn) β
(0gβ(π½
Ο1 π)) β
(Baseβ(π½
Ο1 π))) |
45 | 44 | snssd 4813 |
. . . . 5
β’ ((π β π β§ π½ β SConn) β
{(0gβ(π½
Ο1 π))}
β (Baseβ(π½
Ο1 π))) |
46 | 39, 45 | eqssd 4000 |
. . . 4
β’ ((π β π β§ π½ β SConn) β (Baseβ(π½ Ο1 π)) =
{(0gβ(π½
Ο1 π))}) |
47 | | fvex 6905 |
. . . . 5
β’
(0gβ(π½ Ο1 π)) β V |
48 | 47 | ensn1 9017 |
. . . 4
β’
{(0gβ(π½ Ο1 π))} β 1o |
49 | 46, 48 | eqbrtrdi 5188 |
. . 3
β’ ((π β π β§ π½ β SConn) β (Baseβ(π½ Ο1 π)) β
1o) |
50 | 49 | adantll 713 |
. 2
β’ (((π½ β PConn β§ π β π) β§ π½ β SConn) β (Baseβ(π½ Ο1 π)) β
1o) |
51 | | simpll 766 |
. . 3
β’ (((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β π½ β PConn) |
52 | | eqid 2733 |
. . . . . . . . 9
β’ (π½ Ο1 (πβ0)) = (π½ Ο1 (πβ0)) |
53 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβ(π½
Ο1 (πβ0))) = (Baseβ(π½ Ο1 (πβ0))) |
54 | | simplll 774 |
. . . . . . . . . . 11
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β π½ β PConn) |
55 | | pconntop 34216 |
. . . . . . . . . . 11
β’ (π½ β PConn β π½ β Top) |
56 | 54, 55 | syl 17 |
. . . . . . . . . 10
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β π½ β Top) |
57 | 56, 8 | sylib 217 |
. . . . . . . . 9
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β π½ β (TopOnβπ)) |
58 | | simprl 770 |
. . . . . . . . . . 11
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β π β (II Cn π½)) |
59 | | iiuni 24397 |
. . . . . . . . . . . 12
β’ (0[,]1) =
βͺ II |
60 | 59, 7 | cnf 22750 |
. . . . . . . . . . 11
β’ (π β (II Cn π½) β π:(0[,]1)βΆπ) |
61 | 58, 60 | syl 17 |
. . . . . . . . . 10
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β π:(0[,]1)βΆπ) |
62 | | 0elunit 13446 |
. . . . . . . . . 10
β’ 0 β
(0[,]1) |
63 | | ffvelcdm 7084 |
. . . . . . . . . 10
β’ ((π:(0[,]1)βΆπ β§ 0 β (0[,]1)) β
(πβ0) β π) |
64 | 61, 62, 63 | sylancl 587 |
. . . . . . . . 9
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β (πβ0) β π) |
65 | | eqidd 2734 |
. . . . . . . . 9
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β (πβ0) = (πβ0)) |
66 | | simprr 772 |
. . . . . . . . . 10
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β (πβ0) = (πβ1)) |
67 | 66 | eqcomd 2739 |
. . . . . . . . 9
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β (πβ1) = (πβ0)) |
68 | 52, 53, 57, 64, 58, 65, 67 | elpi1i 24562 |
. . . . . . . 8
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β [π]( βphβπ½) β (Baseβ(π½ Ο1 (πβ0)))) |
69 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ ((0[,]1)
Γ {(πβ0)}) =
((0[,]1) Γ {(πβ0)}) |
70 | 69 | pcoptcl 24537 |
. . . . . . . . . . . 12
β’ ((π½ β (TopOnβπ) β§ (πβ0) β π) β (((0[,]1) Γ {(πβ0)}) β (II Cn π½) β§ (((0[,]1) Γ
{(πβ0)})β0) =
(πβ0) β§ (((0[,]1)
Γ {(πβ0)})β1) = (πβ0))) |
71 | 57, 64, 70 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β (((0[,]1) Γ {(πβ0)}) β (II Cn π½) β§ (((0[,]1) Γ
{(πβ0)})β0) =
(πβ0) β§ (((0[,]1)
Γ {(πβ0)})β1) = (πβ0))) |
72 | 71 | simp1d 1143 |
. . . . . . . . . 10
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β ((0[,]1) Γ {(πβ0)}) β (II Cn π½)) |
73 | 71 | simp2d 1144 |
. . . . . . . . . 10
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β (((0[,]1) Γ {(πβ0)})β0) = (πβ0)) |
74 | 71 | simp3d 1145 |
. . . . . . . . . 10
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β (((0[,]1) Γ {(πβ0)})β1) = (πβ0)) |
75 | 52, 53, 57, 64, 72, 73, 74 | elpi1i 24562 |
. . . . . . . . 9
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β [((0[,]1) Γ {(πβ0)})](
βphβπ½) β (Baseβ(π½ Ο1 (πβ0)))) |
76 | | simpllr 775 |
. . . . . . . . . . . 12
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β π β π) |
77 | 7, 52, 4, 53, 5 | pconnpi1 34228 |
. . . . . . . . . . . 12
β’ ((π½ β PConn β§ (πβ0) β π β§ π β π) β (π½ Ο1 (πβ0)) βπ (π½ Ο1 π)) |
78 | 54, 64, 76, 77 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β (π½ Ο1 (πβ0)) βπ (π½ Ο1 π)) |
79 | 53, 5 | gicen 19151 |
. . . . . . . . . . 11
β’ ((π½ Ο1 (πβ0))
βπ (π½ Ο1 π) β (Baseβ(π½ Ο1 (πβ0))) β (Baseβ(π½ Ο1 π))) |
80 | 78, 79 | syl 17 |
. . . . . . . . . 10
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β (Baseβ(π½ Ο1 (πβ0))) β
(Baseβ(π½
Ο1 π))) |
81 | | simplr 768 |
. . . . . . . . . 10
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β (Baseβ(π½ Ο1 π)) β
1o) |
82 | | entr 9002 |
. . . . . . . . . 10
β’
(((Baseβ(π½
Ο1 (πβ0))) β (Baseβ(π½ Ο1 π)) β§ (Baseβ(π½ Ο1 π)) β 1o) β
(Baseβ(π½
Ο1 (πβ0))) β
1o) |
83 | 80, 81, 82 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β (Baseβ(π½ Ο1 (πβ0))) β
1o) |
84 | | en1eqsn 9274 |
. . . . . . . . 9
β’
(([((0[,]1) Γ {(πβ0)})](
βphβπ½) β (Baseβ(π½ Ο1 (πβ0))) β§ (Baseβ(π½ Ο1 (πβ0))) β
1o) β (Baseβ(π½ Ο1 (πβ0))) = {[((0[,]1) Γ {(πβ0)})](
βphβπ½)}) |
85 | 75, 83, 84 | syl2anc 585 |
. . . . . . . 8
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β (Baseβ(π½ Ο1 (πβ0))) = {[((0[,]1) Γ
{(πβ0)})](
βphβπ½)}) |
86 | 68, 85 | eleqtrd 2836 |
. . . . . . 7
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β [π]( βphβπ½) β {[((0[,]1) Γ
{(πβ0)})](
βphβπ½)}) |
87 | | elsni 4646 |
. . . . . . 7
β’ ([π](
βphβπ½) β {[((0[,]1) Γ {(πβ0)})](
βphβπ½)} β [π]( βphβπ½) = [((0[,]1) Γ {(πβ0)})](
βphβπ½)) |
88 | 86, 87 | syl 17 |
. . . . . 6
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β [π]( βphβπ½) = [((0[,]1) Γ {(πβ0)})](
βphβπ½)) |
89 | 13 | a1i 11 |
. . . . . . 7
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β (
βphβπ½) Er (II Cn π½)) |
90 | 89, 58 | erth 8752 |
. . . . . 6
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β (π( βphβπ½)((0[,]1) Γ {(πβ0)}) β [π](
βphβπ½) = [((0[,]1) Γ {(πβ0)})](
βphβπ½))) |
91 | 88, 90 | mpbird 257 |
. . . . 5
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ (π β (II Cn π½) β§ (πβ0) = (πβ1))) β π( βphβπ½)((0[,]1) Γ {(πβ0)})) |
92 | 91 | expr 458 |
. . . 4
β’ ((((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β§ π β (II Cn π½)) β ((πβ0) = (πβ1) β π( βphβπ½)((0[,]1) Γ {(πβ0)}))) |
93 | 92 | ralrimiva 3147 |
. . 3
β’ (((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β
βπ β (II Cn
π½)((πβ0) = (πβ1) β π( βphβπ½)((0[,]1) Γ {(πβ0)}))) |
94 | | issconn 34217 |
. . 3
β’ (π½ β SConn β (π½ β PConn β§
βπ β (II Cn
π½)((πβ0) = (πβ1) β π( βphβπ½)((0[,]1) Γ {(πβ0)})))) |
95 | 51, 93, 94 | sylanbrc 584 |
. 2
β’ (((π½ β PConn β§ π β π) β§ (Baseβ(π½ Ο1 π)) β 1o) β π½ β SConn) |
96 | 50, 95 | impbida 800 |
1
β’ ((π½ β PConn β§ π β π) β (π½ β SConn β (Baseβ(π½ Ο1 π)) β
1o)) |