Step | Hyp | Ref
| Expression |
1 | | cnsscnp.1 |
. . . 4
β’ π = βͺ
π½ |
2 | | eqid 2732 |
. . . 4
β’ βͺ πΎ =
βͺ πΎ |
3 | 1, 2 | cnf 22749 |
. . 3
β’ (πΉ β (π½ Cn πΎ) β πΉ:πβΆβͺ πΎ) |
4 | 3 | adantr 481 |
. 2
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β π) β πΉ:πβΆβͺ πΎ) |
5 | | cnima 22768 |
. . . . . 6
β’ ((πΉ β (π½ Cn πΎ) β§ π¦ β πΎ) β (β‘πΉ β π¦) β π½) |
6 | 5 | ad2ant2r 745 |
. . . . 5
β’ (((πΉ β (π½ Cn πΎ) β§ π΄ β π) β§ (π¦ β πΎ β§ (πΉβπ΄) β π¦)) β (β‘πΉ β π¦) β π½) |
7 | | simpr 485 |
. . . . . . 7
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β π) β π΄ β π) |
8 | 7 | adantr 481 |
. . . . . 6
β’ (((πΉ β (π½ Cn πΎ) β§ π΄ β π) β§ (π¦ β πΎ β§ (πΉβπ΄) β π¦)) β π΄ β π) |
9 | | simprr 771 |
. . . . . 6
β’ (((πΉ β (π½ Cn πΎ) β§ π΄ β π) β§ (π¦ β πΎ β§ (πΉβπ΄) β π¦)) β (πΉβπ΄) β π¦) |
10 | 3 | ad2antrr 724 |
. . . . . . 7
β’ (((πΉ β (π½ Cn πΎ) β§ π΄ β π) β§ (π¦ β πΎ β§ (πΉβπ΄) β π¦)) β πΉ:πβΆβͺ πΎ) |
11 | | ffn 6717 |
. . . . . . 7
β’ (πΉ:πβΆβͺ πΎ β πΉ Fn π) |
12 | | elpreima 7059 |
. . . . . . 7
β’ (πΉ Fn π β (π΄ β (β‘πΉ β π¦) β (π΄ β π β§ (πΉβπ΄) β π¦))) |
13 | 10, 11, 12 | 3syl 18 |
. . . . . 6
β’ (((πΉ β (π½ Cn πΎ) β§ π΄ β π) β§ (π¦ β πΎ β§ (πΉβπ΄) β π¦)) β (π΄ β (β‘πΉ β π¦) β (π΄ β π β§ (πΉβπ΄) β π¦))) |
14 | 8, 9, 13 | mpbir2and 711 |
. . . . 5
β’ (((πΉ β (π½ Cn πΎ) β§ π΄ β π) β§ (π¦ β πΎ β§ (πΉβπ΄) β π¦)) β π΄ β (β‘πΉ β π¦)) |
15 | | eqimss 4040 |
. . . . . . . 8
β’ (π₯ = (β‘πΉ β π¦) β π₯ β (β‘πΉ β π¦)) |
16 | 15 | biantrud 532 |
. . . . . . 7
β’ (π₯ = (β‘πΉ β π¦) β (π΄ β π₯ β (π΄ β π₯ β§ π₯ β (β‘πΉ β π¦)))) |
17 | | eleq2 2822 |
. . . . . . 7
β’ (π₯ = (β‘πΉ β π¦) β (π΄ β π₯ β π΄ β (β‘πΉ β π¦))) |
18 | 16, 17 | bitr3d 280 |
. . . . . 6
β’ (π₯ = (β‘πΉ β π¦) β ((π΄ β π₯ β§ π₯ β (β‘πΉ β π¦)) β π΄ β (β‘πΉ β π¦))) |
19 | 18 | rspcev 3612 |
. . . . 5
β’ (((β‘πΉ β π¦) β π½ β§ π΄ β (β‘πΉ β π¦)) β βπ₯ β π½ (π΄ β π₯ β§ π₯ β (β‘πΉ β π¦))) |
20 | 6, 14, 19 | syl2anc 584 |
. . . 4
β’ (((πΉ β (π½ Cn πΎ) β§ π΄ β π) β§ (π¦ β πΎ β§ (πΉβπ΄) β π¦)) β βπ₯ β π½ (π΄ β π₯ β§ π₯ β (β‘πΉ β π¦))) |
21 | 20 | expr 457 |
. . 3
β’ (((πΉ β (π½ Cn πΎ) β§ π΄ β π) β§ π¦ β πΎ) β ((πΉβπ΄) β π¦ β βπ₯ β π½ (π΄ β π₯ β§ π₯ β (β‘πΉ β π¦)))) |
22 | 21 | ralrimiva 3146 |
. 2
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β π) β βπ¦ β πΎ ((πΉβπ΄) β π¦ β βπ₯ β π½ (π΄ β π₯ β§ π₯ β (β‘πΉ β π¦)))) |
23 | | cntop1 22743 |
. . . . 5
β’ (πΉ β (π½ Cn πΎ) β π½ β Top) |
24 | 23 | adantr 481 |
. . . 4
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β π) β π½ β Top) |
25 | 1 | toptopon 22418 |
. . . 4
β’ (π½ β Top β π½ β (TopOnβπ)) |
26 | 24, 25 | sylib 217 |
. . 3
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β π) β π½ β (TopOnβπ)) |
27 | | cntop2 22744 |
. . . . 5
β’ (πΉ β (π½ Cn πΎ) β πΎ β Top) |
28 | 27 | adantr 481 |
. . . 4
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β π) β πΎ β Top) |
29 | 2 | toptopon 22418 |
. . . 4
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
30 | 28, 29 | sylib 217 |
. . 3
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β π) β πΎ β (TopOnββͺ πΎ)) |
31 | | iscnp3 22747 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnββͺ πΎ)
β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆβͺ πΎ β§ βπ¦ β πΎ ((πΉβπ΄) β π¦ β βπ₯ β π½ (π΄ β π₯ β§ π₯ β (β‘πΉ β π¦)))))) |
32 | 26, 30, 7, 31 | syl3anc 1371 |
. 2
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆβͺ πΎ β§ βπ¦ β πΎ ((πΉβπ΄) β π¦ β βπ₯ β π½ (π΄ β π₯ β§ π₯ β (β‘πΉ β π¦)))))) |
33 | 4, 22, 32 | mpbir2and 711 |
1
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β π) β πΉ β ((π½ CnP πΎ)βπ΄)) |