Step | Hyp | Ref
| Expression |
1 | | nllytop 22847 |
. . 3
β’ (π
β π-Locally Comp
β π
β
Top) |
2 | | elinel1 4159 |
. . . 4
β’ (π β (ran πGen β©
Haus) β π β ran
πGen) |
3 | | kgentop 22916 |
. . . 4
β’ (π β ran πGen β
π β
Top) |
4 | 2, 3 | syl 17 |
. . 3
β’ (π β (ran πGen β©
Haus) β π β
Top) |
5 | | txtop 22943 |
. . 3
β’ ((π
β Top β§ π β Top) β (π
Γt π) β Top) |
6 | 1, 4, 5 | syl2an 597 |
. 2
β’ ((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β (π
Γt π) β Top) |
7 | | simplll 774 |
. . . . . . . 8
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β π
β π-Locally
Comp) |
8 | | eqid 2733 |
. . . . . . . . . 10
β’ (π‘ β βͺ π
β¦ β¨π‘,
(2nd βπ¦)β©) = (π‘ β βͺ π
β¦ β¨π‘, (2nd βπ¦)β©) |
9 | 8 | mptpreima 6194 |
. . . . . . . . 9
β’ (β‘(π‘ β βͺ π
β¦ β¨π‘, (2nd βπ¦)β©) β π₯) = {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} |
10 | 1 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β π
β Top) |
11 | | toptopon2 22290 |
. . . . . . . . . . . . . 14
β’ (π
β Top β π
β (TopOnββͺ π
)) |
12 | 10, 11 | sylib 217 |
. . . . . . . . . . . . 13
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β π
β (TopOnββͺ π
)) |
13 | | idcn 22631 |
. . . . . . . . . . . . 13
β’ (π
β (TopOnββͺ π
)
β ( I βΎ βͺ π
) β (π
Cn π
)) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β ( I βΎ βͺ π
)
β (π
Cn π
)) |
15 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β π β (ran πGen β©
Haus)) |
16 | 15, 4 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β π β Top) |
17 | | toptopon2 22290 |
. . . . . . . . . . . . . 14
β’ (π β Top β π β (TopOnββͺ π)) |
18 | 16, 17 | sylib 217 |
. . . . . . . . . . . . 13
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β π β (TopOnββͺ π)) |
19 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β π¦ β π₯) |
20 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β π₯ β (πGenβ(π
Γt π))) |
21 | | elunii 4874 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β π₯ β§ π₯ β (πGenβ(π
Γt π))) β π¦ β βͺ
(πGenβ(π
Γt π))) |
22 | 19, 20, 21 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β π¦ β βͺ
(πGenβ(π
Γt π))) |
23 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ π
=
βͺ π
|
24 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ π =
βͺ π |
25 | 23, 24 | txuni 22966 |
. . . . . . . . . . . . . . . . 17
β’ ((π
β Top β§ π β Top) β (βͺ π
Γ βͺ π) = βͺ (π
Γt π)) |
26 | 10, 16, 25 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β (βͺ π
Γ βͺ π) =
βͺ (π
Γt π)) |
27 | 10, 16, 5 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β (π
Γt π) β Top) |
28 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ (π
Γt π) =
βͺ (π
Γt π) |
29 | 28 | kgenuni 22913 |
. . . . . . . . . . . . . . . . 17
β’ ((π
Γt π) β Top β βͺ (π
Γt π) =
βͺ (πGenβ(π
Γt π))) |
30 | 27, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β βͺ (π
Γt π) = βͺ
(πGenβ(π
Γt π))) |
31 | 26, 30 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β (βͺ π
Γ βͺ π) =
βͺ (πGenβ(π
Γt π))) |
32 | 22, 31 | eleqtrrd 2837 |
. . . . . . . . . . . . . 14
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β π¦ β (βͺ π
Γ βͺ π)) |
33 | | xp2nd 7958 |
. . . . . . . . . . . . . 14
β’ (π¦ β (βͺ π
Γ βͺ π) β (2nd βπ¦) β βͺ π) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β (2nd βπ¦) β βͺ π) |
35 | | cnconst2 22657 |
. . . . . . . . . . . . 13
β’ ((π
β (TopOnββͺ π
)
β§ π β
(TopOnββͺ π) β§ (2nd βπ¦) β βͺ π)
β (βͺ π
Γ {(2nd βπ¦)}) β (π
Cn π)) |
36 | 12, 18, 34, 35 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β (βͺ π
Γ {(2nd
βπ¦)}) β (π
Cn π)) |
37 | | fvresi 7123 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β βͺ π
β (( I βΎ βͺ π
)βπ‘) = π‘) |
38 | | fvex 6859 |
. . . . . . . . . . . . . . . . 17
β’
(2nd βπ¦) β V |
39 | 38 | fvconst2 7157 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β βͺ π
β ((βͺ π
Γ {(2nd βπ¦)})βπ‘) = (2nd βπ¦)) |
40 | 37, 39 | opeq12d 4842 |
. . . . . . . . . . . . . . 15
β’ (π‘ β βͺ π
β β¨(( I βΎ βͺ π
)βπ‘), ((βͺ π
Γ {(2nd
βπ¦)})βπ‘)β© = β¨π‘, (2nd βπ¦)β©) |
41 | 40 | mpteq2ia 5212 |
. . . . . . . . . . . . . 14
β’ (π‘ β βͺ π
β¦ β¨(( I βΎ βͺ π
)βπ‘), ((βͺ π
Γ {(2nd
βπ¦)})βπ‘)β©) = (π‘ β βͺ π
β¦ β¨π‘, (2nd βπ¦)β©) |
42 | 41 | eqcomi 2742 |
. . . . . . . . . . . . 13
β’ (π‘ β βͺ π
β¦ β¨π‘,
(2nd βπ¦)β©) = (π‘ β βͺ π
β¦ β¨(( I βΎ
βͺ π
)βπ‘), ((βͺ π
Γ {(2nd
βπ¦)})βπ‘)β©) |
43 | 23, 42 | txcnmpt 22998 |
. . . . . . . . . . . 12
β’ ((( I
βΎ βͺ π
) β (π
Cn π
) β§ (βͺ π
Γ {(2nd
βπ¦)}) β (π
Cn π)) β (π‘ β βͺ π
β¦ β¨π‘, (2nd βπ¦)β©) β (π
Cn (π
Γt π))) |
44 | 14, 36, 43 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β (π‘ β βͺ π
β¦ β¨π‘, (2nd βπ¦)β©) β (π
Cn (π
Γt π))) |
45 | | llycmpkgen 22926 |
. . . . . . . . . . . . 13
β’ (π
β π-Locally Comp
β π
β ran
πGen) |
46 | 45 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β π
β ran πGen) |
47 | 6 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β (π
Γt π) β Top) |
48 | | kgencn3 22932 |
. . . . . . . . . . . 12
β’ ((π
β ran πGen β§
(π
Γt
π) β Top) β
(π
Cn (π
Γt π)) = (π
Cn (πGenβ(π
Γt π)))) |
49 | 46, 47, 48 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β (π
Cn (π
Γt π)) = (π
Cn (πGenβ(π
Γt π)))) |
50 | 44, 49 | eleqtrd 2836 |
. . . . . . . . . 10
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β (π‘ β βͺ π
β¦ β¨π‘, (2nd βπ¦)β©) β (π
Cn (πGenβ(π
Γt π)))) |
51 | | cnima 22639 |
. . . . . . . . . 10
β’ (((π‘ β βͺ π
β¦ β¨π‘,
(2nd βπ¦)β©) β (π
Cn (πGenβ(π
Γt π))) β§ π₯ β (πGenβ(π
Γt π))) β (β‘(π‘ β βͺ π
β¦ β¨π‘, (2nd βπ¦)β©) β π₯) β π
) |
52 | 50, 20, 51 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β (β‘(π‘ β βͺ π
β¦ β¨π‘, (2nd βπ¦)β©) β π₯) β π
) |
53 | 9, 52 | eqeltrrid 2839 |
. . . . . . . 8
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β π
) |
54 | | opeq1 4834 |
. . . . . . . . . 10
β’ (π‘ = (1st βπ¦) β β¨π‘, (2nd βπ¦)β© = β¨(1st
βπ¦), (2nd
βπ¦)β©) |
55 | 54 | eleq1d 2819 |
. . . . . . . . 9
β’ (π‘ = (1st βπ¦) β (β¨π‘, (2nd βπ¦)β© β π₯ β β¨(1st
βπ¦), (2nd
βπ¦)β© β
π₯)) |
56 | | xp1st 7957 |
. . . . . . . . . 10
β’ (π¦ β (βͺ π
Γ βͺ π) β (1st βπ¦) β βͺ π
) |
57 | 32, 56 | syl 17 |
. . . . . . . . 9
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β (1st βπ¦) β βͺ π
) |
58 | | 1st2nd2 7964 |
. . . . . . . . . . 11
β’ (π¦ β (βͺ π
Γ βͺ π) β π¦ = β¨(1st βπ¦), (2nd βπ¦)β©) |
59 | 32, 58 | syl 17 |
. . . . . . . . . 10
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β π¦ = β¨(1st βπ¦), (2nd βπ¦)β©) |
60 | 59, 19 | eqeltrrd 2835 |
. . . . . . . . 9
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β β¨(1st βπ¦), (2nd βπ¦)β© β π₯) |
61 | 55, 57, 60 | elrabd 3651 |
. . . . . . . 8
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β (1st βπ¦) β {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯}) |
62 | | nlly2i 22850 |
. . . . . . . 8
β’ ((π
β π-Locally Comp
β§ {π‘ β βͺ π
β£ β¨π‘,
(2nd βπ¦)β© β π₯} β π
β§ (1st βπ¦) β {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯}) β βπ β π« {π‘ β βͺ π
β£ β¨π‘,
(2nd βπ¦)β© β π₯}βπ’ β π
((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp)) |
63 | 7, 53, 61, 62 | syl3anc 1372 |
. . . . . . 7
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β βπ β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯}βπ’ β π
((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp)) |
64 | 10 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β π
β Top) |
65 | 16 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β π β Top) |
66 | | simprlr 779 |
. . . . . . . . . . 11
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β π’ β π
) |
67 | | ssrab2 4041 |
. . . . . . . . . . . . . 14
β’ {π£ β βͺ π
β£ (π Γ {π£}) β π₯} β βͺ π |
68 | 67 | a1i 11 |
. . . . . . . . . . . . 13
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β {π£ β βͺ π β£ (π Γ {π£}) β π₯} β βͺ π) |
69 | | incom 4165 |
. . . . . . . . . . . . . . . 16
β’ ({π£ β βͺ π
β£ (π Γ {π£}) β π₯} β© π) = (π β© {π£ β βͺ π β£ (π Γ {π£}) β π₯}) |
70 | | simprll 778 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯}) |
71 | 70 | elpwid 4573 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β π β {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯}) |
72 | | ssrab2 4041 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ {π‘ β βͺ π
β£ β¨π‘,
(2nd βπ¦)β© β π₯} β βͺ π
|
73 | 71, 72 | sstrdi 3960 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β π β βͺ π
) |
74 | 73 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β π
β βͺ π
) |
75 | | elpwi 4571 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π« βͺ π
β π β βͺ π) |
76 | 75 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β π
β βͺ π) |
77 | | eldif 3924 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π‘ β ((π Γ π) β π₯) β (π‘ β (π Γ π) β§ Β¬ π‘ β π₯)) |
78 | 77 | anbi1i 625 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π‘ β ((π Γ π) β π₯) β§ ((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π) β ((π‘ β (π Γ π) β§ Β¬ π‘ β π₯) β§ ((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π)) |
79 | | anass 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π‘ β (π Γ π) β§ Β¬ π‘ β π₯) β§ ((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π) β (π‘ β (π Γ π) β§ (Β¬ π‘ β π₯ β§ ((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π))) |
80 | 78, 79 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π‘ β ((π Γ π) β π₯) β§ ((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π) β (π‘ β (π Γ π) β§ (Β¬ π‘ β π₯ β§ ((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π))) |
81 | 80 | rexbii2 3090 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(βπ‘ β
((π Γ π) β π₯)((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π β βπ‘ β (π Γ π)(Β¬ π‘ β π₯ β§ ((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π)) |
82 | | ancom 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((Β¬
π‘ β π₯ β§ ((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π) β (((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π β§ Β¬ π‘ β π₯)) |
83 | | fveqeq2 6855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π‘ = β¨π, π’β© β (((2nd βΎ
(βͺ π
Γ βͺ π))βπ‘) = π β ((2nd βΎ (βͺ π
Γ βͺ π))ββ¨π, π’β©) = π)) |
84 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π‘ = β¨π, π’β© β (π‘ β π₯ β β¨π, π’β© β π₯)) |
85 | 84 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π‘ = β¨π, π’β© β (Β¬ π‘ β π₯ β Β¬ β¨π, π’β© β π₯)) |
86 | 83, 85 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π‘ = β¨π, π’β© β ((((2nd βΎ
(βͺ π
Γ βͺ π))βπ‘) = π β§ Β¬ π‘ β π₯) β (((2nd βΎ (βͺ π
Γ βͺ π))ββ¨π, π’β©) = π β§ Β¬ β¨π, π’β© β π₯))) |
87 | 82, 86 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π‘ = β¨π, π’β© β ((Β¬ π‘ β π₯ β§ ((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π) β (((2nd βΎ (βͺ π
Γ βͺ π))ββ¨π, π’β©) = π β§ Β¬ β¨π, π’β© β π₯))) |
88 | 87 | rexxp 5802 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(βπ‘ β
(π Γ π)(Β¬ π‘ β π₯ β§ ((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π) β βπ β π βπ’ β π (((2nd βΎ (βͺ π
Γ βͺ π))ββ¨π, π’β©) = π β§ Β¬ β¨π, π’β© β π₯)) |
89 | 81, 88 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(βπ‘ β
((π Γ π) β π₯)((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π β βπ β π βπ’ β π (((2nd βΎ (βͺ π
Γ βͺ π))ββ¨π, π’β©) = π β§ Β¬ β¨π, π’β© β π₯)) |
90 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β βͺ π
β§ π β βͺ π)
β π β βͺ π
) |
91 | 90 | sselda 3948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β βͺ π
β§ π β βͺ π)
β§ π β π ) β π β βͺ π
) |
92 | 91 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β βͺ π
β§ π β βͺ π)
β§ π β π ) β§ π’ β π) β π β βͺ π
) |
93 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β βͺ π
β§ π β βͺ π)
β§ π β π ) β π β βͺ π) |
94 | 93 | sselda 3948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((((π β βͺ π
β§ π β βͺ π)
β§ π β π ) β§ π’ β π) β π’ β βͺ π) |
95 | 92, 94 | opelxpd 5675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β βͺ π
β§ π β βͺ π)
β§ π β π ) β§ π’ β π) β β¨π, π’β© β (βͺ
π
Γ βͺ π)) |
96 | 95 | fvresd 6866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β βͺ π
β§ π β βͺ π)
β§ π β π ) β§ π’ β π) β ((2nd βΎ (βͺ π
Γ βͺ π))ββ¨π, π’β©) = (2nd ββ¨π, π’β©)) |
97 | | vex 3451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ π β V |
98 | | vex 3451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ π’ β V |
99 | 97, 98 | op2nd 7934 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(2nd ββ¨π, π’β©) = π’ |
100 | 96, 99 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β βͺ π
β§ π β βͺ π)
β§ π β π ) β§ π’ β π) β ((2nd βΎ (βͺ π
Γ βͺ π))ββ¨π, π’β©) = π’) |
101 | 100 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β βͺ π
β§ π β βͺ π)
β§ π β π ) β§ π’ β π) β (((2nd βΎ (βͺ π
Γ βͺ π))ββ¨π, π’β©) = π β π’ = π)) |
102 | 101 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β βͺ π
β§ π β βͺ π)
β§ π β π ) β§ π’ β π) β ((((2nd βΎ (βͺ π
Γ βͺ π))ββ¨π, π’β©) = π β§ Β¬ β¨π, π’β© β π₯) β (π’ = π β§ Β¬ β¨π, π’β© β π₯))) |
103 | 102 | rexbidva 3170 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β βͺ π
β§ π β βͺ π)
β§ π β π ) β (βπ’ β π (((2nd βΎ (βͺ π
Γ βͺ π))ββ¨π, π’β©) = π β§ Β¬ β¨π, π’β© β π₯) β βπ’ β π (π’ = π β§ Β¬ β¨π, π’β© β π₯))) |
104 | | opeq2 4835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π’ = π β β¨π, π’β© = β¨π, πβ©) |
105 | 104 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π’ = π β (β¨π, π’β© β π₯ β β¨π, πβ© β π₯)) |
106 | 105 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π’ = π β (Β¬ β¨π, π’β© β π₯ β Β¬ β¨π, πβ© β π₯)) |
107 | 106 | ceqsrexbv 3610 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(βπ’ β
π (π’ = π β§ Β¬ β¨π, π’β© β π₯) β (π β π β§ Β¬ β¨π, πβ© β π₯)) |
108 | 103, 107 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β βͺ π
β§ π β βͺ π)
β§ π β π ) β (βπ’ β π (((2nd βΎ (βͺ π
Γ βͺ π))ββ¨π, π’β©) = π β§ Β¬ β¨π, π’β© β π₯) β (π β π β§ Β¬ β¨π, πβ© β π₯))) |
109 | 108 | rexbidva 3170 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β βͺ π
β§ π β βͺ π)
β (βπ β
π βπ’ β π (((2nd βΎ (βͺ π
Γ βͺ π))ββ¨π, π’β©) = π β§ Β¬ β¨π, π’β© β π₯) β βπ β π (π β π β§ Β¬ β¨π, πβ© β π₯))) |
110 | | r19.42v 3184 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(βπ β
π (π β π β§ Β¬ β¨π, πβ© β π₯) β (π β π β§ βπ β π Β¬ β¨π, πβ© β π₯)) |
111 | 109, 110 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β βͺ π
β§ π β βͺ π)
β (βπ β
π βπ’ β π (((2nd βΎ (βͺ π
Γ βͺ π))ββ¨π, π’β©) = π β§ Β¬ β¨π, π’β© β π₯) β (π β π β§ βπ β π Β¬ β¨π, πβ© β π₯))) |
112 | 89, 111 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β βͺ π
β§ π β βͺ π)
β (βπ‘ β
((π Γ π) β π₯)((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π β (π β π β§ βπ β π Β¬ β¨π, πβ© β π₯))) |
113 | | f2ndres 7950 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(2nd βΎ (βͺ π
Γ βͺ π)):(βͺ
π
Γ βͺ π)βΆβͺ π |
114 | | ffn 6672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((2nd βΎ (βͺ π
Γ βͺ π)):(βͺ
π
Γ βͺ π)βΆβͺ π β (2nd βΎ
(βͺ π
Γ βͺ π)) Fn (βͺ π
Γ βͺ π)) |
115 | 113, 114 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(2nd βΎ (βͺ π
Γ βͺ π)) Fn (βͺ π
Γ βͺ π) |
116 | | difss 4095 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π Γ π) β π₯) β (π Γ π) |
117 | | xpss12 5652 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β βͺ π
β§ π β βͺ π)
β (π Γ π) β (βͺ π
Γ βͺ π)) |
118 | 116, 117 | sstrid 3959 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β βͺ π
β§ π β βͺ π)
β ((π Γ π) β π₯) β (βͺ π
Γ βͺ π)) |
119 | | fvelimab 6918 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((2nd βΎ (βͺ π
Γ βͺ π))
Fn (βͺ π
Γ βͺ π) β§ ((π Γ π) β π₯) β (βͺ π
Γ βͺ π))
β (π β
((2nd βΎ (βͺ π
Γ βͺ π)) β ((π Γ π) β π₯)) β βπ‘ β ((π Γ π) β π₯)((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π)) |
120 | 115, 118,
119 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β βͺ π
β§ π β βͺ π)
β (π β
((2nd βΎ (βͺ π
Γ βͺ π)) β ((π Γ π) β π₯)) β βπ‘ β ((π Γ π) β π₯)((2nd βΎ (βͺ π
Γ βͺ π))βπ‘) = π)) |
121 | | eldif 3924 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π β {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β (π β π β§ Β¬ π β {π£ β βͺ π β£ (π Γ {π£}) β π₯})) |
122 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β βͺ π
β§ π β βͺ π)
β π β βͺ π) |
123 | 122 | sselda 3948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β βͺ π
β§ π β βͺ π)
β§ π β π) β π β βͺ π) |
124 | | sneq 4600 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π£ = π β {π£} = {π}) |
125 | 124 | xpeq2d 5667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π£ = π β (π Γ {π£}) = (π Γ {π})) |
126 | 125 | sseq1d 3979 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π£ = π β ((π Γ {π£}) β π₯ β (π Γ {π}) β π₯)) |
127 | | dfss3 3936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π Γ {π}) β π₯ β βπ β (π Γ {π})π β π₯) |
128 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = β¨π, π‘β© β (π β π₯ β β¨π, π‘β© β π₯)) |
129 | 128 | ralxp 5801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(βπ β
(π Γ {π})π β π₯ β βπ β π βπ‘ β {π}β¨π, π‘β© β π₯) |
130 | | vex 3451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ π β V |
131 | | opeq2 4835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π‘ = π β β¨π, π‘β© = β¨π, πβ©) |
132 | 131 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π‘ = π β (β¨π, π‘β© β π₯ β β¨π, πβ© β π₯)) |
133 | 130, 132 | ralsn 4646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(βπ‘ β
{π}β¨π, π‘β© β π₯ β β¨π, πβ© β π₯) |
134 | 133 | ralbii 3093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(βπ β
π βπ‘ β {π}β¨π, π‘β© β π₯ β βπ β π β¨π, πβ© β π₯) |
135 | 127, 129,
134 | 3bitri 297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π Γ {π}) β π₯ β βπ β π β¨π, πβ© β π₯) |
136 | 126, 135 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π£ = π β ((π Γ {π£}) β π₯ β βπ β π β¨π, πβ© β π₯)) |
137 | 136 | elrab3 3650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β βͺ π
β (π β {π£ β βͺ π
β£ (π Γ {π£}) β π₯} β βπ β π β¨π, πβ© β π₯)) |
138 | 123, 137 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β βͺ π
β§ π β βͺ π)
β§ π β π) β (π β {π£ β βͺ π β£ (π Γ {π£}) β π₯} β βπ β π β¨π, πβ© β π₯)) |
139 | 138 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β βͺ π
β§ π β βͺ π)
β§ π β π) β (Β¬ π β {π£ β βͺ π β£ (π Γ {π£}) β π₯} β Β¬ βπ β π β¨π, πβ© β π₯)) |
140 | | rexnal 3100 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ β
π Β¬ β¨π, πβ© β π₯ β Β¬ βπ β π β¨π, πβ© β π₯) |
141 | 139, 140 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β βͺ π
β§ π β βͺ π)
β§ π β π) β (Β¬ π β {π£ β βͺ π β£ (π Γ {π£}) β π₯} β βπ β π Β¬ β¨π, πβ© β π₯)) |
142 | 141 | pm5.32da 580 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β βͺ π
β§ π β βͺ π)
β ((π β π β§ Β¬ π β {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β (π β π β§ βπ β π Β¬ β¨π, πβ© β π₯))) |
143 | 121, 142 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β βͺ π
β§ π β βͺ π)
β (π β (π β {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β (π β π β§ βπ β π Β¬ β¨π, πβ© β π₯))) |
144 | 112, 120,
143 | 3bitr4d 311 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β βͺ π
β§ π β βͺ π)
β (π β
((2nd βΎ (βͺ π
Γ βͺ π)) β ((π Γ π) β π₯)) β π β (π β {π£ β βͺ π β£ (π Γ {π£}) β π₯}))) |
145 | 144 | eqrdv 2731 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β βͺ π
β§ π β βͺ π)
β ((2nd βΎ (βͺ π
Γ βͺ π)) β ((π Γ π) β π₯)) = (π β {π£ β βͺ π β£ (π Γ {π£}) β π₯})) |
146 | 74, 76, 145 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((2nd βΎ (βͺ
π
Γ βͺ π))
β ((π Γ π) β π₯)) = (π β {π£ β βͺ π β£ (π Γ {π£}) β π₯})) |
147 | | difin 4225 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π β© {π£ β βͺ π β£ (π Γ {π£}) β π₯})) = (π β {π£ β βͺ π β£ (π Γ {π£}) β π₯}) |
148 | 65 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β π
β Top) |
149 | 24 | restuni 22536 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Top β§ π β βͺ π)
β π = βͺ (π
βΎt π)) |
150 | 148, 76, 149 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β π =
βͺ (π βΎt π)) |
151 | 150 | difeq1d 4085 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π
β (π β© {π£ β βͺ π
β£ (π Γ {π£}) β π₯})) = (βͺ (π βΎt π) β (π β© {π£ β βͺ π β£ (π Γ {π£}) β π₯}))) |
152 | 147, 151 | eqtr3id 2787 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π
β {π£ β βͺ π
β£ (π Γ {π£}) β π₯}) = (βͺ (π βΎt π) β (π β© {π£ β βͺ π β£ (π Γ {π£}) β π₯}))) |
153 | 146, 152 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((2nd βΎ (βͺ
π
Γ βͺ π))
β ((π Γ π) β π₯)) = (βͺ (π βΎt π) β (π β© {π£ β βͺ π β£ (π Γ {π£}) β π₯}))) |
154 | 15 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β π
β (ran πGen β© Haus)) |
155 | 154 | elin2d 4163 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β π
β Haus) |
156 | | df-ima 5650 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((2nd βΎ (βͺ π
Γ βͺ π)) β ((π Γ π) β π₯)) = ran ((2nd βΎ (βͺ π
Γ βͺ π)) βΎ ((π Γ π) β π₯)) |
157 | | resres 5954 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((2nd βΎ (βͺ π
Γ βͺ π)) βΎ ((π Γ π) β π₯)) = (2nd βΎ ((βͺ π
Γ βͺ π) β© ((π Γ π) β π₯))) |
158 | | inss2 4193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((βͺ π
Γ βͺ π) β© ((π Γ π) β π₯)) β ((π Γ π) β π₯) |
159 | 158, 116 | sstri 3957 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((βͺ π
Γ βͺ π) β© ((π Γ π) β π₯)) β (π Γ π) |
160 | | ssres2 5969 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((βͺ π
Γ βͺ π) β© ((π Γ π) β π₯)) β (π Γ π) β (2nd βΎ ((βͺ π
Γ βͺ π) β© ((π Γ π) β π₯))) β (2nd βΎ (π Γ π))) |
161 | 159, 160 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(2nd βΎ ((βͺ π
Γ βͺ π) β© ((π Γ π) β π₯))) β (2nd βΎ (π Γ π)) |
162 | 157, 161 | eqsstri 3982 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((2nd βΎ (βͺ π
Γ βͺ π)) βΎ ((π Γ π) β π₯)) β (2nd βΎ (π Γ π)) |
163 | 162 | rnssi 5899 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ran
((2nd βΎ (βͺ π
Γ βͺ π)) βΎ ((π Γ π) β π₯)) β ran (2nd βΎ (π Γ π)) |
164 | 156, 163 | eqsstri 3982 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((2nd βΎ (βͺ π
Γ βͺ π)) β ((π Γ π) β π₯)) β ran (2nd βΎ (π Γ π)) |
165 | | f2ndres 7950 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(2nd βΎ (π Γ π)):(π Γ π)βΆπ |
166 | | frn 6679 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((2nd βΎ (π Γ π)):(π Γ π)βΆπ β ran (2nd βΎ (π Γ π)) β π) |
167 | 165, 166 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ran
(2nd βΎ (π
Γ π)) β π |
168 | 164, 167 | sstri 3957 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((2nd βΎ (βͺ π
Γ βͺ π)) β ((π Γ π) β π₯)) β π |
169 | 168, 76 | sstrid 3959 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((2nd βΎ (βͺ
π
Γ βͺ π))
β ((π Γ π) β π₯)) β βͺ π) |
170 | 12 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β π
β (TopOnββͺ π
)) |
171 | 148, 17 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β π
β (TopOnββͺ π)) |
172 | | tx2cn 22984 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π
β (TopOnββͺ π
)
β§ π β
(TopOnββͺ π)) β (2nd βΎ (βͺ π
Γ βͺ π)) β ((π
Γt π) Cn π)) |
173 | 170, 171,
172 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (2nd βΎ (βͺ
π
Γ βͺ π))
β ((π
Γt π) Cn
π)) |
174 | 27 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π
Γt π)
β Top) |
175 | 116 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((π
Γ π) β π₯) β (π Γ π)) |
176 | | vex 3451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ π β V |
177 | | vex 3451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ π β V |
178 | 176, 177 | xpex 7691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π Γ π) β V |
179 | 178 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π
Γ π) β
V) |
180 | | restabs 22539 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π
Γt π) β Top β§ ((π Γ π) β π₯) β (π Γ π) β§ (π Γ π) β V) β (((π
Γt π) βΎt (π Γ π)) βΎt ((π Γ π) β π₯)) = ((π
Γt π) βΎt ((π Γ π) β π₯))) |
181 | 174, 175,
179, 180 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (((π
Γt π)
βΎt (π
Γ π))
βΎt ((π
Γ π) β π₯)) = ((π
Γt π) βΎt ((π Γ π) β π₯))) |
182 | 64 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β π
β Top) |
183 | 154, 4 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β π
β Top) |
184 | 176 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β π
β V) |
185 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β π
β π« βͺ π) |
186 | | txrest 23005 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π
β Top β§ π β Top) β§ (π β V β§ π β π« βͺ π))
β ((π
Γt π)
βΎt (π
Γ π)) = ((π
βΎt π ) Γt (π βΎt π))) |
187 | 182, 183,
184, 185, 186 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((π
Γt π)
βΎt (π
Γ π)) = ((π
βΎt π ) Γt (π βΎt π))) |
188 | | simprr3 1224 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β (π
βΎt π ) β Comp) |
189 | 188 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π
βΎt π )
β Comp) |
190 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π
βΎt π)
β Comp) |
191 | | txcmp 23017 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π
βΎt π ) β Comp β§ (π βΎt π) β Comp) β ((π
βΎt π ) Γt (π βΎt π)) β Comp) |
192 | 189, 190,
191 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((π
βΎt π )
Γt (π
βΎt π))
β Comp) |
193 | 187, 192 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((π
Γt π)
βΎt (π
Γ π)) β
Comp) |
194 | | difin 4225 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π Γ π) β ((π Γ π) β© π₯)) = ((π Γ π) β π₯) |
195 | 74, 76, 117 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π
Γ π) β (βͺ π
Γ βͺ π)) |
196 | 182, 148,
25 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (βͺ π
Γ βͺ π) = βͺ
(π
Γt
π)) |
197 | 195, 196 | sseqtrd 3988 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π
Γ π) β βͺ (π
Γt π)) |
198 | 28 | restuni 22536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π
Γt π) β Top β§ (π Γ π) β βͺ (π
Γt π)) β (π Γ π) = βͺ ((π
Γt π) βΎt (π Γ π))) |
199 | 174, 197,
198 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π
Γ π) = βͺ ((π
Γt π)
βΎt (π
Γ π))) |
200 | 199 | difeq1d 4085 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((π
Γ π) β ((π Γ π) β© π₯)) = (βͺ ((π
Γt π) βΎt (π Γ π)) β ((π Γ π) β© π₯))) |
201 | 194, 200 | eqtr3id 2787 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((π
Γ π) β π₯) = (βͺ ((π
Γt π)
βΎt (π
Γ π)) β ((π Γ π) β© π₯))) |
202 | | resttop 22534 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π
Γt π) β Top β§ (π Γ π) β V) β ((π
Γt π) βΎt (π Γ π)) β Top) |
203 | 174, 178,
202 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((π
Γt π)
βΎt (π
Γ π)) β
Top) |
204 | | incom 4165 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π Γ π) β© π₯) = (π₯ β© (π Γ π)) |
205 | 20 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β π₯
β (πGenβ(π
Γt π))) |
206 | | kgeni 22911 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π₯ β
(πGenβ(π
Γt π))
β§ ((π
Γt π)
βΎt (π
Γ π)) β Comp)
β (π₯ β© (π Γ π)) β ((π
Γt π) βΎt (π Γ π))) |
207 | 205, 193,
206 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π₯
β© (π Γ π)) β ((π
Γt π) βΎt (π Γ π))) |
208 | 204, 207 | eqeltrid 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((π
Γ π) β© π₯) β ((π
Γt π) βΎt (π Γ π))) |
209 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ βͺ ((π
Γt π)
βΎt (π
Γ π)) = βͺ ((π
Γt π)
βΎt (π
Γ π)) |
210 | 209 | opncld 22407 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π
Γt π) βΎt (π Γ π)) β Top β§ ((π Γ π) β© π₯) β ((π
Γt π) βΎt (π Γ π))) β (βͺ
((π
Γt
π) βΎt
(π Γ π)) β ((π Γ π) β© π₯)) β (Clsdβ((π
Γt π) βΎt (π Γ π)))) |
211 | 203, 208,
210 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (βͺ ((π
Γt π) βΎt (π Γ π)) β ((π Γ π) β© π₯)) β (Clsdβ((π
Γt π) βΎt (π Γ π)))) |
212 | 201, 211 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((π
Γ π) β π₯) β (Clsdβ((π
Γt π) βΎt (π Γ π)))) |
213 | | cmpcld 22776 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π
Γt π) βΎt (π Γ π)) β Comp β§ ((π Γ π) β π₯) β (Clsdβ((π
Γt π) βΎt (π Γ π)))) β (((π
Γt π) βΎt (π Γ π)) βΎt ((π Γ π) β π₯)) β Comp) |
214 | 193, 212,
213 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (((π
Γt π)
βΎt (π
Γ π))
βΎt ((π
Γ π) β π₯)) β Comp) |
215 | 181, 214 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((π
Γt π)
βΎt ((π
Γ π) β π₯)) β Comp) |
216 | | imacmp 22771 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((2nd βΎ (βͺ π
Γ βͺ π))
β ((π
Γt π) Cn
π) β§ ((π
Γt π) βΎt ((π Γ π) β π₯)) β Comp) β (π βΎt ((2nd
βΎ (βͺ π
Γ βͺ π)) β ((π Γ π) β π₯))) β Comp) |
217 | 173, 215,
216 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π
βΎt ((2nd βΎ (βͺ
π
Γ βͺ π))
β ((π Γ π) β π₯))) β Comp) |
218 | 24 | hauscmp 22781 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Haus β§
((2nd βΎ (βͺ π
Γ βͺ π)) β ((π Γ π) β π₯)) β βͺ π β§ (π βΎt ((2nd
βΎ (βͺ π
Γ βͺ π)) β ((π Γ π) β π₯))) β Comp) β ((2nd
βΎ (βͺ π
Γ βͺ π)) β ((π Γ π) β π₯)) β (Clsdβπ)) |
219 | 155, 169,
217, 218 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((2nd βΎ (βͺ
π
Γ βͺ π))
β ((π Γ π) β π₯)) β (Clsdβπ)) |
220 | 168 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((2nd βΎ (βͺ
π
Γ βͺ π))
β ((π Γ π) β π₯)) β π) |
221 | 24 | restcldi 22547 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β βͺ π
β§ ((2nd βΎ (βͺ π
Γ βͺ π)) β ((π Γ π) β π₯)) β (Clsdβπ) β§ ((2nd βΎ (βͺ π
Γ βͺ π)) β ((π Γ π) β π₯)) β π) β ((2nd βΎ (βͺ π
Γ βͺ π)) β ((π Γ π) β π₯)) β (Clsdβ(π βΎt π))) |
222 | 76, 219, 220, 221 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((2nd βΎ (βͺ
π
Γ βͺ π))
β ((π Γ π) β π₯)) β (Clsdβ(π βΎt π))) |
223 | 153, 222 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . . 17
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (βͺ (π βΎt π) β (π β© {π£ β βͺ π β£ (π Γ {π£}) β π₯})) β (Clsdβ(π βΎt π))) |
224 | | resttop 22534 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Top β§ π β π« βͺ π)
β (π
βΎt π)
β Top) |
225 | 148, 185,
224 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π
βΎt π)
β Top) |
226 | | inss1 4192 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β© {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β π |
227 | 226, 150 | sseqtrid 4000 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π
β© {π£ β βͺ π
β£ (π Γ {π£}) β π₯}) β βͺ
(π βΎt
π)) |
228 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’ βͺ (π
βΎt π) =
βͺ (π βΎt π) |
229 | 228 | isopn2 22406 |
. . . . . . . . . . . . . . . . . 18
β’ (((π βΎt π) β Top β§ (π β© {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β βͺ
(π βΎt
π)) β ((π β© {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β (π βΎt π) β (βͺ (π βΎt π) β (π β© {π£ β βͺ π β£ (π Γ {π£}) β π₯})) β (Clsdβ(π βΎt π)))) |
230 | 225, 227,
229 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ((π
β© {π£ β βͺ π
β£ (π Γ {π£}) β π₯}) β (π βΎt π) β (βͺ (π βΎt π) β (π β© {π£ β βͺ π β£ (π Γ {π£}) β π₯})) β (Clsdβ(π βΎt π)))) |
231 | 223, 230 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β (π
β© {π£ β βͺ π
β£ (π Γ {π£}) β π₯}) β (π βΎt π)) |
232 | 69, 231 | eqeltrid 2838 |
. . . . . . . . . . . . . . 15
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ (π β π« βͺ π
β§ (π
βΎt π)
β Comp)) β ({π£
β βͺ π β£ (π Γ {π£}) β π₯} β© π) β (π βΎt π)) |
233 | 232 | expr 458 |
. . . . . . . . . . . . . 14
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ π β π« βͺ π)
β ((π
βΎt π)
β Comp β ({π£
β βͺ π β£ (π Γ {π£}) β π₯} β© π) β (π βΎt π))) |
234 | 233 | ralrimiva 3140 |
. . . . . . . . . . . . 13
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β βπ β π« βͺ π((π βΎt π) β Comp β ({π£ β βͺ π β£ (π Γ {π£}) β π₯} β© π) β (π βΎt π))) |
235 | 65, 17 | sylib 217 |
. . . . . . . . . . . . . 14
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β π β (TopOnββͺ π)) |
236 | | elkgen 22910 |
. . . . . . . . . . . . . 14
β’ (π β (TopOnββͺ π)
β ({π£ β βͺ π
β£ (π Γ {π£}) β π₯} β (πGenβπ) β ({π£ β βͺ π β£ (π Γ {π£}) β π₯} β βͺ π β§ βπ β π« βͺ π((π βΎt π) β Comp β ({π£ β βͺ π β£ (π Γ {π£}) β π₯} β© π) β (π βΎt π))))) |
237 | 235, 236 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β ({π£ β βͺ π β£ (π Γ {π£}) β π₯} β (πGenβπ) β ({π£ β βͺ π β£ (π Γ {π£}) β π₯} β βͺ π β§ βπ β π« βͺ π((π βΎt π) β Comp β ({π£ β βͺ π β£ (π Γ {π£}) β π₯} β© π) β (π βΎt π))))) |
238 | 68, 234, 237 | mpbir2and 712 |
. . . . . . . . . . . 12
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β {π£ β βͺ π β£ (π Γ {π£}) β π₯} β (πGenβπ)) |
239 | 15 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β π β (ran πGen β©
Haus)) |
240 | 239, 2 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β π β ran πGen) |
241 | | kgenidm 22921 |
. . . . . . . . . . . . 13
β’ (π β ran πGen β
(πGenβπ) =
π) |
242 | 240, 241 | syl 17 |
. . . . . . . . . . . 12
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β
(πGenβπ) =
π) |
243 | 238, 242 | eleqtrd 2836 |
. . . . . . . . . . 11
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β {π£ β βͺ π β£ (π Γ {π£}) β π₯} β π) |
244 | | txopn 22976 |
. . . . . . . . . . 11
β’ (((π
β Top β§ π β Top) β§ (π’ β π
β§ {π£ β βͺ π β£ (π Γ {π£}) β π₯} β π)) β (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β (π
Γt π)) |
245 | 64, 65, 66, 243, 244 | syl22anc 838 |
. . . . . . . . . 10
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β (π
Γt π)) |
246 | 59 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β π¦ = β¨(1st βπ¦), (2nd βπ¦)β©) |
247 | | simprr1 1222 |
. . . . . . . . . . . 12
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β (1st
βπ¦) β π’) |
248 | | sneq 4600 |
. . . . . . . . . . . . . . 15
β’ (π£ = (2nd βπ¦) β {π£} = {(2nd βπ¦)}) |
249 | 248 | xpeq2d 5667 |
. . . . . . . . . . . . . 14
β’ (π£ = (2nd βπ¦) β (π Γ {π£}) = (π Γ {(2nd βπ¦)})) |
250 | 249 | sseq1d 3979 |
. . . . . . . . . . . . 13
β’ (π£ = (2nd βπ¦) β ((π Γ {π£}) β π₯ β (π Γ {(2nd βπ¦)}) β π₯)) |
251 | 34 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β (2nd
βπ¦) β βͺ π) |
252 | | relxp 5655 |
. . . . . . . . . . . . . . 15
β’ Rel
(π Γ {(2nd
βπ¦)}) |
253 | 252 | a1i 11 |
. . . . . . . . . . . . . 14
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β Rel (π Γ {(2nd
βπ¦)})) |
254 | | opelxp 5673 |
. . . . . . . . . . . . . . 15
β’
(β¨π, πβ© β (π Γ {(2nd
βπ¦)}) β (π β π β§ π β {(2nd βπ¦)})) |
255 | 71 | sselda 3948 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ π β π ) β π β {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯}) |
256 | | opeq1 4834 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π‘ = π β β¨π‘, (2nd βπ¦)β© = β¨π, (2nd βπ¦)β©) |
257 | 256 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π‘ = π β (β¨π‘, (2nd βπ¦)β© β π₯ β β¨π, (2nd βπ¦)β© β π₯)) |
258 | 257 | elrab 3649 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β (π β βͺ π
β§ β¨π, (2nd βπ¦)β© β π₯)) |
259 | 258 | simprbi 498 |
. . . . . . . . . . . . . . . . . 18
β’ (π β {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β β¨π, (2nd βπ¦)β© β π₯) |
260 | 255, 259 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ π β π ) β β¨π, (2nd βπ¦)β© β π₯) |
261 | | elsni 4607 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {(2nd
βπ¦)} β π = (2nd βπ¦)) |
262 | 261 | opeq2d 4841 |
. . . . . . . . . . . . . . . . . 18
β’ (π β {(2nd
βπ¦)} β
β¨π, πβ© = β¨π, (2nd βπ¦)β©) |
263 | 262 | eleq1d 2819 |
. . . . . . . . . . . . . . . . 17
β’ (π β {(2nd
βπ¦)} β
(β¨π, πβ© β π₯ β β¨π, (2nd βπ¦)β© β π₯)) |
264 | 260, 263 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . 16
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ π β π ) β (π β {(2nd βπ¦)} β β¨π, πβ© β π₯)) |
265 | 264 | expimpd 455 |
. . . . . . . . . . . . . . 15
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β ((π β π β§ π β {(2nd βπ¦)}) β β¨π, πβ© β π₯)) |
266 | 254, 265 | biimtrid 241 |
. . . . . . . . . . . . . 14
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β (β¨π, πβ© β (π Γ {(2nd βπ¦)}) β β¨π, πβ© β π₯)) |
267 | 253, 266 | relssdv 5748 |
. . . . . . . . . . . . 13
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β (π Γ {(2nd βπ¦)}) β π₯) |
268 | 250, 251,
267 | elrabd 3651 |
. . . . . . . . . . . 12
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β (2nd
βπ¦) β {π£ β βͺ π
β£ (π Γ {π£}) β π₯}) |
269 | 247, 268 | opelxpd 5675 |
. . . . . . . . . . 11
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β β¨(1st
βπ¦), (2nd
βπ¦)β© β
(π’ Γ {π£ β βͺ π
β£ (π Γ {π£}) β π₯})) |
270 | 246, 269 | eqeltrd 2834 |
. . . . . . . . . 10
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β π¦ β (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯})) |
271 | | relxp 5655 |
. . . . . . . . . . . 12
β’ Rel
(π’ Γ {π£ β βͺ π
β£ (π Γ {π£}) β π₯}) |
272 | 271 | a1i 11 |
. . . . . . . . . . 11
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β Rel (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯})) |
273 | | opelxp 5673 |
. . . . . . . . . . . 12
β’
(β¨π, πβ© β (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β (π β π’ β§ π β {π£ β βͺ π β£ (π Γ {π£}) β π₯})) |
274 | 126 | elrab 3649 |
. . . . . . . . . . . . . . 15
β’ (π β {π£ β βͺ π β£ (π Γ {π£}) β π₯} β (π β βͺ π β§ (π Γ {π}) β π₯)) |
275 | 274 | simprbi 498 |
. . . . . . . . . . . . . 14
β’ (π β {π£ β βͺ π β£ (π Γ {π£}) β π₯} β (π Γ {π}) β π₯) |
276 | | simprr2 1223 |
. . . . . . . . . . . . . . . 16
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β π’ β π ) |
277 | 276 | sselda 3948 |
. . . . . . . . . . . . . . 15
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ π β π’) β π β π ) |
278 | | vsnid 4627 |
. . . . . . . . . . . . . . 15
β’ π β {π} |
279 | | opelxpi 5674 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β {π}) β β¨π, πβ© β (π Γ {π})) |
280 | 277, 278,
279 | sylancl 587 |
. . . . . . . . . . . . . 14
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ π β π’) β β¨π, πβ© β (π Γ {π})) |
281 | | ssel 3941 |
. . . . . . . . . . . . . 14
β’ ((π Γ {π}) β π₯ β (β¨π, πβ© β (π Γ {π}) β β¨π, πβ© β π₯)) |
282 | 275, 280,
281 | syl2imc 41 |
. . . . . . . . . . . . 13
β’
((((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β§ π β π’) β (π β {π£ β βͺ π β£ (π Γ {π£}) β π₯} β β¨π, πβ© β π₯)) |
283 | 282 | expimpd 455 |
. . . . . . . . . . . 12
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β ((π β π’ β§ π β {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β β¨π, πβ© β π₯)) |
284 | 273, 283 | biimtrid 241 |
. . . . . . . . . . 11
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β (β¨π, πβ© β (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β β¨π, πβ© β π₯)) |
285 | 272, 284 | relssdv 5748 |
. . . . . . . . . 10
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β π₯) |
286 | | eleq2 2823 |
. . . . . . . . . . . 12
β’ (π‘ = (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β (π¦ β π‘ β π¦ β (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}))) |
287 | | sseq1 3973 |
. . . . . . . . . . . 12
β’ (π‘ = (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β (π‘ β π₯ β (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β π₯)) |
288 | 286, 287 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π‘ = (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β ((π¦ β π‘ β§ π‘ β π₯) β (π¦ β (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β§ (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β π₯))) |
289 | 288 | rspcev 3583 |
. . . . . . . . . 10
β’ (((π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β (π
Γt π) β§ (π¦ β (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β§ (π’ Γ {π£ β βͺ π β£ (π Γ {π£}) β π₯}) β π₯)) β βπ‘ β (π
Γt π)(π¦ β π‘ β§ π‘ β π₯)) |
290 | 245, 270,
285, 289 | syl12anc 836 |
. . . . . . . . 9
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ ((π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
) β§ ((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp))) β βπ‘ β (π
Γt π)(π¦ β π‘ β§ π‘ β π₯)) |
291 | 290 | expr 458 |
. . . . . . . 8
β’
(((((π
β
π-Locally Comp β§ π β (ran πGen β© Haus)) β§
π₯ β
(πGenβ(π
Γt π)))
β§ π¦ β π₯) β§ (π β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯} β§ π’ β π
)) β (((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp) β βπ‘ β (π
Γt π)(π¦ β π‘ β§ π‘ β π₯))) |
292 | 291 | rexlimdvva 3202 |
. . . . . . 7
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β (βπ β π« {π‘ β βͺ π
β£ β¨π‘, (2nd βπ¦)β© β π₯}βπ’ β π
((1st βπ¦) β π’ β§ π’ β π β§ (π
βΎt π ) β Comp) β βπ‘ β (π
Γt π)(π¦ β π‘ β§ π‘ β π₯))) |
293 | 63, 292 | mpd 15 |
. . . . . 6
β’ ((((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β§ π¦ β π₯) β βπ‘ β (π
Γt π)(π¦ β π‘ β§ π‘ β π₯)) |
294 | 293 | ralrimiva 3140 |
. . . . 5
β’ (((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β βπ¦ β π₯ βπ‘ β (π
Γt π)(π¦ β π‘ β§ π‘ β π₯)) |
295 | 6 | adantr 482 |
. . . . . 6
β’ (((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β (π
Γt π) β Top) |
296 | | eltop2 22348 |
. . . . . 6
β’ ((π
Γt π) β Top β (π₯ β (π
Γt π) β βπ¦ β π₯ βπ‘ β (π
Γt π)(π¦ β π‘ β§ π‘ β π₯))) |
297 | 295, 296 | syl 17 |
. . . . 5
β’ (((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β (π₯ β (π
Γt π) β βπ¦ β π₯ βπ‘ β (π
Γt π)(π¦ β π‘ β§ π‘ β π₯))) |
298 | 294, 297 | mpbird 257 |
. . . 4
β’ (((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β§ π₯ β (πGenβ(π
Γt π))) β π₯ β (π
Γt π)) |
299 | 298 | ex 414 |
. . 3
β’ ((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β (π₯ β (πGenβ(π
Γt π)) β π₯ β (π
Γt π))) |
300 | 299 | ssrdv 3954 |
. 2
β’ ((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β (πGenβ(π
Γt π)) β (π
Γt π)) |
301 | | iskgen2 22922 |
. 2
β’ ((π
Γt π) β ran πGen β
((π
Γt
π) β Top β§
(πGenβ(π
Γt π))
β (π
Γt π))) |
302 | 6, 300, 301 | sylanbrc 584 |
1
β’ ((π
β π-Locally Comp
β§ π β (ran
πGen β© Haus)) β (π
Γt π) β ran πGen) |