Step | Hyp | Ref
| Expression |
1 | | simpl3 1194 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ π₯ β π) β π΅ β π΄) |
2 | | ptrescn.2 |
. . . . . . . . . 10
β’ π½ =
(βtβπΉ) |
3 | 2 | ptuni 23098 |
. . . . . . . . 9
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β Xπ β
π΄ βͺ (πΉβπ) = βͺ π½) |
4 | 3 | 3adant3 1133 |
. . . . . . . 8
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β Xπ β π΄ βͺ (πΉβπ) = βͺ π½) |
5 | | ptrescn.1 |
. . . . . . . 8
β’ π = βͺ
π½ |
6 | 4, 5 | eqtr4di 2791 |
. . . . . . 7
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β Xπ β π΄ βͺ (πΉβπ) = π) |
7 | 6 | eleq2d 2820 |
. . . . . 6
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β (π₯ β Xπ β π΄ βͺ (πΉβπ) β π₯ β π)) |
8 | 7 | biimpar 479 |
. . . . 5
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ π₯ β π) β π₯ β Xπ β π΄ βͺ (πΉβπ)) |
9 | | resixp 8927 |
. . . . 5
β’ ((π΅ β π΄ β§ π₯ β Xπ β π΄ βͺ (πΉβπ)) β (π₯ βΎ π΅) β Xπ β π΅ βͺ (πΉβπ)) |
10 | 1, 8, 9 | syl2anc 585 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ π₯ β π) β (π₯ βΎ π΅) β Xπ β π΅ βͺ (πΉβπ)) |
11 | | ixpeq2 8905 |
. . . . . . 7
β’
(βπ β
π΅ βͺ ((πΉ
βΎ π΅)βπ) = βͺ
(πΉβπ) β Xπ β π΅ βͺ ((πΉ βΎ π΅)βπ) = Xπ β π΅ βͺ (πΉβπ)) |
12 | | fvres 6911 |
. . . . . . . 8
β’ (π β π΅ β ((πΉ βΎ π΅)βπ) = (πΉβπ)) |
13 | 12 | unieqd 4923 |
. . . . . . 7
β’ (π β π΅ β βͺ ((πΉ βΎ π΅)βπ) = βͺ (πΉβπ)) |
14 | 11, 13 | mprg 3068 |
. . . . . 6
β’ Xπ β
π΅ βͺ ((πΉ
βΎ π΅)βπ) = Xπ β
π΅ βͺ (πΉβπ) |
15 | | ssexg 5324 |
. . . . . . . . 9
β’ ((π΅ β π΄ β§ π΄ β π) β π΅ β V) |
16 | 15 | ancoms 460 |
. . . . . . . 8
β’ ((π΄ β π β§ π΅ β π΄) β π΅ β V) |
17 | 16 | 3adant2 1132 |
. . . . . . 7
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β π΅ β V) |
18 | | fssres 6758 |
. . . . . . . 8
β’ ((πΉ:π΄βΆTop β§ π΅ β π΄) β (πΉ βΎ π΅):π΅βΆTop) |
19 | 18 | 3adant1 1131 |
. . . . . . 7
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β (πΉ βΎ π΅):π΅βΆTop) |
20 | | ptrescn.3 |
. . . . . . . 8
β’ πΎ =
(βtβ(πΉ βΎ π΅)) |
21 | 20 | ptuni 23098 |
. . . . . . 7
β’ ((π΅ β V β§ (πΉ βΎ π΅):π΅βΆTop) β Xπ β
π΅ βͺ ((πΉ
βΎ π΅)βπ) = βͺ
πΎ) |
22 | 17, 19, 21 | syl2anc 585 |
. . . . . 6
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β Xπ β π΅ βͺ ((πΉ βΎ π΅)βπ) = βͺ πΎ) |
23 | 14, 22 | eqtr3id 2787 |
. . . . 5
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β Xπ β π΅ βͺ (πΉβπ) = βͺ πΎ) |
24 | 23 | adantr 482 |
. . . 4
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ π₯ β π) β Xπ β π΅ βͺ (πΉβπ) = βͺ πΎ) |
25 | 10, 24 | eleqtrd 2836 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ π₯ β π) β (π₯ βΎ π΅) β βͺ πΎ) |
26 | 25 | fmpttd 7115 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β (π₯ β π β¦ (π₯ βΎ π΅)):πβΆβͺ πΎ) |
27 | | fimacnv 6740 |
. . . . . . 7
β’ ((π₯ β π β¦ (π₯ βΎ π΅)):πβΆβͺ πΎ β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β βͺ
πΎ) = π) |
28 | 26, 27 | syl 17 |
. . . . . 6
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β βͺ
πΎ) = π) |
29 | | pttop 23086 |
. . . . . . . . 9
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β
(βtβπΉ) β Top) |
30 | 2, 29 | eqeltrid 2838 |
. . . . . . . 8
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β π½ β Top) |
31 | 30 | 3adant3 1133 |
. . . . . . 7
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β π½ β Top) |
32 | 5 | topopn 22408 |
. . . . . . 7
β’ (π½ β Top β π β π½) |
33 | 31, 32 | syl 17 |
. . . . . 6
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β π β π½) |
34 | 28, 33 | eqeltrd 2834 |
. . . . 5
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β βͺ
πΎ) β π½) |
35 | | elsni 4646 |
. . . . . . 7
β’ (π£ β {βͺ πΎ}
β π£ = βͺ πΎ) |
36 | 35 | imaeq2d 6060 |
. . . . . 6
β’ (π£ β {βͺ πΎ}
β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) = (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β βͺ
πΎ)) |
37 | 36 | eleq1d 2819 |
. . . . 5
β’ (π£ β {βͺ πΎ}
β ((β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½ β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β βͺ
πΎ) β π½)) |
38 | 34, 37 | syl5ibrcom 246 |
. . . 4
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β (π£ β {βͺ πΎ} β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½)) |
39 | 38 | ralrimiv 3146 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β βπ£ β {βͺ πΎ} (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½) |
40 | | imaco 6251 |
. . . . . . . . 9
β’ ((β‘(π₯ β π β¦ (π₯ βΎ π΅)) β β‘(π§ β βͺ πΎ β¦ (π§βπ))) β π’) = (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)) |
41 | | cnvco 5886 |
. . . . . . . . . . 11
β’ β‘((π§ β βͺ πΎ β¦ (π§βπ)) β (π₯ β π β¦ (π₯ βΎ π΅))) = (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β β‘(π§ β βͺ πΎ β¦ (π§βπ))) |
42 | 25 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β§ π₯ β π) β (π₯ βΎ π΅) β βͺ πΎ) |
43 | | eqidd 2734 |
. . . . . . . . . . . . . 14
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β (π₯ β π β¦ (π₯ βΎ π΅)) = (π₯ β π β¦ (π₯ βΎ π΅))) |
44 | | eqidd 2734 |
. . . . . . . . . . . . . 14
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β (π§ β βͺ πΎ β¦ (π§βπ)) = (π§ β βͺ πΎ β¦ (π§βπ))) |
45 | | fveq1 6891 |
. . . . . . . . . . . . . 14
β’ (π§ = (π₯ βΎ π΅) β (π§βπ) = ((π₯ βΎ π΅)βπ)) |
46 | 42, 43, 44, 45 | fmptco 7127 |
. . . . . . . . . . . . 13
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β ((π§ β βͺ πΎ β¦ (π§βπ)) β (π₯ β π β¦ (π₯ βΎ π΅))) = (π₯ β π β¦ ((π₯ βΎ π΅)βπ))) |
47 | | fvres 6911 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β ((π₯ βΎ π΅)βπ) = (π₯βπ)) |
48 | 47 | ad2antrl 727 |
. . . . . . . . . . . . . 14
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β ((π₯ βΎ π΅)βπ) = (π₯βπ)) |
49 | 48 | mpteq2dv 5251 |
. . . . . . . . . . . . 13
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β (π₯ β π β¦ ((π₯ βΎ π΅)βπ)) = (π₯ β π β¦ (π₯βπ))) |
50 | 46, 49 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β ((π§ β βͺ πΎ β¦ (π§βπ)) β (π₯ β π β¦ (π₯ βΎ π΅))) = (π₯ β π β¦ (π₯βπ))) |
51 | 50 | cnveqd 5876 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β β‘((π§ β βͺ πΎ β¦ (π§βπ)) β (π₯ β π β¦ (π₯ βΎ π΅))) = β‘(π₯ β π β¦ (π₯βπ))) |
52 | 41, 51 | eqtr3id 2787 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β β‘(π§ β βͺ πΎ β¦ (π§βπ))) = β‘(π₯ β π β¦ (π₯βπ))) |
53 | 52 | imaeq1d 6059 |
. . . . . . . . 9
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β ((β‘(π₯ β π β¦ (π₯ βΎ π΅)) β β‘(π§ β βͺ πΎ β¦ (π§βπ))) β π’) = (β‘(π₯ β π β¦ (π₯βπ)) β π’)) |
54 | 40, 53 | eqtr3id 2787 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)) = (β‘(π₯ β π β¦ (π₯βπ)) β π’)) |
55 | | simpl1 1192 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β π΄ β π) |
56 | | simpl2 1193 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β πΉ:π΄βΆTop) |
57 | | simpl3 1194 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β π΅ β π΄) |
58 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β π β π΅) |
59 | 57, 58 | sseldd 3984 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β π β π΄) |
60 | 5, 2 | ptpjcn 23115 |
. . . . . . . . . 10
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π β π΄) β (π₯ β π β¦ (π₯βπ)) β (π½ Cn (πΉβπ))) |
61 | 55, 56, 59, 60 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β (π₯ β π β¦ (π₯βπ)) β (π½ Cn (πΉβπ))) |
62 | | simprr 772 |
. . . . . . . . 9
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β π’ β (πΉβπ)) |
63 | | cnima 22769 |
. . . . . . . . 9
β’ (((π₯ β π β¦ (π₯βπ)) β (π½ Cn (πΉβπ)) β§ π’ β (πΉβπ)) β (β‘(π₯ β π β¦ (π₯βπ)) β π’) β π½) |
64 | 61, 62, 63 | syl2anc 585 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β (β‘(π₯ β π β¦ (π₯βπ)) β π’) β π½) |
65 | 54, 64 | eqeltrd 2834 |
. . . . . . 7
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)) β π½) |
66 | | imaeq2 6056 |
. . . . . . . 8
β’ (π£ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’) β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) = (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’))) |
67 | 66 | eleq1d 2819 |
. . . . . . 7
β’ (π£ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’) β ((β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½ β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)) β π½)) |
68 | 65, 67 | syl5ibrcom 246 |
. . . . . 6
β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β§ (π β π΅ β§ π’ β (πΉβπ))) β (π£ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’) β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½)) |
69 | 68 | rexlimdvva 3212 |
. . . . 5
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β (βπ β π΅ βπ’ β (πΉβπ)π£ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’) β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½)) |
70 | 69 | alrimiv 1931 |
. . . 4
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β βπ£(βπ β π΅ βπ’ β (πΉβπ)π£ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’) β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½)) |
71 | | eqid 2733 |
. . . . . . 7
β’ (π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)) = (π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)) |
72 | 71 | rnmpo 7542 |
. . . . . 6
β’ ran
(π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)) = {π¦ β£ βπ β π΅ βπ’ β ((πΉ βΎ π΅)βπ)π¦ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)} |
73 | 72 | raleqi 3324 |
. . . . 5
β’
(βπ£ β
ran (π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’))(β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½ β βπ£ β {π¦ β£ βπ β π΅ βπ’ β ((πΉ βΎ π΅)βπ)π¦ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)} (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½) |
74 | 12 | rexeqdv 3327 |
. . . . . . . 8
β’ (π β π΅ β (βπ’ β ((πΉ βΎ π΅)βπ)π¦ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’) β βπ’ β (πΉβπ)π¦ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’))) |
75 | | eqeq1 2737 |
. . . . . . . . 9
β’ (π¦ = π£ β (π¦ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’) β π£ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’))) |
76 | 75 | rexbidv 3179 |
. . . . . . . 8
β’ (π¦ = π£ β (βπ’ β (πΉβπ)π¦ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’) β βπ’ β (πΉβπ)π£ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’))) |
77 | 74, 76 | sylan9bbr 512 |
. . . . . . 7
β’ ((π¦ = π£ β§ π β π΅) β (βπ’ β ((πΉ βΎ π΅)βπ)π¦ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’) β βπ’ β (πΉβπ)π£ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’))) |
78 | 77 | rexbidva 3177 |
. . . . . 6
β’ (π¦ = π£ β (βπ β π΅ βπ’ β ((πΉ βΎ π΅)βπ)π¦ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’) β βπ β π΅ βπ’ β (πΉβπ)π£ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’))) |
79 | 78 | ralab 3688 |
. . . . 5
β’
(βπ£ β
{π¦ β£ βπ β π΅ βπ’ β ((πΉ βΎ π΅)βπ)π¦ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)} (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½ β βπ£(βπ β π΅ βπ’ β (πΉβπ)π£ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’) β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½)) |
80 | 73, 79 | bitri 275 |
. . . 4
β’
(βπ£ β
ran (π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’))(β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½ β βπ£(βπ β π΅ βπ’ β (πΉβπ)π£ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’) β (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½)) |
81 | 70, 80 | sylibr 233 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β βπ£ β ran (π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’))(β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½) |
82 | | ralunb 4192 |
. . 3
β’
(βπ£ β
({βͺ πΎ} βͺ ran (π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)))(β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½ β (βπ£ β {βͺ πΎ} (β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½ β§ βπ£ β ran (π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’))(β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½)) |
83 | 39, 81, 82 | sylanbrc 584 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β βπ£ β ({βͺ πΎ} βͺ ran (π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)))(β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½) |
84 | 5 | toptopon 22419 |
. . . 4
β’ (π½ β Top β π½ β (TopOnβπ)) |
85 | 31, 84 | sylib 217 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β π½ β (TopOnβπ)) |
86 | | snex 5432 |
. . . 4
β’ {βͺ πΎ}
β V |
87 | | fvex 6905 |
. . . . . . . 8
β’ ((πΉ βΎ π΅)βπ) β V |
88 | 87 | abrexex 7949 |
. . . . . . 7
β’ {π¦ β£ βπ’ β ((πΉ βΎ π΅)βπ)π¦ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)} β V |
89 | 88 | rgenw 3066 |
. . . . . 6
β’
βπ β
π΅ {π¦ β£ βπ’ β ((πΉ βΎ π΅)βπ)π¦ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)} β V |
90 | | abrexex2g 7951 |
. . . . . 6
β’ ((π΅ β V β§ βπ β π΅ {π¦ β£ βπ’ β ((πΉ βΎ π΅)βπ)π¦ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)} β V) β {π¦ β£ βπ β π΅ βπ’ β ((πΉ βΎ π΅)βπ)π¦ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)} β V) |
91 | 17, 89, 90 | sylancl 587 |
. . . . 5
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β {π¦ β£ βπ β π΅ βπ’ β ((πΉ βΎ π΅)βπ)π¦ = (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)} β V) |
92 | 72, 91 | eqeltrid 2838 |
. . . 4
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β ran (π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)) β V) |
93 | | unexg 7736 |
. . . 4
β’ (({βͺ πΎ}
β V β§ ran (π
β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)) β V) β ({βͺ πΎ}
βͺ ran (π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’))) β V) |
94 | 86, 92, 93 | sylancr 588 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β ({βͺ
πΎ} βͺ ran (π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’))) β V) |
95 | | eqid 2733 |
. . . . 5
β’ βͺ πΎ =
βͺ πΎ |
96 | 20, 95, 71 | ptval2 23105 |
. . . 4
β’ ((π΅ β V β§ (πΉ βΎ π΅):π΅βΆTop) β πΎ = (topGenβ(fiβ({βͺ πΎ}
βͺ ran (π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)))))) |
97 | 17, 19, 96 | syl2anc 585 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β πΎ = (topGenβ(fiβ({βͺ πΎ}
βͺ ran (π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)))))) |
98 | | pttop 23086 |
. . . . . 6
β’ ((π΅ β V β§ (πΉ βΎ π΅):π΅βΆTop) β
(βtβ(πΉ βΎ π΅)) β Top) |
99 | 17, 19, 98 | syl2anc 585 |
. . . . 5
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β (βtβ(πΉ βΎ π΅)) β Top) |
100 | 20, 99 | eqeltrid 2838 |
. . . 4
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β πΎ β Top) |
101 | 95 | toptopon 22419 |
. . . 4
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
102 | 100, 101 | sylib 217 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β πΎ β (TopOnββͺ πΎ)) |
103 | 85, 94, 97, 102 | subbascn 22758 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β ((π₯ β π β¦ (π₯ βΎ π΅)) β (π½ Cn πΎ) β ((π₯ β π β¦ (π₯ βΎ π΅)):πβΆβͺ πΎ β§ βπ£ β ({βͺ πΎ}
βͺ ran (π β π΅, π’ β ((πΉ βΎ π΅)βπ) β¦ (β‘(π§ β βͺ πΎ β¦ (π§βπ)) β π’)))(β‘(π₯ β π β¦ (π₯ βΎ π΅)) β π£) β π½))) |
104 | 26, 83, 103 | mpbir2and 712 |
1
β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β (π₯ β π β¦ (π₯ βΎ π΅)) β (π½ Cn πΎ)) |