Step | Hyp | Ref
| Expression |
1 | | htpyco2.f |
. . . 4
β’ (π β πΉ β (π½ Cn πΎ)) |
2 | | cntop1 22735 |
. . . 4
β’ (πΉ β (π½ Cn πΎ) β π½ β Top) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β π½ β Top) |
4 | | toptopon2 22411 |
. . 3
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
5 | 3, 4 | sylib 217 |
. 2
β’ (π β π½ β (TopOnββͺ π½)) |
6 | | htpyco2.p |
. . 3
β’ (π β π β (πΎ Cn πΏ)) |
7 | | cnco 22761 |
. . 3
β’ ((πΉ β (π½ Cn πΎ) β§ π β (πΎ Cn πΏ)) β (π β πΉ) β (π½ Cn πΏ)) |
8 | 1, 6, 7 | syl2anc 584 |
. 2
β’ (π β (π β πΉ) β (π½ Cn πΏ)) |
9 | | htpyco2.g |
. . 3
β’ (π β πΊ β (π½ Cn πΎ)) |
10 | | cnco 22761 |
. . 3
β’ ((πΊ β (π½ Cn πΎ) β§ π β (πΎ Cn πΏ)) β (π β πΊ) β (π½ Cn πΏ)) |
11 | 9, 6, 10 | syl2anc 584 |
. 2
β’ (π β (π β πΊ) β (π½ Cn πΏ)) |
12 | 5, 1, 9 | htpycn 24480 |
. . . 4
β’ (π β (πΉ(π½ Htpy πΎ)πΊ) β ((π½ Γt II) Cn πΎ)) |
13 | | htpyco2.h |
. . . 4
β’ (π β π» β (πΉ(π½ Htpy πΎ)πΊ)) |
14 | 12, 13 | sseldd 3982 |
. . 3
β’ (π β π» β ((π½ Γt II) Cn πΎ)) |
15 | | cnco 22761 |
. . 3
β’ ((π» β ((π½ Γt II) Cn πΎ) β§ π β (πΎ Cn πΏ)) β (π β π») β ((π½ Γt II) Cn πΏ)) |
16 | 14, 6, 15 | syl2anc 584 |
. 2
β’ (π β (π β π») β ((π½ Γt II) Cn πΏ)) |
17 | 5, 1, 9, 13 | htpyi 24481 |
. . . . 5
β’ ((π β§ π β βͺ π½) β ((π π»0) = (πΉβπ ) β§ (π π»1) = (πΊβπ ))) |
18 | 17 | simpld 495 |
. . . 4
β’ ((π β§ π β βͺ π½) β (π π»0) = (πΉβπ )) |
19 | 18 | fveq2d 6892 |
. . 3
β’ ((π β§ π β βͺ π½) β (πβ(π π»0)) = (πβ(πΉβπ ))) |
20 | | iitopon 24386 |
. . . . . . 7
β’ II β
(TopOnβ(0[,]1)) |
21 | | txtopon 23086 |
. . . . . . 7
β’ ((π½ β (TopOnββͺ π½)
β§ II β (TopOnβ(0[,]1))) β (π½ Γt II) β
(TopOnβ(βͺ π½ Γ (0[,]1)))) |
22 | 5, 20, 21 | sylancl 586 |
. . . . . 6
β’ (π β (π½ Γt II) β
(TopOnβ(βͺ π½ Γ (0[,]1)))) |
23 | | cntop2 22736 |
. . . . . . . 8
β’ (πΉ β (π½ Cn πΎ) β πΎ β Top) |
24 | 1, 23 | syl 17 |
. . . . . . 7
β’ (π β πΎ β Top) |
25 | | toptopon2 22411 |
. . . . . . 7
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
26 | 24, 25 | sylib 217 |
. . . . . 6
β’ (π β πΎ β (TopOnββͺ πΎ)) |
27 | | cnf2 22744 |
. . . . . 6
β’ (((π½ Γt II) β
(TopOnβ(βͺ π½ Γ (0[,]1))) β§ πΎ β (TopOnββͺ πΎ)
β§ π» β ((π½ Γt II) Cn
πΎ)) β π»:(βͺ
π½ Γ
(0[,]1))βΆβͺ πΎ) |
28 | 22, 26, 14, 27 | syl3anc 1371 |
. . . . 5
β’ (π β π»:(βͺ π½ Γ (0[,]1))βΆβͺ πΎ) |
29 | | simpr 485 |
. . . . . 6
β’ ((π β§ π β βͺ π½) β π β βͺ π½) |
30 | | 0elunit 13442 |
. . . . . 6
β’ 0 β
(0[,]1) |
31 | | opelxpi 5712 |
. . . . . 6
β’ ((π β βͺ π½
β§ 0 β (0[,]1)) β β¨π , 0β© β (βͺ π½
Γ (0[,]1))) |
32 | 29, 30, 31 | sylancl 586 |
. . . . 5
β’ ((π β§ π β βͺ π½) β β¨π , 0β© β (βͺ π½
Γ (0[,]1))) |
33 | | fvco3 6987 |
. . . . 5
β’ ((π»:(βͺ
π½ Γ
(0[,]1))βΆβͺ πΎ β§ β¨π , 0β© β (βͺ π½
Γ (0[,]1))) β ((π β π»)ββ¨π , 0β©) = (πβ(π»ββ¨π , 0β©))) |
34 | 28, 32, 33 | syl2an2r 683 |
. . . 4
β’ ((π β§ π β βͺ π½) β ((π β π»)ββ¨π , 0β©) = (πβ(π»ββ¨π , 0β©))) |
35 | | df-ov 7408 |
. . . 4
β’ (π (π β π»)0) = ((π β π»)ββ¨π , 0β©) |
36 | | df-ov 7408 |
. . . . 5
β’ (π π»0) = (π»ββ¨π , 0β©) |
37 | 36 | fveq2i 6891 |
. . . 4
β’ (πβ(π π»0)) = (πβ(π»ββ¨π , 0β©)) |
38 | 34, 35, 37 | 3eqtr4g 2797 |
. . 3
β’ ((π β§ π β βͺ π½) β (π (π β π»)0) = (πβ(π π»0))) |
39 | | eqid 2732 |
. . . . . 6
β’ βͺ π½ =
βͺ π½ |
40 | | eqid 2732 |
. . . . . 6
β’ βͺ πΎ =
βͺ πΎ |
41 | 39, 40 | cnf 22741 |
. . . . 5
β’ (πΉ β (π½ Cn πΎ) β πΉ:βͺ π½βΆβͺ πΎ) |
42 | 1, 41 | syl 17 |
. . . 4
β’ (π β πΉ:βͺ π½βΆβͺ πΎ) |
43 | | fvco3 6987 |
. . . 4
β’ ((πΉ:βͺ
π½βΆβͺ πΎ
β§ π β βͺ π½)
β ((π β πΉ)βπ ) = (πβ(πΉβπ ))) |
44 | 42, 43 | sylan 580 |
. . 3
β’ ((π β§ π β βͺ π½) β ((π β πΉ)βπ ) = (πβ(πΉβπ ))) |
45 | 19, 38, 44 | 3eqtr4d 2782 |
. 2
β’ ((π β§ π β βͺ π½) β (π (π β π»)0) = ((π β πΉ)βπ )) |
46 | 17 | simprd 496 |
. . . 4
β’ ((π β§ π β βͺ π½) β (π π»1) = (πΊβπ )) |
47 | 46 | fveq2d 6892 |
. . 3
β’ ((π β§ π β βͺ π½) β (πβ(π π»1)) = (πβ(πΊβπ ))) |
48 | | 1elunit 13443 |
. . . . . 6
β’ 1 β
(0[,]1) |
49 | | opelxpi 5712 |
. . . . . 6
β’ ((π β βͺ π½
β§ 1 β (0[,]1)) β β¨π , 1β© β (βͺ π½
Γ (0[,]1))) |
50 | 29, 48, 49 | sylancl 586 |
. . . . 5
β’ ((π β§ π β βͺ π½) β β¨π , 1β© β (βͺ π½
Γ (0[,]1))) |
51 | | fvco3 6987 |
. . . . 5
β’ ((π»:(βͺ
π½ Γ
(0[,]1))βΆβͺ πΎ β§ β¨π , 1β© β (βͺ π½
Γ (0[,]1))) β ((π β π»)ββ¨π , 1β©) = (πβ(π»ββ¨π , 1β©))) |
52 | 28, 50, 51 | syl2an2r 683 |
. . . 4
β’ ((π β§ π β βͺ π½) β ((π β π»)ββ¨π , 1β©) = (πβ(π»ββ¨π , 1β©))) |
53 | | df-ov 7408 |
. . . 4
β’ (π (π β π»)1) = ((π β π»)ββ¨π , 1β©) |
54 | | df-ov 7408 |
. . . . 5
β’ (π π»1) = (π»ββ¨π , 1β©) |
55 | 54 | fveq2i 6891 |
. . . 4
β’ (πβ(π π»1)) = (πβ(π»ββ¨π , 1β©)) |
56 | 52, 53, 55 | 3eqtr4g 2797 |
. . 3
β’ ((π β§ π β βͺ π½) β (π (π β π»)1) = (πβ(π π»1))) |
57 | 39, 40 | cnf 22741 |
. . . . 5
β’ (πΊ β (π½ Cn πΎ) β πΊ:βͺ π½βΆβͺ πΎ) |
58 | 9, 57 | syl 17 |
. . . 4
β’ (π β πΊ:βͺ π½βΆβͺ πΎ) |
59 | | fvco3 6987 |
. . . 4
β’ ((πΊ:βͺ
π½βΆβͺ πΎ
β§ π β βͺ π½)
β ((π β πΊ)βπ ) = (πβ(πΊβπ ))) |
60 | 58, 59 | sylan 580 |
. . 3
β’ ((π β§ π β βͺ π½) β ((π β πΊ)βπ ) = (πβ(πΊβπ ))) |
61 | 47, 56, 60 | 3eqtr4d 2782 |
. 2
β’ ((π β§ π β βͺ π½) β (π (π β π»)1) = ((π β πΊ)βπ )) |
62 | 5, 8, 11, 16, 45, 61 | ishtpyd 24482 |
1
β’ (π β (π β π») β ((π β πΉ)(π½ Htpy πΏ)(π β πΊ))) |