Step | Hyp | Ref
| Expression |
1 | | conntop 22768 |
. . 3
β’ (π½ β Conn β π½ β Top) |
2 | 1 | adantr 481 |
. 2
β’ ((π½ β Conn β§ π½ β π-Locally PConn)
β π½ β
Top) |
3 | | eqid 2736 |
. . . . . 6
β’ βͺ π½ =
βͺ π½ |
4 | | simpll 765 |
. . . . . 6
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β π½ β
Conn) |
5 | | inss1 4188 |
. . . . . . 7
β’ (π½ β© (Clsdβπ½)) β π½ |
6 | | simplr 767 |
. . . . . . . . . . . 12
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β π½ β
π-Locally PConn) |
7 | 1 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β π½ β
Top) |
8 | 3 | topopn 22255 |
. . . . . . . . . . . . 13
β’ (π½ β Top β βͺ π½
β π½) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . . 12
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β βͺ π½ β π½) |
10 | | simprr 771 |
. . . . . . . . . . . 12
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β π§ β βͺ π½) |
11 | | nlly2i 22827 |
. . . . . . . . . . . 12
β’ ((π½ β π-Locally PConn
β§ βͺ π½ β π½ β§ π§ β βͺ π½) β βπ β π« βͺ π½βπ’ β π½ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn)) |
12 | 6, 9, 10, 11 | syl3anc 1371 |
. . . . . . . . . . 11
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β βπ β
π« βͺ π½βπ’ β π½ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn)) |
13 | | simprr1 1221 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β§ (π β π«
βͺ π½ β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β π§ β π’) |
14 | | eqeq2 2748 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π¦ = π€ β ((πβ1) = π¦ β (πβ1) = π€)) |
15 | 14 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π€ β (((πβ0) = π₯ β§ (πβ1) = π¦) β ((πβ0) = π₯ β§ (πβ1) = π€))) |
16 | 15 | rexbidv 3175 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π€ β (βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦) β βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π€))) |
17 | 16 | elrab 3645 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β (π€ β βͺ π½ β§ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π€))) |
18 | 17 | simprbi 497 |
. . . . . . . . . . . . . . . . 17
β’ (π€ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π€)) |
19 | | simprr3 1223 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β§ (π β π«
βͺ π½ β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β (π½ βΎt π ) β PConn) |
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β (π½ βΎt π ) β PConn) |
21 | | simprr2 1222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β§ (π β π«
βͺ π½ β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β π’ β π ) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β π’ β π ) |
23 | | simprll 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β π€ β π’) |
24 | 22, 23 | sseldd 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β π€ β π ) |
25 | 7 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β π½ β Top) |
26 | | elpwi 4567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π« βͺ π½
β π β βͺ π½) |
27 | 26 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β§ (π β π«
βͺ π½ β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β π β βͺ π½) |
28 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β π β βͺ π½) |
29 | 3 | restuni 22513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π½ β Top β§ π β βͺ π½)
β π = βͺ (π½
βΎt π )) |
30 | 25, 28, 29 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β π = βͺ (π½ βΎt π )) |
31 | 24, 30 | eleqtrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β π€ β βͺ (π½ βΎt π )) |
32 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β π¦ β π’) |
33 | 22, 32 | sseldd 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β π¦ β π ) |
34 | 33, 30 | eleqtrd 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β π¦ β βͺ (π½ βΎt π )) |
35 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ βͺ (π½
βΎt π ) =
βͺ (π½ βΎt π ) |
36 | 35 | pconncn 33818 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π½ βΎt π ) β PConn β§ π€ β βͺ (π½
βΎt π )
β§ π¦ β βͺ (π½
βΎt π ))
β ββ β (II
Cn (π½ βΎt
π ))((ββ0) = π€ β§ (ββ1) = π¦)) |
37 | 20, 31, 34, 36 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β ββ β (II Cn (π½ βΎt π ))((ββ0) = π€ β§ (ββ1) = π¦)) |
38 | | simplrl 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’) β π β (II Cn π½)) |
39 | 38 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β π β (II Cn π½)) |
40 | 25 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β π½ β Top) |
41 | | cnrest2r 22638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π½ β Top β (II Cn (π½ βΎt π )) β (II Cn π½)) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β (II Cn (π½ βΎt π )) β (II Cn π½)) |
43 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β β β (II Cn (π½ βΎt π ))) |
44 | 42, 43 | sseldd 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β β β (II Cn π½)) |
45 | | simplrr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’) β ((πβ0) = π₯ β§ (πβ1) = π€)) |
46 | 45 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β ((πβ0) = π₯ β§ (πβ1) = π€)) |
47 | 46 | simprd 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β (πβ1) = π€) |
48 | | simprrl 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β (ββ0) = π€) |
49 | 47, 48 | eqtr4d 2779 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β (πβ1) = (ββ0)) |
50 | 39, 44, 49 | pcocn 24380 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β (π(*πβπ½)β) β (II Cn π½)) |
51 | 39, 44 | pco0 24377 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β ((π(*πβπ½)β)β0) = (πβ0)) |
52 | 46 | simpld 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β (πβ0) = π₯) |
53 | 51, 52 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β ((π(*πβπ½)β)β0) = π₯) |
54 | 39, 44 | pco1 24378 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β ((π(*πβπ½)β)β1) = (ββ1)) |
55 | | simprrr 780 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β (ββ1) = π¦) |
56 | 54, 55 | eqtrd 2776 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β ((π(*πβπ½)β)β1) = π¦) |
57 | | fveq1 6841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = (π(*πβπ½)β) β (πβ0) = ((π(*πβπ½)β)β0)) |
58 | 57 | eqeq1d 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = (π(*πβπ½)β) β ((πβ0) = π₯ β ((π(*πβπ½)β)β0) = π₯)) |
59 | | fveq1 6841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = (π(*πβπ½)β) β (πβ1) = ((π(*πβπ½)β)β1)) |
60 | 59 | eqeq1d 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = (π(*πβπ½)β) β ((πβ1) = π¦ β ((π(*πβπ½)β)β1) = π¦)) |
61 | 58, 60 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (π(*πβπ½)β) β (((πβ0) = π₯ β§ (πβ1) = π¦) β (((π(*πβπ½)β)β0) = π₯ β§ ((π(*πβπ½)β)β1) = π¦))) |
62 | 61 | rspcev 3581 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π(*πβπ½)β) β (II Cn π½) β§ (((π(*πβπ½)β)β0) = π₯ β§ ((π(*πβπ½)β)β1) = π¦)) β βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)) |
63 | 50, 53, 56, 62 | syl12anc 835 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β§ (β β (II Cn (π½ βΎt π )) β§ ((ββ0) = π€ β§ (ββ1) = π¦))) β βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)) |
64 | 37, 63 | rexlimddv 3158 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ ((π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β§ π¦ β π’)) β βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)) |
65 | 64 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ (π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€)))) β§ π¦ β π’) β βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)) |
66 | 65 | ralrimiva 3143 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ (π€ β π’ β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€)))) β βπ¦ β π’ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)) |
67 | 66 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ π€ β π’) β§ (π β (II Cn π½) β§ ((πβ0) = π₯ β§ (πβ1) = π€))) β βπ¦ β π’ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)) |
68 | 67 | rexlimdvaa 3153 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ π€ β π’) β (βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π€) β βπ¦ β π’ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦))) |
69 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ π€ β π’) β π’ β π ) |
70 | | simplrl 775 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ π€ β π’) β π β π« βͺ π½) |
71 | 70, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ π€ β π’) β π β βͺ π½) |
72 | 69, 71 | sstrd 3954 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ π€ β π’) β π’ β βͺ π½) |
73 | 68, 72 | jctild 526 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ π€ β π’) β (βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π€) β (π’ β βͺ π½ β§ βπ¦ β π’ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)))) |
74 | | fveq1 6841 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (πβ0) = (πβ0)) |
75 | 74 | eqeq1d 2738 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((πβ0) = π₯ β (πβ0) = π₯)) |
76 | | fveq1 6841 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (πβ1) = (πβ1)) |
77 | 76 | eqeq1d 2738 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((πβ1) = π€ β (πβ1) = π€)) |
78 | 75, 77 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (((πβ0) = π₯ β§ (πβ1) = π€) β ((πβ0) = π₯ β§ (πβ1) = π€))) |
79 | 78 | cbvrexvw 3226 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β (II
Cn π½)((πβ0) = π₯ β§ (πβ1) = π€) β βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π€)) |
80 | | ssrab 4030 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β (π’ β βͺ π½ β§ βπ¦ β π’ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦))) |
81 | 73, 79, 80 | 3imtr4g 295 |
. . . . . . . . . . . . . . . . 17
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ π€ β π’) β (βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π€) β π’ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)})) |
82 | 18, 81 | syl5 34 |
. . . . . . . . . . . . . . . 16
β’
(((((π½ β Conn
β§ π½ β
π-Locally PConn) β§ (π₯ β βͺ π½ β§ π§ β βͺ π½)) β§ (π β π« βͺ π½
β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β§ π€ β π’) β (π€ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β π’ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)})) |
83 | 82 | ralrimiva 3143 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β§ (π β π«
βͺ π½ β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β βπ€ β π’ (π€ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β π’ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)})) |
84 | 13, 83 | jca 512 |
. . . . . . . . . . . . . 14
β’ ((((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β§ (π β π«
βͺ π½ β§ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn))) β (π§ β π’ β§ βπ€ β π’ (π€ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β π’ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)}))) |
85 | 84 | expr 457 |
. . . . . . . . . . . . 13
β’ ((((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β§ π β π«
βͺ π½) β ((π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn) β (π§ β π’ β§ βπ€ β π’ (π€ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β π’ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)})))) |
86 | 85 | reximdv 3167 |
. . . . . . . . . . . 12
β’ ((((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β§ π β π«
βͺ π½) β (βπ’ β π½ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn) β βπ’ β π½ (π§ β π’ β§ βπ€ β π’ (π€ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β π’ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)})))) |
87 | 86 | rexlimdva 3152 |
. . . . . . . . . . 11
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β (βπ β
π« βͺ π½βπ’ β π½ (π§ β π’ β§ π’ β π β§ (π½ βΎt π ) β PConn) β βπ’ β π½ (π§ β π’ β§ βπ€ β π’ (π€ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β π’ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)})))) |
88 | 12, 87 | mpd 15 |
. . . . . . . . . 10
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ (π₯ β βͺ π½
β§ π§ β βͺ π½))
β βπ’ β
π½ (π§ β π’ β§ βπ€ β π’ (π€ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β π’ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)}))) |
89 | 88 | anassrs 468 |
. . . . . . . . 9
β’ ((((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β§ π§ β βͺ π½)
β βπ’ β
π½ (π§ β π’ β§ βπ€ β π’ (π€ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β π’ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)}))) |
90 | 89 | ralrimiva 3143 |
. . . . . . . 8
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β βπ§ β
βͺ π½βπ’ β π½ (π§ β π’ β§ βπ€ β π’ (π€ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β π’ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)}))) |
91 | 1 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β π½ β
Top) |
92 | | ssrab2 4037 |
. . . . . . . . 9
β’ {π¦ β βͺ π½
β£ βπ β (II
Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β βͺ π½ |
93 | 3 | isclo2 22439 |
. . . . . . . . 9
β’ ((π½ β Top β§ {π¦ β βͺ π½
β£ βπ β (II
Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β βͺ π½) β ({π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β (π½ β© (Clsdβπ½)) β βπ§ β βͺ π½βπ’ β π½ (π§ β π’ β§ βπ€ β π’ (π€ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β π’ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)})))) |
94 | 91, 92, 93 | sylancl 586 |
. . . . . . . 8
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β ({π¦ β βͺ π½
β£ βπ β (II
Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β (π½ β© (Clsdβπ½)) β βπ§ β βͺ π½βπ’ β π½ (π§ β π’ β§ βπ€ β π’ (π€ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β π’ β {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)})))) |
95 | 90, 94 | mpbird 256 |
. . . . . . 7
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β {π¦ β βͺ π½
β£ βπ β (II
Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β (π½ β© (Clsdβπ½))) |
96 | 5, 95 | sselid 3942 |
. . . . . 6
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β {π¦ β βͺ π½
β£ βπ β (II
Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β π½) |
97 | | simpr 485 |
. . . . . . . 8
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β π₯ β βͺ π½) |
98 | | iitopon 24242 |
. . . . . . . . . 10
β’ II β
(TopOnβ(0[,]1)) |
99 | 98 | a1i 11 |
. . . . . . . . 9
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β II β (TopOnβ(0[,]1))) |
100 | 3 | toptopon 22266 |
. . . . . . . . . 10
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
101 | 91, 100 | sylib 217 |
. . . . . . . . 9
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β π½ β
(TopOnββͺ π½)) |
102 | | cnconst2 22634 |
. . . . . . . . 9
β’ ((II
β (TopOnβ(0[,]1)) β§ π½ β (TopOnββͺ π½)
β§ π₯ β βͺ π½)
β ((0[,]1) Γ {π₯}) β (II Cn π½)) |
103 | 99, 101, 97, 102 | syl3anc 1371 |
. . . . . . . 8
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β ((0[,]1) Γ {π₯}) β (II Cn π½)) |
104 | | 0elunit 13386 |
. . . . . . . . 9
β’ 0 β
(0[,]1) |
105 | | vex 3449 |
. . . . . . . . . 10
β’ π₯ β V |
106 | 105 | fvconst2 7153 |
. . . . . . . . 9
β’ (0 β
(0[,]1) β (((0[,]1) Γ {π₯})β0) = π₯) |
107 | 104, 106 | mp1i 13 |
. . . . . . . 8
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β (((0[,]1) Γ {π₯})β0) = π₯) |
108 | | 1elunit 13387 |
. . . . . . . . 9
β’ 1 β
(0[,]1) |
109 | 105 | fvconst2 7153 |
. . . . . . . . 9
β’ (1 β
(0[,]1) β (((0[,]1) Γ {π₯})β1) = π₯) |
110 | 108, 109 | mp1i 13 |
. . . . . . . 8
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β (((0[,]1) Γ {π₯})β1) = π₯) |
111 | | eqeq2 2748 |
. . . . . . . . . 10
β’ (π¦ = π₯ β ((πβ1) = π¦ β (πβ1) = π₯)) |
112 | 111 | anbi2d 629 |
. . . . . . . . 9
β’ (π¦ = π₯ β (((πβ0) = π₯ β§ (πβ1) = π¦) β ((πβ0) = π₯ β§ (πβ1) = π₯))) |
113 | | fveq1 6841 |
. . . . . . . . . . 11
β’ (π = ((0[,]1) Γ {π₯}) β (πβ0) = (((0[,]1) Γ {π₯})β0)) |
114 | 113 | eqeq1d 2738 |
. . . . . . . . . 10
β’ (π = ((0[,]1) Γ {π₯}) β ((πβ0) = π₯ β (((0[,]1) Γ {π₯})β0) = π₯)) |
115 | | fveq1 6841 |
. . . . . . . . . . 11
β’ (π = ((0[,]1) Γ {π₯}) β (πβ1) = (((0[,]1) Γ {π₯})β1)) |
116 | 115 | eqeq1d 2738 |
. . . . . . . . . 10
β’ (π = ((0[,]1) Γ {π₯}) β ((πβ1) = π₯ β (((0[,]1) Γ {π₯})β1) = π₯)) |
117 | 114, 116 | anbi12d 631 |
. . . . . . . . 9
β’ (π = ((0[,]1) Γ {π₯}) β (((πβ0) = π₯ β§ (πβ1) = π₯) β ((((0[,]1) Γ {π₯})β0) = π₯ β§ (((0[,]1) Γ {π₯})β1) = π₯))) |
118 | 112, 117 | rspc2ev 3592 |
. . . . . . . 8
β’ ((π₯ β βͺ π½
β§ ((0[,]1) Γ {π₯})
β (II Cn π½) β§
((((0[,]1) Γ {π₯})β0) = π₯ β§ (((0[,]1) Γ {π₯})β1) = π₯)) β βπ¦ β βͺ π½βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)) |
119 | 97, 103, 107, 110, 118 | syl112anc 1374 |
. . . . . . 7
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β βπ¦ β
βͺ π½βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)) |
120 | | rabn0 4345 |
. . . . . . 7
β’ ({π¦ β βͺ π½
β£ βπ β (II
Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β β
β βπ¦ β βͺ π½βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)) |
121 | 119, 120 | sylibr 233 |
. . . . . 6
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β {π¦ β βͺ π½
β£ βπ β (II
Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β β
) |
122 | | inss2 4189 |
. . . . . . 7
β’ (π½ β© (Clsdβπ½)) β (Clsdβπ½) |
123 | 122, 95 | sselid 3942 |
. . . . . 6
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β {π¦ β βͺ π½
β£ βπ β (II
Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β (Clsdβπ½)) |
124 | 3, 4, 96, 121, 123 | connclo 22766 |
. . . . 5
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β {π¦ β βͺ π½
β£ βπ β (II
Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} = βͺ π½) |
125 | 124 | eqcomd 2742 |
. . . 4
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β βͺ π½ = {π¦ β βͺ π½ β£ βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)}) |
126 | | rabid2 3436 |
. . . 4
β’ (βͺ π½ =
{π¦ β βͺ π½
β£ βπ β (II
Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)} β βπ¦ β βͺ π½βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)) |
127 | 125, 126 | sylib 217 |
. . 3
β’ (((π½ β Conn β§ π½ β π-Locally PConn)
β§ π₯ β βͺ π½)
β βπ¦ β
βͺ π½βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)) |
128 | 127 | ralrimiva 3143 |
. 2
β’ ((π½ β Conn β§ π½ β π-Locally PConn)
β βπ₯ β
βͺ π½βπ¦ β βͺ π½βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦)) |
129 | 3 | ispconn 33817 |
. 2
β’ (π½ β PConn β (π½ β Top β§ βπ₯ β βͺ π½βπ¦ β βͺ π½βπ β (II Cn π½)((πβ0) = π₯ β§ (πβ1) = π¦))) |
130 | 2, 128, 129 | sylanbrc 583 |
1
β’ ((π½ β Conn β§ π½ β π-Locally PConn)
β π½ β
PConn) |