Step | Hyp | Ref
| Expression |
1 | | conntop 22791 |
. . 3
β’ (π
β Conn β π
β Top) |
2 | | conntop 22791 |
. . 3
β’ (π β Conn β π β Top) |
3 | | txtop 22943 |
. . 3
β’ ((π
β Top β§ π β Top) β (π
Γt π) β Top) |
4 | 1, 2, 3 | syl2an 597 |
. 2
β’ ((π
β Conn β§ π β Conn) β (π
Γt π) β Top) |
5 | | neq0 4309 |
. . . . . . 7
β’ (Β¬
π₯ = β
β
βπ§ π§ β π₯) |
6 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ π§ β π₯) β π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) |
7 | 6 | elin1d 4162 |
. . . . . . . . . . 11
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ π§ β π₯) β π₯ β (π
Γt π)) |
8 | | elssuni 4902 |
. . . . . . . . . . 11
β’ (π₯ β (π
Γt π) β π₯ β βͺ (π
Γt π)) |
9 | 7, 8 | syl 17 |
. . . . . . . . . 10
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ π§ β π₯) β π₯ β βͺ (π
Γt π)) |
10 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π€ β βͺ (π
Γt π)) |
11 | | simplll 774 |
. . . . . . . . . . . . . . . . 17
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π
β Conn) |
12 | 11, 1 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π
β Top) |
13 | | simpllr 775 |
. . . . . . . . . . . . . . . . 17
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π β Conn) |
14 | 13, 2 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π β Top) |
15 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ βͺ π
=
βͺ π
|
16 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ βͺ π =
βͺ π |
17 | 15, 16 | txuni 22966 |
. . . . . . . . . . . . . . . 16
β’ ((π
β Top β§ π β Top) β (βͺ π
Γ βͺ π) = βͺ (π
Γt π)) |
18 | 12, 14, 17 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (βͺ π
Γ βͺ π) = βͺ (π
Γt π)) |
19 | 10, 18 | eleqtrrd 2837 |
. . . . . . . . . . . . . 14
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π€ β (βͺ π
Γ βͺ π)) |
20 | | 1st2nd2 7964 |
. . . . . . . . . . . . . 14
β’ (π€ β (βͺ π
Γ βͺ π) β π€ = β¨(1st βπ€), (2nd βπ€)β©) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π€ = β¨(1st βπ€), (2nd βπ€)β©) |
22 | | xp2nd 7958 |
. . . . . . . . . . . . . . . 16
β’ (π€ β (βͺ π
Γ βͺ π) β (2nd βπ€) β βͺ π) |
23 | 19, 22 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (2nd
βπ€) β βͺ π) |
24 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ (π β βͺ π
β¦ β¨(1st βπ€), πβ©) = (π β βͺ π β¦ β¨(1st
βπ€), πβ©) |
25 | 24 | mptpreima 6194 |
. . . . . . . . . . . . . . . . 17
β’ (β‘(π β βͺ π β¦ β¨(1st
βπ€), πβ©) β π₯) = {π β βͺ π β£ β¨(1st
βπ€), πβ© β π₯} |
26 | | toptopon2 22290 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β Top β π β (TopOnββͺ π)) |
27 | 14, 26 | sylib 217 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π β (TopOnββͺ π)) |
28 | | toptopon2 22290 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π
β Top β π
β (TopOnββͺ π
)) |
29 | 12, 28 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π
β (TopOnββͺ π
)) |
30 | | xp1st 7957 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β (βͺ π
Γ βͺ π) β (1st βπ€) β βͺ π
) |
31 | 19, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (1st
βπ€) β βͺ π
) |
32 | 27, 29, 31 | cnmptc 23036 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (π β βͺ π β¦ (1st
βπ€)) β (π Cn π
)) |
33 | 27 | cnmptid 23035 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (π β βͺ π β¦ π) β (π Cn π)) |
34 | 27, 32, 33 | cnmpt1t 23039 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (π β βͺ π β¦ β¨(1st
βπ€), πβ©) β (π Cn (π
Γt π))) |
35 | | simplr 768 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) |
36 | 35 | elin1d 4162 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π₯ β (π
Γt π)) |
37 | | cnima 22639 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β βͺ π
β¦ β¨(1st βπ€), πβ©) β (π Cn (π
Γt π)) β§ π₯ β (π
Γt π)) β (β‘(π β βͺ π β¦ β¨(1st
βπ€), πβ©) β π₯) β π) |
38 | 34, 36, 37 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (β‘(π β βͺ π β¦ β¨(1st
βπ€), πβ©) β π₯) β π) |
39 | 25, 38 | eqeltrrid 2839 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β {π β βͺ π β£ β¨(1st
βπ€), πβ© β π₯} β π) |
40 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π§ β π₯) |
41 | | elunii 4874 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π§ β π₯ β§ π₯ β (π
Γt π)) β π§ β βͺ (π
Γt π)) |
42 | 40, 36, 41 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π§ β βͺ (π
Γt π)) |
43 | 42, 18 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π§ β (βͺ π
Γ βͺ π)) |
44 | | xp2nd 7958 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β (βͺ π
Γ βͺ π) β (2nd βπ§) β βͺ π) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (2nd
βπ§) β βͺ π) |
46 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β βͺ π
β¦ β¨π,
(2nd βπ§)β©) = (π β βͺ π
β¦ β¨π, (2nd βπ§)β©) |
47 | 46 | mptpreima 6194 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (β‘(π β βͺ π
β¦ β¨π, (2nd βπ§)β©) β π₯) = {π β βͺ π
β£ β¨π, (2nd βπ§)β© β π₯} |
48 | 29 | cnmptid 23035 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (π β βͺ π
β¦ π) β (π
Cn π
)) |
49 | 29, 27, 45 | cnmptc 23036 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (π β βͺ π
β¦ (2nd
βπ§)) β (π
Cn π)) |
50 | 29, 48, 49 | cnmpt1t 23039 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (π β βͺ π
β¦ β¨π, (2nd βπ§)β©) β (π
Cn (π
Γt π))) |
51 | | cnima 22639 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β βͺ π
β¦ β¨π,
(2nd βπ§)β©) β (π
Cn (π
Γt π)) β§ π₯ β (π
Γt π)) β (β‘(π β βͺ π
β¦ β¨π, (2nd βπ§)β©) β π₯) β π
) |
52 | 50, 36, 51 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (β‘(π β βͺ π
β¦ β¨π, (2nd βπ§)β©) β π₯) β π
) |
53 | 47, 52 | eqeltrrid 2839 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β {π β βͺ π
β£ β¨π, (2nd βπ§)β© β π₯} β π
) |
54 | | xp1st 7957 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π§ β (βͺ π
Γ βͺ π) β (1st βπ§) β βͺ π
) |
55 | 43, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (1st
βπ§) β βͺ π
) |
56 | | 1st2nd2 7964 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π§ β (βͺ π
Γ βͺ π) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
57 | 43, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π§ = β¨(1st βπ§), (2nd βπ§)β©) |
58 | 57, 40 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β β¨(1st
βπ§), (2nd
βπ§)β© β
π₯) |
59 | | opeq1 4834 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (1st βπ§) β β¨π, (2nd βπ§)β© = β¨(1st
βπ§), (2nd
βπ§)β©) |
60 | 59 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (1st βπ§) β (β¨π, (2nd βπ§)β© β π₯ β β¨(1st
βπ§), (2nd
βπ§)β© β
π₯)) |
61 | 60 | rspcev 3583 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((1st βπ§) β βͺ π
β§ β¨(1st
βπ§), (2nd
βπ§)β© β
π₯) β βπ β βͺ π
β¨π, (2nd βπ§)β© β π₯) |
62 | 55, 58, 61 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β βπ β βͺ π
β¨π, (2nd βπ§)β© β π₯) |
63 | | rabn0 4349 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ({π β βͺ π
β£ β¨π,
(2nd βπ§)β© β π₯} β β
β βπ β βͺ π
β¨π, (2nd βπ§)β© β π₯) |
64 | 62, 63 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β {π β βͺ π
β£ β¨π, (2nd βπ§)β© β π₯} β β
) |
65 | 35 | elin2d 4163 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π₯ β (Clsdβ(π
Γt π))) |
66 | | cnclima 22642 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β βͺ π
β¦ β¨π,
(2nd βπ§)β©) β (π
Cn (π
Γt π)) β§ π₯ β (Clsdβ(π
Γt π))) β (β‘(π β βͺ π
β¦ β¨π, (2nd βπ§)β©) β π₯) β (Clsdβπ
)) |
67 | 50, 65, 66 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (β‘(π β βͺ π
β¦ β¨π, (2nd βπ§)β©) β π₯) β (Clsdβπ
)) |
68 | 47, 67 | eqeltrrid 2839 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β {π β βͺ π
β£ β¨π, (2nd βπ§)β© β π₯} β (Clsdβπ
)) |
69 | 15, 11, 53, 64, 68 | connclo 22789 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β {π β βͺ π
β£ β¨π, (2nd βπ§)β© β π₯} = βͺ
π
) |
70 | 31, 69 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (1st
βπ€) β {π β βͺ π
β£ β¨π,
(2nd βπ§)β© β π₯}) |
71 | | opeq1 4834 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (1st βπ€) β β¨π, (2nd βπ§)β© = β¨(1st
βπ€), (2nd
βπ§)β©) |
72 | 71 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (1st βπ€) β (β¨π, (2nd βπ§)β© β π₯ β β¨(1st
βπ€), (2nd
βπ§)β© β
π₯)) |
73 | 72 | elrab 3649 |
. . . . . . . . . . . . . . . . . . . 20
β’
((1st βπ€) β {π β βͺ π
β£ β¨π, (2nd βπ§)β© β π₯} β ((1st
βπ€) β βͺ π
β§ β¨(1st βπ€), (2nd βπ§)β© β π₯)) |
74 | 73 | simprbi 498 |
. . . . . . . . . . . . . . . . . . 19
β’
((1st βπ€) β {π β βͺ π
β£ β¨π, (2nd βπ§)β© β π₯} β β¨(1st
βπ€), (2nd
βπ§)β© β
π₯) |
75 | 70, 74 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β β¨(1st
βπ€), (2nd
βπ§)β© β
π₯) |
76 | | opeq2 4835 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = (2nd βπ§) β β¨(1st
βπ€), πβ© = β¨(1st
βπ€), (2nd
βπ§)β©) |
77 | 76 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (2nd βπ§) β (β¨(1st
βπ€), πβ© β π₯ β β¨(1st βπ€), (2nd βπ§)β© β π₯)) |
78 | 77 | rspcev 3583 |
. . . . . . . . . . . . . . . . . 18
β’
(((2nd βπ§) β βͺ π β§ β¨(1st
βπ€), (2nd
βπ§)β© β
π₯) β βπ β βͺ πβ¨(1st βπ€), πβ© β π₯) |
79 | 45, 75, 78 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β βπ β βͺ πβ¨(1st βπ€), πβ© β π₯) |
80 | | rabn0 4349 |
. . . . . . . . . . . . . . . . 17
β’ ({π β βͺ π
β£ β¨(1st βπ€), πβ© β π₯} β β
β βπ β βͺ πβ¨(1st βπ€), πβ© β π₯) |
81 | 79, 80 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β {π β βͺ π β£ β¨(1st
βπ€), πβ© β π₯} β β
) |
82 | | cnclima 22642 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β βͺ π
β¦ β¨(1st βπ€), πβ©) β (π Cn (π
Γt π)) β§ π₯ β (Clsdβ(π
Γt π))) β (β‘(π β βͺ π β¦ β¨(1st
βπ€), πβ©) β π₯) β (Clsdβπ)) |
83 | 34, 65, 82 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (β‘(π β βͺ π β¦ β¨(1st
βπ€), πβ©) β π₯) β (Clsdβπ)) |
84 | 25, 83 | eqeltrrid 2839 |
. . . . . . . . . . . . . . . 16
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β {π β βͺ π β£ β¨(1st
βπ€), πβ© β π₯} β (Clsdβπ)) |
85 | 16, 13, 39, 81, 84 | connclo 22789 |
. . . . . . . . . . . . . . 15
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β {π β βͺ π β£ β¨(1st
βπ€), πβ© β π₯} = βͺ π) |
86 | 23, 85 | eleqtrrd 2837 |
. . . . . . . . . . . . . 14
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β (2nd
βπ€) β {π β βͺ π
β£ β¨(1st βπ€), πβ© β π₯}) |
87 | | opeq2 4835 |
. . . . . . . . . . . . . . . . 17
β’ (π = (2nd βπ€) β β¨(1st
βπ€), πβ© = β¨(1st
βπ€), (2nd
βπ€)β©) |
88 | 87 | eleq1d 2819 |
. . . . . . . . . . . . . . . 16
β’ (π = (2nd βπ€) β (β¨(1st
βπ€), πβ© β π₯ β β¨(1st βπ€), (2nd βπ€)β© β π₯)) |
89 | 88 | elrab 3649 |
. . . . . . . . . . . . . . 15
β’
((2nd βπ€) β {π β βͺ π β£ β¨(1st
βπ€), πβ© β π₯} β ((2nd βπ€) β βͺ π
β§ β¨(1st βπ€), (2nd βπ€)β© β π₯)) |
90 | 89 | simprbi 498 |
. . . . . . . . . . . . . 14
β’
((2nd βπ€) β {π β βͺ π β£ β¨(1st
βπ€), πβ© β π₯} β β¨(1st βπ€), (2nd βπ€)β© β π₯) |
91 | 86, 90 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β β¨(1st
βπ€), (2nd
βπ€)β© β
π₯) |
92 | 21, 91 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ (π§ β π₯ β§ π€ β βͺ (π
Γt π))) β π€ β π₯) |
93 | 92 | expr 458 |
. . . . . . . . . . 11
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ π§ β π₯) β (π€ β βͺ (π
Γt π) β π€ β π₯)) |
94 | 93 | ssrdv 3954 |
. . . . . . . . . 10
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ π§ β π₯) β βͺ (π
Γt π) β π₯) |
95 | 9, 94 | eqssd 3965 |
. . . . . . . . 9
β’ ((((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β§ π§ β π₯) β π₯ = βͺ (π
Γt π)) |
96 | 95 | ex 414 |
. . . . . . . 8
β’ (((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β (π§ β π₯ β π₯ = βͺ (π
Γt π))) |
97 | 96 | exlimdv 1937 |
. . . . . . 7
β’ (((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β (βπ§ π§ β π₯ β π₯ = βͺ (π
Γt π))) |
98 | 5, 97 | biimtrid 241 |
. . . . . 6
β’ (((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β (Β¬ π₯ = β
β π₯ = βͺ (π
Γt π))) |
99 | 98 | orrd 862 |
. . . . 5
β’ (((π
β Conn β§ π β Conn) β§ π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π)))) β (π₯ = β
β¨ π₯ = βͺ (π
Γt π))) |
100 | 99 | ex 414 |
. . . 4
β’ ((π
β Conn β§ π β Conn) β (π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π))) β (π₯ = β
β¨ π₯ = βͺ (π
Γt π)))) |
101 | | vex 3451 |
. . . . 5
β’ π₯ β V |
102 | 101 | elpr 4613 |
. . . 4
β’ (π₯ β {β
, βͺ (π
Γt π)}
β (π₯ = β
β¨
π₯ = βͺ (π
Γt π))) |
103 | 100, 102 | syl6ibr 252 |
. . 3
β’ ((π
β Conn β§ π β Conn) β (π₯ β ((π
Γt π) β© (Clsdβ(π
Γt π))) β π₯ β {β
, βͺ (π
Γt π)})) |
104 | 103 | ssrdv 3954 |
. 2
β’ ((π
β Conn β§ π β Conn) β ((π
Γt π) β© (Clsdβ(π
Γt π))) β {β
, βͺ (π
Γt π)}) |
105 | | eqid 2733 |
. . 3
β’ βͺ (π
Γt π) =
βͺ (π
Γt π) |
106 | 105 | isconn2 22788 |
. 2
β’ ((π
Γt π) β Conn β ((π
Γt π) β Top β§ ((π
Γt π) β© (Clsdβ(π
Γt π))) β {β
, βͺ (π
Γt π)})) |
107 | 4, 104, 106 | sylanbrc 584 |
1
β’ ((π
β Conn β§ π β Conn) β (π
Γt π) β Conn) |