Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. 2
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β π½ β Comp) |
2 | | eqid 2733 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
3 | | eqid 2733 |
. . . . . . 7
β’ βͺ πΎ =
βͺ πΎ |
4 | 2, 3 | cnf 22620 |
. . . . . 6
β’ (πΉ β (π½ Cn πΎ) β πΉ:βͺ π½βΆβͺ πΎ) |
5 | 4 | adantl 483 |
. . . . 5
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΉ:βͺ π½βΆβͺ πΎ) |
6 | 5 | ffnd 6673 |
. . . 4
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΉ Fn βͺ π½) |
7 | | dffn4 6766 |
. . . 4
β’ (πΉ Fn βͺ
π½ β πΉ:βͺ π½βontoβran πΉ) |
8 | 6, 7 | sylib 217 |
. . 3
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΉ:βͺ π½βontoβran πΉ) |
9 | | cntop2 22615 |
. . . . . 6
β’ (πΉ β (π½ Cn πΎ) β πΎ β Top) |
10 | 9 | adantl 483 |
. . . . 5
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΎ β Top) |
11 | 5 | frnd 6680 |
. . . . 5
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β ran πΉ β βͺ πΎ) |
12 | 3 | restuni 22536 |
. . . . 5
β’ ((πΎ β Top β§ ran πΉ β βͺ πΎ)
β ran πΉ = βͺ (πΎ
βΎt ran πΉ)) |
13 | 10, 11, 12 | syl2anc 585 |
. . . 4
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β ran πΉ = βͺ (πΎ βΎt ran πΉ)) |
14 | | foeq3 6758 |
. . . 4
β’ (ran
πΉ = βͺ (πΎ
βΎt ran πΉ)
β (πΉ:βͺ π½βontoβran πΉ β πΉ:βͺ π½βontoββͺ (πΎ βΎt ran πΉ))) |
15 | 13, 14 | syl 17 |
. . 3
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β (πΉ:βͺ π½βontoβran πΉ β πΉ:βͺ π½βontoββͺ (πΎ βΎt ran πΉ))) |
16 | 8, 15 | mpbid 231 |
. 2
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΉ:βͺ π½βontoββͺ (πΎ βΎt ran πΉ)) |
17 | | simpr 486 |
. . 3
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΉ β (π½ Cn πΎ)) |
18 | | toptopon2 22290 |
. . . . 5
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
19 | 10, 18 | sylib 217 |
. . . 4
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΎ β (TopOnββͺ πΎ)) |
20 | | ssidd 3971 |
. . . 4
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β ran πΉ β ran πΉ) |
21 | | cnrest2 22660 |
. . . 4
β’ ((πΎ β (TopOnββͺ πΎ)
β§ ran πΉ β ran
πΉ β§ ran πΉ β βͺ πΎ)
β (πΉ β (π½ Cn πΎ) β πΉ β (π½ Cn (πΎ βΎt ran πΉ)))) |
22 | 19, 20, 11, 21 | syl3anc 1372 |
. . 3
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β (πΉ β (π½ Cn πΎ) β πΉ β (π½ Cn (πΎ βΎt ran πΉ)))) |
23 | 17, 22 | mpbid 231 |
. 2
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΉ β (π½ Cn (πΎ βΎt ran πΉ))) |
24 | | eqid 2733 |
. . 3
β’ βͺ (πΎ
βΎt ran πΉ)
= βͺ (πΎ βΎt ran πΉ) |
25 | 24 | cncmp 22766 |
. 2
β’ ((π½ β Comp β§ πΉ:βͺ
π½βontoββͺ (πΎ βΎt ran πΉ) β§ πΉ β (π½ Cn (πΎ βΎt ran πΉ))) β (πΎ βΎt ran πΉ) β Comp) |
26 | 1, 16, 23, 25 | syl3anc 1372 |
1
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β (πΎ βΎt ran πΉ) β Comp) |