Step | Hyp | Ref
| Expression |
1 | | kgencn 23052 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β ((πGenβπ½) Cn πΎ) β (πΉ:πβΆπ β§ βπ β π« π((π½ βΎt π) β Comp β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ))))) |
2 | | rncmp 22892 |
. . . . . . . 8
β’ ((π§ β Comp β§ π β (π§ Cn π½)) β (π½ βΎt ran π) β Comp) |
3 | 2 | adantl 483 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β (π½ βΎt ran π) β Comp) |
4 | | simprr 772 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β π β (π§ Cn π½)) |
5 | | eqid 2733 |
. . . . . . . . . . . 12
β’ βͺ π§ =
βͺ π§ |
6 | | eqid 2733 |
. . . . . . . . . . . 12
β’ βͺ π½ =
βͺ π½ |
7 | 5, 6 | cnf 22742 |
. . . . . . . . . . 11
β’ (π β (π§ Cn π½) β π:βͺ π§βΆβͺ π½) |
8 | | frn 6722 |
. . . . . . . . . . 11
β’ (π:βͺ
π§βΆβͺ π½
β ran π β βͺ π½) |
9 | 4, 7, 8 | 3syl 18 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β ran π β βͺ π½) |
10 | | toponuni 22408 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
11 | 10 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β π = βͺ π½) |
12 | 9, 11 | sseqtrrd 4023 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β ran π β π) |
13 | | vex 3479 |
. . . . . . . . . . 11
β’ π β V |
14 | 13 | rnex 7900 |
. . . . . . . . . 10
β’ ran π β V |
15 | 14 | elpw 4606 |
. . . . . . . . 9
β’ (ran
π β π« π β ran π β π) |
16 | 12, 15 | sylibr 233 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β ran π β π« π) |
17 | | oveq2 7414 |
. . . . . . . . . . 11
β’ (π = ran π β (π½ βΎt π) = (π½ βΎt ran π)) |
18 | 17 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = ran π β ((π½ βΎt π) β Comp β (π½ βΎt ran π) β Comp)) |
19 | | reseq2 5975 |
. . . . . . . . . . 11
β’ (π = ran π β (πΉ βΎ π) = (πΉ βΎ ran π)) |
20 | 17 | oveq1d 7421 |
. . . . . . . . . . 11
β’ (π = ran π β ((π½ βΎt π) Cn πΎ) = ((π½ βΎt ran π) Cn πΎ)) |
21 | 19, 20 | eleq12d 2828 |
. . . . . . . . . 10
β’ (π = ran π β ((πΉ βΎ π) β ((π½ βΎt π) Cn πΎ) β (πΉ βΎ ran π) β ((π½ βΎt ran π) Cn πΎ))) |
22 | 18, 21 | imbi12d 345 |
. . . . . . . . 9
β’ (π = ran π β (((π½ βΎt π) β Comp β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ)) β ((π½ βΎt ran π) β Comp β (πΉ βΎ ran π) β ((π½ βΎt ran π) Cn πΎ)))) |
23 | 22 | rspcv 3609 |
. . . . . . . 8
β’ (ran
π β π« π β (βπ β π« π((π½ βΎt π) β Comp β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ)) β ((π½ βΎt ran π) β Comp β (πΉ βΎ ran π) β ((π½ βΎt ran π) Cn πΎ)))) |
24 | 16, 23 | syl 17 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β (βπ β π« π((π½ βΎt π) β Comp β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ)) β ((π½ βΎt ran π) β Comp β (πΉ βΎ ran π) β ((π½ βΎt ran π) Cn πΎ)))) |
25 | 3, 24 | mpid 44 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β (βπ β π« π((π½ βΎt π) β Comp β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ)) β (πΉ βΎ ran π) β ((π½ βΎt ran π) Cn πΎ))) |
26 | | simplll 774 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β π½ β (TopOnβπ)) |
27 | | ssidd 4005 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β ran π β ran π) |
28 | | cnrest2 22782 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ ran π β ran π β§ ran π β π) β (π β (π§ Cn π½) β π β (π§ Cn (π½ βΎt ran π)))) |
29 | 26, 27, 12, 28 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β (π β (π§ Cn π½) β π β (π§ Cn (π½ βΎt ran π)))) |
30 | 4, 29 | mpbid 231 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β π β (π§ Cn (π½ βΎt ran π))) |
31 | | cnco 22762 |
. . . . . . . . 9
β’ ((π β (π§ Cn (π½ βΎt ran π)) β§ (πΉ βΎ ran π) β ((π½ βΎt ran π) Cn πΎ)) β ((πΉ βΎ ran π) β π) β (π§ Cn πΎ)) |
32 | 31 | ex 414 |
. . . . . . . 8
β’ (π β (π§ Cn (π½ βΎt ran π)) β ((πΉ βΎ ran π) β ((π½ βΎt ran π) Cn πΎ) β ((πΉ βΎ ran π) β π) β (π§ Cn πΎ))) |
33 | 30, 32 | syl 17 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β ((πΉ βΎ ran π) β ((π½ βΎt ran π) Cn πΎ) β ((πΉ βΎ ran π) β π) β (π§ Cn πΎ))) |
34 | | ssid 4004 |
. . . . . . . . 9
β’ ran π β ran π |
35 | | cores 6246 |
. . . . . . . . 9
β’ (ran
π β ran π β ((πΉ βΎ ran π) β π) = (πΉ β π)) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . 8
β’ ((πΉ βΎ ran π) β π) = (πΉ β π) |
37 | 36 | eleq1i 2825 |
. . . . . . 7
β’ (((πΉ βΎ ran π) β π) β (π§ Cn πΎ) β (πΉ β π) β (π§ Cn πΎ)) |
38 | 33, 37 | imbitrdi 250 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β ((πΉ βΎ ran π) β ((π½ βΎt ran π) Cn πΎ) β (πΉ β π) β (π§ Cn πΎ))) |
39 | 25, 38 | syld 47 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ (π§ β Comp β§ π β (π§ Cn π½))) β (βπ β π« π((π½ βΎt π) β Comp β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ)) β (πΉ β π) β (π§ Cn πΎ))) |
40 | 39 | ralrimdvva 3210 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β (βπ β π« π((π½ βΎt π) β Comp β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ)) β βπ§ β Comp βπ β (π§ Cn π½)(πΉ β π) β (π§ Cn πΎ))) |
41 | | oveq1 7413 |
. . . . . . . . 9
β’ (π§ = (π½ βΎt π) β (π§ Cn π½) = ((π½ βΎt π) Cn π½)) |
42 | | oveq1 7413 |
. . . . . . . . . 10
β’ (π§ = (π½ βΎt π) β (π§ Cn πΎ) = ((π½ βΎt π) Cn πΎ)) |
43 | 42 | eleq2d 2820 |
. . . . . . . . 9
β’ (π§ = (π½ βΎt π) β ((πΉ β π) β (π§ Cn πΎ) β (πΉ β π) β ((π½ βΎt π) Cn πΎ))) |
44 | 41, 43 | raleqbidv 3343 |
. . . . . . . 8
β’ (π§ = (π½ βΎt π) β (βπ β (π§ Cn π½)(πΉ β π) β (π§ Cn πΎ) β βπ β ((π½ βΎt π) Cn π½)(πΉ β π) β ((π½ βΎt π) Cn πΎ))) |
45 | 44 | rspcv 3609 |
. . . . . . 7
β’ ((π½ βΎt π) β Comp β
(βπ§ β Comp
βπ β (π§ Cn π½)(πΉ β π) β (π§ Cn πΎ) β βπ β ((π½ βΎt π) Cn π½)(πΉ β π) β ((π½ βΎt π) Cn πΎ))) |
46 | | elpwi 4609 |
. . . . . . . . . . . 12
β’ (π β π« π β π β π) |
47 | 46 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ π β π« π) β π β π) |
48 | 47 | resabs1d 6011 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ π β π« π) β (( I βΎ π) βΎ π) = ( I βΎ π)) |
49 | | idcn 22753 |
. . . . . . . . . . . 12
β’ (π½ β (TopOnβπ) β ( I βΎ π) β (π½ Cn π½)) |
50 | 49 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ π β π« π) β ( I βΎ π) β (π½ Cn π½)) |
51 | 10 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ π β π« π) β π = βͺ π½) |
52 | 47, 51 | sseqtrd 4022 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ π β π« π) β π β βͺ π½) |
53 | 6 | cnrest 22781 |
. . . . . . . . . . 11
β’ ((( I
βΎ π) β (π½ Cn π½) β§ π β βͺ π½) β (( I βΎ π) βΎ π) β ((π½ βΎt π) Cn π½)) |
54 | 50, 52, 53 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ π β π« π) β (( I βΎ π) βΎ π) β ((π½ βΎt π) Cn π½)) |
55 | 48, 54 | eqeltrrd 2835 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ π β π« π) β ( I βΎ π) β ((π½ βΎt π) Cn π½)) |
56 | | coeq2 5857 |
. . . . . . . . . . 11
β’ (π = ( I βΎ π) β (πΉ β π) = (πΉ β ( I βΎ π))) |
57 | 56 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = ( I βΎ π) β ((πΉ β π) β ((π½ βΎt π) Cn πΎ) β (πΉ β ( I βΎ π)) β ((π½ βΎt π) Cn πΎ))) |
58 | 57 | rspcv 3609 |
. . . . . . . . 9
β’ (( I
βΎ π) β ((π½ βΎt π) Cn π½) β (βπ β ((π½ βΎt π) Cn π½)(πΉ β π) β ((π½ βΎt π) Cn πΎ) β (πΉ β ( I βΎ π)) β ((π½ βΎt π) Cn πΎ))) |
59 | 55, 58 | syl 17 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ π β π« π) β (βπ β ((π½ βΎt π) Cn π½)(πΉ β π) β ((π½ βΎt π) Cn πΎ) β (πΉ β ( I βΎ π)) β ((π½ βΎt π) Cn πΎ))) |
60 | | coires1 6261 |
. . . . . . . . 9
β’ (πΉ β ( I βΎ π)) = (πΉ βΎ π) |
61 | 60 | eleq1i 2825 |
. . . . . . . 8
β’ ((πΉ β ( I βΎ π)) β ((π½ βΎt π) Cn πΎ) β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ)) |
62 | 59, 61 | imbitrdi 250 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ π β π« π) β (βπ β ((π½ βΎt π) Cn π½)(πΉ β π) β ((π½ βΎt π) Cn πΎ) β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ))) |
63 | 45, 62 | syl9r 78 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ π β π« π) β ((π½ βΎt π) β Comp β (βπ§ β Comp βπ β (π§ Cn π½)(πΉ β π) β (π§ Cn πΎ) β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ)))) |
64 | 63 | com23 86 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β§ π β π« π) β (βπ§ β Comp βπ β (π§ Cn π½)(πΉ β π) β (π§ Cn πΎ) β ((π½ βΎt π) β Comp β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ)))) |
65 | 64 | ralrimdva 3155 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β (βπ§ β Comp βπ β (π§ Cn π½)(πΉ β π) β (π§ Cn πΎ) β βπ β π« π((π½ βΎt π) β Comp β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ)))) |
66 | 40, 65 | impbid 211 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ:πβΆπ) β (βπ β π« π((π½ βΎt π) β Comp β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ)) β βπ§ β Comp βπ β (π§ Cn π½)(πΉ β π) β (π§ Cn πΎ))) |
67 | 66 | pm5.32da 580 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β ((πΉ:πβΆπ β§ βπ β π« π((π½ βΎt π) β Comp β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ))) β (πΉ:πβΆπ β§ βπ§ β Comp βπ β (π§ Cn π½)(πΉ β π) β (π§ Cn πΎ)))) |
68 | 1, 67 | bitrd 279 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β ((πGenβπ½) Cn πΎ) β (πΉ:πβΆπ β§ βπ§ β Comp βπ β (π§ Cn π½)(πΉ β π) β (π§ Cn πΎ)))) |