Step | Hyp | Ref
| Expression |
1 | | cnptop1 22966 |
. . . 4
β’ (πΉ β ((π½ CnP πΎ)βπ) β π½ β Top) |
2 | | cnprest.1 |
. . . . 5
β’ π = βͺ
π½ |
3 | 2 | cnprcl 22969 |
. . . 4
β’ (πΉ β ((π½ CnP πΎ)βπ) β π β π) |
4 | 1, 3 | jca 510 |
. . 3
β’ (πΉ β ((π½ CnP πΎ)βπ) β (π½ β Top β§ π β π)) |
5 | 4 | a1i 11 |
. 2
β’ ((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β (πΉ β ((π½ CnP πΎ)βπ) β (π½ β Top β§ π β π))) |
6 | | cnptop1 22966 |
. . . 4
β’ (πΉ β ((π½ CnP (πΎ βΎt π΅))βπ) β π½ β Top) |
7 | 2 | cnprcl 22969 |
. . . 4
β’ (πΉ β ((π½ CnP (πΎ βΎt π΅))βπ) β π β π) |
8 | 6, 7 | jca 510 |
. . 3
β’ (πΉ β ((π½ CnP (πΎ βΎt π΅))βπ) β (π½ β Top β§ π β π)) |
9 | 8 | a1i 11 |
. 2
β’ ((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β (πΉ β ((π½ CnP (πΎ βΎt π΅))βπ) β (π½ β Top β§ π β π))) |
10 | | simpl2 1190 |
. . . . . . . . . 10
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β πΉ:πβΆπ΅) |
11 | | simprr 769 |
. . . . . . . . . 10
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β π β π) |
12 | 10, 11 | ffvelcdmd 7086 |
. . . . . . . . 9
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β (πΉβπ) β π΅) |
13 | 12 | biantrud 530 |
. . . . . . . 8
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β ((πΉβπ) β π₯ β ((πΉβπ) β π₯ β§ (πΉβπ) β π΅))) |
14 | | elin 3963 |
. . . . . . . 8
β’ ((πΉβπ) β (π₯ β© π΅) β ((πΉβπ) β π₯ β§ (πΉβπ) β π΅)) |
15 | 13, 14 | bitr4di 288 |
. . . . . . 7
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β ((πΉβπ) β π₯ β (πΉβπ) β (π₯ β© π΅))) |
16 | | imassrn 6069 |
. . . . . . . . . . . 12
β’ (πΉ β π¦) β ran πΉ |
17 | 10 | frnd 6724 |
. . . . . . . . . . . 12
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β ran πΉ β π΅) |
18 | 16, 17 | sstrid 3992 |
. . . . . . . . . . 11
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β (πΉ β π¦) β π΅) |
19 | 18 | biantrud 530 |
. . . . . . . . . 10
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β ((πΉ β π¦) β π₯ β ((πΉ β π¦) β π₯ β§ (πΉ β π¦) β π΅))) |
20 | | ssin 4229 |
. . . . . . . . . 10
β’ (((πΉ β π¦) β π₯ β§ (πΉ β π¦) β π΅) β (πΉ β π¦) β (π₯ β© π΅)) |
21 | 19, 20 | bitrdi 286 |
. . . . . . . . 9
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β ((πΉ β π¦) β π₯ β (πΉ β π¦) β (π₯ β© π΅))) |
22 | 21 | anbi2d 627 |
. . . . . . . 8
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β ((π β π¦ β§ (πΉ β π¦) β π₯) β (π β π¦ β§ (πΉ β π¦) β (π₯ β© π΅)))) |
23 | 22 | rexbidv 3176 |
. . . . . . 7
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β (βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π₯) β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β (π₯ β© π΅)))) |
24 | 15, 23 | imbi12d 343 |
. . . . . 6
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β (((πΉβπ) β π₯ β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π₯)) β ((πΉβπ) β (π₯ β© π΅) β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β (π₯ β© π΅))))) |
25 | 24 | ralbidv 3175 |
. . . . 5
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β (βπ₯ β πΎ ((πΉβπ) β π₯ β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π₯)) β βπ₯ β πΎ ((πΉβπ) β (π₯ β© π΅) β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β (π₯ β© π΅))))) |
26 | | vex 3476 |
. . . . . . . 8
β’ π₯ β V |
27 | 26 | inex1 5316 |
. . . . . . 7
β’ (π₯ β© π΅) β V |
28 | 27 | a1i 11 |
. . . . . 6
β’ ((((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β§ π₯ β πΎ) β (π₯ β© π΅) β V) |
29 | | simpl1 1189 |
. . . . . . 7
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β πΎ β Top) |
30 | | cnprest.2 |
. . . . . . . . . 10
β’ π = βͺ
πΎ |
31 | | uniexg 7732 |
. . . . . . . . . 10
β’ (πΎ β Top β βͺ πΎ
β V) |
32 | 30, 31 | eqeltrid 2835 |
. . . . . . . . 9
β’ (πΎ β Top β π β V) |
33 | 29, 32 | syl 17 |
. . . . . . . 8
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β π β V) |
34 | | simpl3 1191 |
. . . . . . . 8
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β π΅ β π) |
35 | 33, 34 | ssexd 5323 |
. . . . . . 7
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β π΅ β V) |
36 | | elrest 17377 |
. . . . . . 7
β’ ((πΎ β Top β§ π΅ β V) β (π§ β (πΎ βΎt π΅) β βπ₯ β πΎ π§ = (π₯ β© π΅))) |
37 | 29, 35, 36 | syl2anc 582 |
. . . . . 6
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β (π§ β (πΎ βΎt π΅) β βπ₯ β πΎ π§ = (π₯ β© π΅))) |
38 | | eleq2 2820 |
. . . . . . . 8
β’ (π§ = (π₯ β© π΅) β ((πΉβπ) β π§ β (πΉβπ) β (π₯ β© π΅))) |
39 | | sseq2 4007 |
. . . . . . . . . 10
β’ (π§ = (π₯ β© π΅) β ((πΉ β π¦) β π§ β (πΉ β π¦) β (π₯ β© π΅))) |
40 | 39 | anbi2d 627 |
. . . . . . . . 9
β’ (π§ = (π₯ β© π΅) β ((π β π¦ β§ (πΉ β π¦) β π§) β (π β π¦ β§ (πΉ β π¦) β (π₯ β© π΅)))) |
41 | 40 | rexbidv 3176 |
. . . . . . . 8
β’ (π§ = (π₯ β© π΅) β (βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π§) β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β (π₯ β© π΅)))) |
42 | 38, 41 | imbi12d 343 |
. . . . . . 7
β’ (π§ = (π₯ β© π΅) β (((πΉβπ) β π§ β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π§)) β ((πΉβπ) β (π₯ β© π΅) β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β (π₯ β© π΅))))) |
43 | 42 | adantl 480 |
. . . . . 6
β’ ((((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β§ π§ = (π₯ β© π΅)) β (((πΉβπ) β π§ β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π§)) β ((πΉβπ) β (π₯ β© π΅) β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β (π₯ β© π΅))))) |
44 | 28, 37, 43 | ralxfr2d 5407 |
. . . . 5
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β (βπ§ β (πΎ βΎt π΅)((πΉβπ) β π§ β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π§)) β βπ₯ β πΎ ((πΉβπ) β (π₯ β© π΅) β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β (π₯ β© π΅))))) |
45 | 25, 44 | bitr4d 281 |
. . . 4
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β (βπ₯ β πΎ ((πΉβπ) β π₯ β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π₯)) β βπ§ β (πΎ βΎt π΅)((πΉβπ) β π§ β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π§)))) |
46 | 10, 34 | fssd 6734 |
. . . . 5
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β πΉ:πβΆπ) |
47 | | simprl 767 |
. . . . . 6
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β π½ β Top) |
48 | 2, 30 | iscnp2 22963 |
. . . . . . 7
β’ (πΉ β ((π½ CnP πΎ)βπ) β ((π½ β Top β§ πΎ β Top β§ π β π) β§ (πΉ:πβΆπ β§ βπ₯ β πΎ ((πΉβπ) β π₯ β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π₯))))) |
49 | 48 | baib 534 |
. . . . . 6
β’ ((π½ β Top β§ πΎ β Top β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ₯ β πΎ ((πΉβπ) β π₯ β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π₯))))) |
50 | 47, 29, 11, 49 | syl3anc 1369 |
. . . . 5
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ₯ β πΎ ((πΉβπ) β π₯ β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π₯))))) |
51 | 46, 50 | mpbirand 703 |
. . . 4
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β (πΉ β ((π½ CnP πΎ)βπ) β βπ₯ β πΎ ((πΉβπ) β π₯ β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π₯)))) |
52 | 2 | toptopon 22639 |
. . . . . . 7
β’ (π½ β Top β π½ β (TopOnβπ)) |
53 | 47, 52 | sylib 217 |
. . . . . 6
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β π½ β (TopOnβπ)) |
54 | 30 | toptopon 22639 |
. . . . . . . 8
β’ (πΎ β Top β πΎ β (TopOnβπ)) |
55 | 29, 54 | sylib 217 |
. . . . . . 7
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β πΎ β (TopOnβπ)) |
56 | | resttopon 22885 |
. . . . . . 7
β’ ((πΎ β (TopOnβπ) β§ π΅ β π) β (πΎ βΎt π΅) β (TopOnβπ΅)) |
57 | 55, 34, 56 | syl2anc 582 |
. . . . . 6
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β (πΎ βΎt π΅) β (TopOnβπ΅)) |
58 | | iscnp 22961 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ (πΎ βΎt π΅) β (TopOnβπ΅) β§ π β π) β (πΉ β ((π½ CnP (πΎ βΎt π΅))βπ) β (πΉ:πβΆπ΅ β§ βπ§ β (πΎ βΎt π΅)((πΉβπ) β π§ β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π§))))) |
59 | 53, 57, 11, 58 | syl3anc 1369 |
. . . . 5
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β (πΉ β ((π½ CnP (πΎ βΎt π΅))βπ) β (πΉ:πβΆπ΅ β§ βπ§ β (πΎ βΎt π΅)((πΉβπ) β π§ β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π§))))) |
60 | 10, 59 | mpbirand 703 |
. . . 4
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β (πΉ β ((π½ CnP (πΎ βΎt π΅))βπ) β βπ§ β (πΎ βΎt π΅)((πΉβπ) β π§ β βπ¦ β π½ (π β π¦ β§ (πΉ β π¦) β π§)))) |
61 | 45, 51, 60 | 3bitr4d 310 |
. . 3
β’ (((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β§ (π½ β Top β§ π β π)) β (πΉ β ((π½ CnP πΎ)βπ) β πΉ β ((π½ CnP (πΎ βΎt π΅))βπ))) |
62 | 61 | ex 411 |
. 2
β’ ((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β ((π½ β Top β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β πΉ β ((π½ CnP (πΎ βΎt π΅))βπ)))) |
63 | 5, 9, 62 | pm5.21ndd 378 |
1
β’ ((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β (πΉ β ((π½ CnP πΎ)βπ) β πΉ β ((π½ CnP (πΎ βΎt π΅))βπ))) |