Step | Hyp | Ref
| Expression |
1 | | cntop1 13671 |
. . . . 5
β’ (πΉ β (π½ Cn πΎ) β π½ β Top) |
2 | | cncnp.1 |
. . . . . 6
β’ π = βͺ
π½ |
3 | 2 | toptopon 13488 |
. . . . 5
β’ (π½ β Top β π½ β (TopOnβπ)) |
4 | 1, 3 | sylib 122 |
. . . 4
β’ (πΉ β (π½ Cn πΎ) β π½ β (TopOnβπ)) |
5 | | cntop2 13672 |
. . . . 5
β’ (πΉ β (π½ Cn πΎ) β πΎ β Top) |
6 | | cncnp.2 |
. . . . . 6
β’ π = βͺ
πΎ |
7 | 6 | toptopon 13488 |
. . . . 5
β’ (πΎ β Top β πΎ β (TopOnβπ)) |
8 | 5, 7 | sylib 122 |
. . . 4
β’ (πΉ β (π½ Cn πΎ) β πΎ β (TopOnβπ)) |
9 | 2, 6 | cnf 13674 |
. . . 4
β’ (πΉ β (π½ Cn πΎ) β πΉ:πβΆπ) |
10 | 4, 8, 9 | jca31 309 |
. . 3
β’ (πΉ β (π½ Cn πΎ) β ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ)) |
11 | 10 | adantl 277 |
. 2
β’ (((π½ β Top β§ πΎ β Top β§ βπ¦ π¦ β π) β§ πΉ β (π½ Cn πΎ)) β ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ)) |
12 | 3 | biimpi 120 |
. . . . 5
β’ (π½ β Top β π½ β (TopOnβπ)) |
13 | 12 | 3ad2ant1 1018 |
. . . 4
β’ ((π½ β Top β§ πΎ β Top β§ βπ¦ π¦ β π) β π½ β (TopOnβπ)) |
14 | 13 | adantr 276 |
. . 3
β’ (((π½ β Top β§ πΎ β Top β§ βπ¦ π¦ β π) β§ βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)) β π½ β (TopOnβπ)) |
15 | 7 | biimpi 120 |
. . . . 5
β’ (πΎ β Top β πΎ β (TopOnβπ)) |
16 | 15 | 3ad2ant2 1019 |
. . . 4
β’ ((π½ β Top β§ πΎ β Top β§ βπ¦ π¦ β π) β πΎ β (TopOnβπ)) |
17 | 16 | adantr 276 |
. . 3
β’ (((π½ β Top β§ πΎ β Top β§ βπ¦ π¦ β π) β§ βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)) β πΎ β (TopOnβπ)) |
18 | | r19.2m 3509 |
. . . . . . 7
β’
((βπ¦ π¦ β π β§ βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)) β βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)) |
19 | 18 | ex 115 |
. . . . . 6
β’
(βπ¦ π¦ β π β (βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯) β βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯))) |
20 | 19 | 3ad2ant3 1020 |
. . . . 5
β’ ((π½ β Top β§ πΎ β Top β§ βπ¦ π¦ β π) β (βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯) β βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯))) |
21 | | cnpf2 13677 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ₯)) β πΉ:πβΆπ) |
22 | 21 | 3expia 1205 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β ((π½ CnP πΎ)βπ₯) β πΉ:πβΆπ)) |
23 | 22 | rexlimdvw 2598 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯) β πΉ:πβΆπ)) |
24 | 13, 16, 23 | syl2anc 411 |
. . . . 5
β’ ((π½ β Top β§ πΎ β Top β§ βπ¦ π¦ β π) β (βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯) β πΉ:πβΆπ)) |
25 | 20, 24 | syld 45 |
. . . 4
β’ ((π½ β Top β§ πΎ β Top β§ βπ¦ π¦ β π) β (βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯) β πΉ:πβΆπ)) |
26 | 25 | imp 124 |
. . 3
β’ (((π½ β Top β§ πΎ β Top β§ βπ¦ π¦ β π) β§ βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)) β πΉ:πβΆπ) |
27 | 14, 17, 26 | jca31 309 |
. 2
β’ (((π½ β Top β§ πΎ β Top β§ βπ¦ π¦ β π) β§ βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)) β ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ)) |
28 | | cncnp 13700 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯)))) |
29 | 28 | baibd 923 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β (πΉ β (π½ Cn πΎ) β βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯))) |
30 | 11, 27, 29 | pm5.21nd 916 |
1
β’ ((π½ β Top β§ πΎ β Top β§ βπ¦ π¦ β π) β (πΉ β (π½ Cn πΎ) β βπ₯ β π πΉ β ((π½ CnP πΎ)βπ₯))) |