Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. 2
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β π½ β Comp) |
2 | | eqid 2732 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
3 | | eqid 2732 |
. . . . . . 7
β’ βͺ πΎ =
βͺ πΎ |
4 | 2, 3 | cnf 22749 |
. . . . . 6
β’ (πΉ β (π½ Cn πΎ) β πΉ:βͺ π½βΆβͺ πΎ) |
5 | 4 | adantl 482 |
. . . . 5
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΉ:βͺ π½βΆβͺ πΎ) |
6 | 5 | ffnd 6718 |
. . . 4
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΉ Fn βͺ π½) |
7 | | dffn4 6811 |
. . . 4
β’ (πΉ Fn βͺ
π½ β πΉ:βͺ π½βontoβran πΉ) |
8 | 6, 7 | sylib 217 |
. . 3
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΉ:βͺ π½βontoβran πΉ) |
9 | | cntop2 22744 |
. . . . . 6
β’ (πΉ β (π½ Cn πΎ) β πΎ β Top) |
10 | 9 | adantl 482 |
. . . . 5
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΎ β Top) |
11 | 5 | frnd 6725 |
. . . . 5
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β ran πΉ β βͺ πΎ) |
12 | 3 | restuni 22665 |
. . . . 5
β’ ((πΎ β Top β§ ran πΉ β βͺ πΎ)
β ran πΉ = βͺ (πΎ
βΎt ran πΉ)) |
13 | 10, 11, 12 | syl2anc 584 |
. . . 4
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β ran πΉ = βͺ (πΎ βΎt ran πΉ)) |
14 | | foeq3 6803 |
. . . 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 485 |
. . 3
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΉ β (π½ Cn πΎ)) |
18 | | toptopon2 22419 |
. . . . 5
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
19 | 10, 18 | sylib 217 |
. . . 4
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΎ β (TopOnββͺ πΎ)) |
20 | | ssidd 4005 |
. . . 4
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β ran πΉ β ran πΉ) |
21 | | cnrest2 22789 |
. . . 4
β’ ((πΎ β (TopOnββͺ πΎ)
β§ ran πΉ β ran
πΉ β§ ran πΉ β βͺ πΎ)
β (πΉ β (π½ Cn πΎ) β πΉ β (π½ Cn (πΎ βΎt ran πΉ)))) |
22 | 19, 20, 11, 21 | syl3anc 1371 |
. . 3
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β (πΉ β (π½ Cn πΎ) β πΉ β (π½ Cn (πΎ βΎt ran πΉ)))) |
23 | 17, 22 | mpbid 231 |
. 2
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β πΉ β (π½ Cn (πΎ βΎt ran πΉ))) |
24 | | eqid 2732 |
. . 3
β’ βͺ (πΎ
βΎt ran πΉ)
= βͺ (πΎ βΎt ran πΉ) |
25 | 24 | cncmp 22895 |
. 2
β’ ((π½ β Comp β§ πΉ:βͺ
π½βontoββͺ (πΎ βΎt ran πΉ) β§ πΉ β (π½ Cn (πΎ βΎt ran πΉ))) β (πΎ βΎt ran πΉ) β Comp) |
26 | 1, 16, 23, 25 | syl3anc 1371 |
1
β’ ((π½ β Comp β§ πΉ β (π½ Cn πΎ)) β (πΎ βΎt ran πΉ) β Comp) |