Step | Hyp | Ref
| Expression |
1 | | cnpf2 22617 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ)) β πΉ:πβΆπ) |
2 | 1 | 3expa 1119 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β πΉ:πβΆπ) |
3 | 2 | 3adantl3 1169 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β πΉ:πβΆπ) |
4 | | simplr 768 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β πΉ β ((π½ CnP πΎ)βπ)) |
5 | | simpll2 1214 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β πΎ β (TopOnβπ)) |
6 | | topontop 22278 |
. . . . . . . . 9
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
7 | 5, 6 | syl 17 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β πΎ β Top) |
8 | | eqid 2733 |
. . . . . . . . . 10
β’ βͺ πΎ =
βͺ πΎ |
9 | 8 | neii1 22473 |
. . . . . . . . 9
β’ ((πΎ β Top β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β π¦ β βͺ πΎ) |
10 | 7, 9 | sylancom 589 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β π¦ β βͺ πΎ) |
11 | 8 | ntropn 22416 |
. . . . . . . 8
β’ ((πΎ β Top β§ π¦ β βͺ πΎ)
β ((intβπΎ)βπ¦) β πΎ) |
12 | 7, 10, 11 | syl2anc 585 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β ((intβπΎ)βπ¦) β πΎ) |
13 | | simpr 486 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β π¦ β ((neiβπΎ)β{(πΉβπ)})) |
14 | 3 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β πΉ:πβΆπ) |
15 | | simpll3 1215 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β π β π) |
16 | 14, 15 | ffvelcdmd 7037 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β (πΉβπ) β π) |
17 | | toponuni 22279 |
. . . . . . . . . . . . 13
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
18 | 5, 17 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β π = βͺ πΎ) |
19 | 16, 18 | eleqtrd 2836 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β (πΉβπ) β βͺ πΎ) |
20 | 19 | snssd 4770 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β {(πΉβπ)} β βͺ
πΎ) |
21 | 8 | neiint 22471 |
. . . . . . . . . 10
β’ ((πΎ β Top β§ {(πΉβπ)} β βͺ
πΎ β§ π¦ β βͺ πΎ) β (π¦ β ((neiβπΎ)β{(πΉβπ)}) β {(πΉβπ)} β ((intβπΎ)βπ¦))) |
22 | 7, 20, 10, 21 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β (π¦ β ((neiβπΎ)β{(πΉβπ)}) β {(πΉβπ)} β ((intβπΎ)βπ¦))) |
23 | 13, 22 | mpbid 231 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β {(πΉβπ)} β ((intβπΎ)βπ¦)) |
24 | | fvex 6856 |
. . . . . . . . 9
β’ (πΉβπ) β V |
25 | 24 | snss 4747 |
. . . . . . . 8
β’ ((πΉβπ) β ((intβπΎ)βπ¦) β {(πΉβπ)} β ((intβπΎ)βπ¦)) |
26 | 23, 25 | sylibr 233 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β (πΉβπ) β ((intβπΎ)βπ¦)) |
27 | | cnpimaex 22623 |
. . . . . . 7
β’ ((πΉ β ((π½ CnP πΎ)βπ) β§ ((intβπΎ)βπ¦) β πΎ β§ (πΉβπ) β ((intβπΎ)βπ¦)) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β ((intβπΎ)βπ¦))) |
28 | 4, 12, 26, 27 | syl3anc 1372 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β ((intβπΎ)βπ¦))) |
29 | | simpl1 1192 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β π½ β (TopOnβπ)) |
30 | 29 | ad2antrr 725 |
. . . . . . . 8
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β§ (π₯ β π½ β§ (π β π₯ β§ (πΉ β π₯) β ((intβπΎ)βπ¦)))) β π½ β (TopOnβπ)) |
31 | | topontop 22278 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β π½ β Top) |
32 | 30, 31 | syl 17 |
. . . . . . 7
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β§ (π₯ β π½ β§ (π β π₯ β§ (πΉ β π₯) β ((intβπΎ)βπ¦)))) β π½ β Top) |
33 | | simprl 770 |
. . . . . . 7
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β§ (π₯ β π½ β§ (π β π₯ β§ (πΉ β π₯) β ((intβπΎ)βπ¦)))) β π₯ β π½) |
34 | | simprrl 780 |
. . . . . . 7
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β§ (π₯ β π½ β§ (π β π₯ β§ (πΉ β π₯) β ((intβπΎ)βπ¦)))) β π β π₯) |
35 | | opnneip 22486 |
. . . . . . 7
β’ ((π½ β Top β§ π₯ β π½ β§ π β π₯) β π₯ β ((neiβπ½)β{π})) |
36 | 32, 33, 34, 35 | syl3anc 1372 |
. . . . . 6
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β§ (π₯ β π½ β§ (π β π₯ β§ (πΉ β π₯) β ((intβπΎ)βπ¦)))) β π₯ β ((neiβπ½)β{π})) |
37 | | simprrr 781 |
. . . . . . 7
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β§ (π₯ β π½ β§ (π β π₯ β§ (πΉ β π₯) β ((intβπΎ)βπ¦)))) β (πΉ β π₯) β ((intβπΎ)βπ¦)) |
38 | 8 | ntrss2 22424 |
. . . . . . . . 9
β’ ((πΎ β Top β§ π¦ β βͺ πΎ)
β ((intβπΎ)βπ¦) β π¦) |
39 | 7, 10, 38 | syl2anc 585 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β ((intβπΎ)βπ¦) β π¦) |
40 | 39 | adantr 482 |
. . . . . . 7
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β§ (π₯ β π½ β§ (π β π₯ β§ (πΉ β π₯) β ((intβπΎ)βπ¦)))) β ((intβπΎ)βπ¦) β π¦) |
41 | 37, 40 | sstrd 3955 |
. . . . . 6
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β§ (π₯ β π½ β§ (π β π₯ β§ (πΉ β π₯) β ((intβπΎ)βπ¦)))) β (πΉ β π₯) β π¦) |
42 | 28, 36, 41 | reximssdv 3166 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β§ π¦ β ((neiβπΎ)β{(πΉβπ)})) β βπ₯ β ((neiβπ½)β{π})(πΉ β π₯) β π¦) |
43 | 42 | ralrimiva 3140 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β βπ¦ β ((neiβπΎ)β{(πΉβπ)})βπ₯ β ((neiβπ½)β{π})(πΉ β π₯) β π¦) |
44 | 3, 43 | jca 513 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ β ((π½ CnP πΎ)βπ)) β (πΉ:πβΆπ β§ βπ¦ β ((neiβπΎ)β{(πΉβπ)})βπ₯ β ((neiβπ½)β{π})(πΉ β π₯) β π¦)) |
45 | 44 | ex 414 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β ((neiβπΎ)β{(πΉβπ)})βπ₯ β ((neiβπ½)β{π})(πΉ β π₯) β π¦))) |
46 | | simpll2 1214 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β πΎ β (TopOnβπ)) |
47 | 46, 6 | syl 17 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β πΎ β Top) |
48 | | simprl 770 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β π¦ β πΎ) |
49 | | simprr 772 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β (πΉβπ) β π¦) |
50 | | opnneip 22486 |
. . . . . . . . . 10
β’ ((πΎ β Top β§ π¦ β πΎ β§ (πΉβπ) β π¦) β π¦ β ((neiβπΎ)β{(πΉβπ)})) |
51 | 47, 48, 49, 50 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β π¦ β ((neiβπΎ)β{(πΉβπ)})) |
52 | | simpl1 1192 |
. . . . . . . . . . . . . 14
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β π½ β (TopOnβπ)) |
53 | 52 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β π½ β (TopOnβπ)) |
54 | 53, 31 | syl 17 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β π½ β Top) |
55 | | simprl 770 |
. . . . . . . . . . . . 13
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β π₯ β ((neiβπ½)β{π})) |
56 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ βͺ π½ =
βͺ π½ |
57 | 56 | neii1 22473 |
. . . . . . . . . . . . 13
β’ ((π½ β Top β§ π₯ β ((neiβπ½)β{π})) β π₯ β βͺ π½) |
58 | 54, 55, 57 | syl2anc 585 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β π₯ β βͺ π½) |
59 | 56 | ntropn 22416 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ π₯ β βͺ π½)
β ((intβπ½)βπ₯) β π½) |
60 | 54, 58, 59 | syl2anc 585 |
. . . . . . . . . . 11
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β ((intβπ½)βπ₯) β π½) |
61 | | simpll3 1215 |
. . . . . . . . . . . . . . . . 17
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β π β π) |
62 | 61 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β π β π) |
63 | | toponuni 22279 |
. . . . . . . . . . . . . . . . 17
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
64 | 53, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β π = βͺ π½) |
65 | 62, 64 | eleqtrd 2836 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β π β βͺ π½) |
66 | 65 | snssd 4770 |
. . . . . . . . . . . . . 14
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β {π} β βͺ π½) |
67 | 56 | neiint 22471 |
. . . . . . . . . . . . . 14
β’ ((π½ β Top β§ {π} β βͺ π½
β§ π₯ β βͺ π½)
β (π₯ β
((neiβπ½)β{π}) β {π} β ((intβπ½)βπ₯))) |
68 | 54, 66, 58, 67 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β (π₯ β ((neiβπ½)β{π}) β {π} β ((intβπ½)βπ₯))) |
69 | 55, 68 | mpbid 231 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β {π} β ((intβπ½)βπ₯)) |
70 | | snssg 4745 |
. . . . . . . . . . . . 13
β’ (π β π β (π β ((intβπ½)βπ₯) β {π} β ((intβπ½)βπ₯))) |
71 | 62, 70 | syl 17 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β (π β ((intβπ½)βπ₯) β {π} β ((intβπ½)βπ₯))) |
72 | 69, 71 | mpbird 257 |
. . . . . . . . . . 11
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β π β ((intβπ½)βπ₯)) |
73 | 56 | ntrss2 22424 |
. . . . . . . . . . . . . 14
β’ ((π½ β Top β§ π₯ β βͺ π½)
β ((intβπ½)βπ₯) β π₯) |
74 | 54, 58, 73 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β ((intβπ½)βπ₯) β π₯) |
75 | | imass2 6055 |
. . . . . . . . . . . . 13
β’
(((intβπ½)βπ₯) β π₯ β (πΉ β ((intβπ½)βπ₯)) β (πΉ β π₯)) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β (πΉ β ((intβπ½)βπ₯)) β (πΉ β π₯)) |
77 | | simprr 772 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β (πΉ β π₯) β π¦) |
78 | 76, 77 | sstrd 3955 |
. . . . . . . . . . 11
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β (πΉ β ((intβπ½)βπ₯)) β π¦) |
79 | | eleq2 2823 |
. . . . . . . . . . . . 13
β’ (π§ = ((intβπ½)βπ₯) β (π β π§ β π β ((intβπ½)βπ₯))) |
80 | | imaeq2 6010 |
. . . . . . . . . . . . . 14
β’ (π§ = ((intβπ½)βπ₯) β (πΉ β π§) = (πΉ β ((intβπ½)βπ₯))) |
81 | 80 | sseq1d 3976 |
. . . . . . . . . . . . 13
β’ (π§ = ((intβπ½)βπ₯) β ((πΉ β π§) β π¦ β (πΉ β ((intβπ½)βπ₯)) β π¦)) |
82 | 79, 81 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π§ = ((intβπ½)βπ₯) β ((π β π§ β§ (πΉ β π§) β π¦) β (π β ((intβπ½)βπ₯) β§ (πΉ β ((intβπ½)βπ₯)) β π¦))) |
83 | 82 | rspcev 3580 |
. . . . . . . . . . 11
β’
((((intβπ½)βπ₯) β π½ β§ (π β ((intβπ½)βπ₯) β§ (πΉ β ((intβπ½)βπ₯)) β π¦)) β βπ§ β π½ (π β π§ β§ (πΉ β π§) β π¦)) |
84 | 60, 72, 78, 83 | syl12anc 836 |
. . . . . . . . . 10
β’
(((((π½ β
(TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β§ (π₯ β ((neiβπ½)β{π}) β§ (πΉ β π₯) β π¦)) β βπ§ β π½ (π β π§ β§ (πΉ β π§) β π¦)) |
85 | 84 | rexlimdvaa 3150 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β (βπ₯ β ((neiβπ½)β{π})(πΉ β π₯) β π¦ β βπ§ β π½ (π β π§ β§ (πΉ β π§) β π¦))) |
86 | 51, 85 | embantd 59 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β§ (π¦ β πΎ β§ (πΉβπ) β π¦)) β ((π¦ β ((neiβπΎ)β{(πΉβπ)}) β βπ₯ β ((neiβπ½)β{π})(πΉ β π₯) β π¦) β βπ§ β π½ (π β π§ β§ (πΉ β π§) β π¦))) |
87 | 86 | ex 414 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β ((π¦ β πΎ β§ (πΉβπ) β π¦) β ((π¦ β ((neiβπΎ)β{(πΉβπ)}) β βπ₯ β ((neiβπ½)β{π})(πΉ β π₯) β π¦) β βπ§ β π½ (π β π§ β§ (πΉ β π§) β π¦)))) |
88 | 87 | com23 86 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β ((π¦ β ((neiβπΎ)β{(πΉβπ)}) β βπ₯ β ((neiβπ½)β{π})(πΉ β π₯) β π¦) β ((π¦ β πΎ β§ (πΉβπ) β π¦) β βπ§ β π½ (π β π§ β§ (πΉ β π§) β π¦)))) |
89 | 88 | exp4a 433 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β ((π¦ β ((neiβπΎ)β{(πΉβπ)}) β βπ₯ β ((neiβπ½)β{π})(πΉ β π₯) β π¦) β (π¦ β πΎ β ((πΉβπ) β π¦ β βπ§ β π½ (π β π§ β§ (πΉ β π§) β π¦))))) |
90 | 89 | ralimdv2 3157 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β§ πΉ:πβΆπ) β (βπ¦ β ((neiβπΎ)β{(πΉβπ)})βπ₯ β ((neiβπ½)β{π})(πΉ β π₯) β π¦ β βπ¦ β πΎ ((πΉβπ) β π¦ β βπ§ β π½ (π β π§ β§ (πΉ β π§) β π¦)))) |
91 | 90 | imdistanda 573 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β ((πΉ:πβΆπ β§ βπ¦ β ((neiβπΎ)β{(πΉβπ)})βπ₯ β ((neiβπ½)β{π})(πΉ β π₯) β π¦) β (πΉ:πβΆπ β§ βπ¦ β πΎ ((πΉβπ) β π¦ β βπ§ β π½ (π β π§ β§ (πΉ β π§) β π¦))))) |
92 | | iscnp 22604 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β πΎ ((πΉβπ) β π¦ β βπ§ β π½ (π β π§ β§ (πΉ β π§) β π¦))))) |
93 | 91, 92 | sylibrd 259 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β ((πΉ:πβΆπ β§ βπ¦ β ((neiβπΎ)β{(πΉβπ)})βπ₯ β ((neiβπ½)β{π})(πΉ β π₯) β π¦) β πΉ β ((π½ CnP πΎ)βπ))) |
94 | 45, 93 | impbid 211 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β ((neiβπΎ)β{(πΉβπ)})βπ₯ β ((neiβπ½)β{π})(πΉ β π₯) β π¦))) |