Step | Hyp | Ref
| Expression |
1 | | vpwex 5374 |
. . . . . . 7
β’ π«
π‘ β V |
2 | 1 | inex2 5317 |
. . . . . 6
β’ (π½ β© π« π‘) β V |
3 | 2 | uniex 7727 |
. . . . 5
β’ βͺ (π½
β© π« π‘) β
V |
4 | 3 | rgenw 3065 |
. . . 4
β’
βπ‘ β
π« πβͺ (π½
β© π« π‘) β
V |
5 | | nfcv 2903 |
. . . . 5
β’
β²π‘π« π |
6 | 5 | fnmptf 6683 |
. . . 4
β’
(βπ‘ β
π« πβͺ (π½
β© π« π‘) β V
β (π‘ β π«
π β¦ βͺ (π½
β© π« π‘)) Fn
π« π) |
7 | 4, 6 | mp1i 13 |
. . 3
β’ (π½ β Top β (π‘ β π« π β¦ βͺ (π½
β© π« π‘)) Fn
π« π) |
8 | | dssmapclsntr.i |
. . . . 5
β’ πΌ = (intβπ½) |
9 | | dssmapclsntr.x |
. . . . . 6
β’ π = βͺ
π½ |
10 | 9 | ntrfval 22519 |
. . . . 5
β’ (π½ β Top β
(intβπ½) = (π‘ β π« π β¦ βͺ (π½
β© π« π‘))) |
11 | 8, 10 | eqtrid 2784 |
. . . 4
β’ (π½ β Top β πΌ = (π‘ β π« π β¦ βͺ (π½ β© π« π‘))) |
12 | 11 | fneq1d 6639 |
. . 3
β’ (π½ β Top β (πΌ Fn π« π β (π‘ β π« π β¦ βͺ (π½ β© π« π‘)) Fn π« π)) |
13 | 7, 12 | mpbird 256 |
. 2
β’ (π½ β Top β πΌ Fn π« π) |
14 | | dssmapclsntr.o |
. . . . . 6
β’ π = (π β V β¦ (π β (π« π βm π« π) β¦ (π β π« π β¦ (π β (πβ(π β π )))))) |
15 | | dssmapclsntr.d |
. . . . . 6
β’ π· = (πβπ) |
16 | 9 | topopn 22399 |
. . . . . 6
β’ (π½ β Top β π β π½) |
17 | 14, 15, 16 | dssmapf1od 42757 |
. . . . 5
β’ (π½ β Top β π·:(π« π βm π« π)β1-1-ontoβ(π« π βm π« π)) |
18 | | f1of 6830 |
. . . . 5
β’ (π·:(π« π βm π« π)β1-1-ontoβ(π« π βm π« π) β π·:(π« π βm π« π)βΆ(π« π βm π«
π)) |
19 | 17, 18 | syl 17 |
. . . 4
β’ (π½ β Top β π·:(π« π βm π« π)βΆ(π« π βm π«
π)) |
20 | | dssmapclsntr.k |
. . . . 5
β’ πΎ = (clsβπ½) |
21 | 9, 20 | clselmap 42863 |
. . . 4
β’ (π½ β Top β πΎ β (π« π βm π«
π)) |
22 | 19, 21 | ffvelcdmd 7084 |
. . 3
β’ (π½ β Top β (π·βπΎ) β (π« π βm π« π)) |
23 | | elmapfn 8855 |
. . 3
β’ ((π·βπΎ) β (π« π βm π« π) β (π·βπΎ) Fn π« π) |
24 | 22, 23 | syl 17 |
. 2
β’ (π½ β Top β (π·βπΎ) Fn π« π) |
25 | | elpwi 4608 |
. . . . 5
β’ (π‘ β π« π β π‘ β π) |
26 | 9 | ntrval2 22546 |
. . . . 5
β’ ((π½ β Top β§ π‘ β π) β ((intβπ½)βπ‘) = (π β ((clsβπ½)β(π β π‘)))) |
27 | 25, 26 | sylan2 593 |
. . . 4
β’ ((π½ β Top β§ π‘ β π« π) β ((intβπ½)βπ‘) = (π β ((clsβπ½)β(π β π‘)))) |
28 | 8 | fveq1i 6889 |
. . . 4
β’ (πΌβπ‘) = ((intβπ½)βπ‘) |
29 | 20 | fveq1i 6889 |
. . . . 5
β’ (πΎβ(π β π‘)) = ((clsβπ½)β(π β π‘)) |
30 | 29 | difeq2i 4118 |
. . . 4
β’ (π β (πΎβ(π β π‘))) = (π β ((clsβπ½)β(π β π‘))) |
31 | 27, 28, 30 | 3eqtr4g 2797 |
. . 3
β’ ((π½ β Top β§ π‘ β π« π) β (πΌβπ‘) = (π β (πΎβ(π β π‘)))) |
32 | 16 | adantr 481 |
. . . 4
β’ ((π½ β Top β§ π‘ β π« π) β π β π½) |
33 | 21 | adantr 481 |
. . . 4
β’ ((π½ β Top β§ π‘ β π« π) β πΎ β (π« π βm π« π)) |
34 | | eqid 2732 |
. . . 4
β’ (π·βπΎ) = (π·βπΎ) |
35 | | simpr 485 |
. . . 4
β’ ((π½ β Top β§ π‘ β π« π) β π‘ β π« π) |
36 | | eqid 2732 |
. . . 4
β’ ((π·βπΎ)βπ‘) = ((π·βπΎ)βπ‘) |
37 | 14, 15, 32, 33, 34, 35, 36 | dssmapfv3d 42755 |
. . 3
β’ ((π½ β Top β§ π‘ β π« π) β ((π·βπΎ)βπ‘) = (π β (πΎβ(π β π‘)))) |
38 | 31, 37 | eqtr4d 2775 |
. 2
β’ ((π½ β Top β§ π‘ β π« π) β (πΌβπ‘) = ((π·βπΎ)βπ‘)) |
39 | 13, 24, 38 | eqfnfvd 7032 |
1
β’ (π½ β Top β πΌ = (π·βπΎ)) |