Step | Hyp | Ref
| Expression |
1 | | cmetmet 24653 |
. . . . 5
β’ (π· β (CMetβπ) β π· β (Metβπ)) |
2 | | metxmet 23690 |
. . . . 5
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π· β (CMetβπ) β π· β (βMetβπ)) |
4 | | bcth.2 |
. . . . . . . . . 10
β’ π½ = (MetOpenβπ·) |
5 | 4 | mopntop 23796 |
. . . . . . . . 9
β’ (π· β (βMetβπ) β π½ β Top) |
6 | 5 | ad2antrr 725 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β π½ β Top) |
7 | | ffvelcdm 7033 |
. . . . . . . . . 10
β’ ((π:ββΆπ½ β§ π β β) β (πβπ) β π½) |
8 | | elssuni 4899 |
. . . . . . . . . 10
β’ ((πβπ) β π½ β (πβπ) β βͺ π½) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
β’ ((π:ββΆπ½ β§ π β β) β (πβπ) β βͺ π½) |
10 | 9 | adantll 713 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β (πβπ) β βͺ π½) |
11 | | eqid 2737 |
. . . . . . . . 9
β’ βͺ π½ =
βͺ π½ |
12 | 11 | clsval2 22404 |
. . . . . . . 8
β’ ((π½ β Top β§ (πβπ) β βͺ π½) β ((clsβπ½)β(πβπ)) = (βͺ π½ β ((intβπ½)β(βͺ π½
β (πβπ))))) |
13 | 6, 10, 12 | syl2anc 585 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β ((clsβπ½)β(πβπ)) = (βͺ π½ β ((intβπ½)β(βͺ π½
β (πβπ))))) |
14 | 4 | mopnuni 23797 |
. . . . . . . 8
β’ (π· β (βMetβπ) β π = βͺ π½) |
15 | 14 | ad2antrr 725 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β π = βͺ π½) |
16 | 13, 15 | eqeq12d 2753 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β (((clsβπ½)β(πβπ)) = π β (βͺ π½ β ((intβπ½)β(βͺ π½
β (πβπ)))) = βͺ π½)) |
17 | | difeq2 4077 |
. . . . . . . 8
β’ ((βͺ π½
β ((intβπ½)β(βͺ π½ β (πβπ)))) = βͺ π½ β (βͺ π½
β (βͺ π½ β ((intβπ½)β(βͺ π½ β (πβπ))))) = (βͺ π½ β βͺ π½)) |
18 | | difid 4331 |
. . . . . . . 8
β’ (βͺ π½
β βͺ π½) = β
|
19 | 17, 18 | eqtrdi 2793 |
. . . . . . 7
β’ ((βͺ π½
β ((intβπ½)β(βͺ π½ β (πβπ)))) = βͺ π½ β (βͺ π½
β (βͺ π½ β ((intβπ½)β(βͺ π½ β (πβπ))))) = β
) |
20 | | difss 4092 |
. . . . . . . . . . . 12
β’ (βͺ π½
β (πβπ)) β βͺ π½ |
21 | 11 | ntropn 22403 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ (βͺ π½
β (πβπ)) β βͺ π½)
β ((intβπ½)β(βͺ π½ β (πβπ))) β π½) |
22 | 6, 20, 21 | sylancl 587 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β ((intβπ½)β(βͺ π½
β (πβπ))) β π½) |
23 | | elssuni 4899 |
. . . . . . . . . . 11
β’
(((intβπ½)β(βͺ π½ β (πβπ))) β π½ β ((intβπ½)β(βͺ π½ β (πβπ))) β βͺ
π½) |
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β ((intβπ½)β(βͺ π½
β (πβπ))) β βͺ π½) |
25 | | dfss4 4219 |
. . . . . . . . . 10
β’
(((intβπ½)β(βͺ π½ β (πβπ))) β βͺ
π½ β (βͺ π½
β (βͺ π½ β ((intβπ½)β(βͺ π½ β (πβπ))))) = ((intβπ½)β(βͺ π½ β (πβπ)))) |
26 | 24, 25 | sylib 217 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β (βͺ π½
β (βͺ π½ β ((intβπ½)β(βͺ π½ β (πβπ))))) = ((intβπ½)β(βͺ π½ β (πβπ)))) |
27 | | id 22 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
28 | | elfvdm 6880 |
. . . . . . . . . . . . . 14
β’ (π· β (βMetβπ) β π β dom βMet) |
29 | 28 | difexd 5287 |
. . . . . . . . . . . . 13
β’ (π· β (βMetβπ) β (π β (πβπ)) β V) |
30 | 29 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β (π β (πβπ)) β V) |
31 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
32 | 31 | difeq2d 4083 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (π β (πβπ₯)) = (π β (πβπ))) |
33 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π₯ β β β¦ (π β (πβπ₯))) = (π₯ β β β¦ (π β (πβπ₯))) |
34 | 32, 33 | fvmptg 6947 |
. . . . . . . . . . . 12
β’ ((π β β β§ (π β (πβπ)) β V) β ((π₯ β β β¦ (π β (πβπ₯)))βπ) = (π β (πβπ))) |
35 | 27, 30, 34 | syl2anr 598 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β ((π₯ β β β¦ (π β (πβπ₯)))βπ) = (π β (πβπ))) |
36 | 15 | difeq1d 4082 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β (π β (πβπ)) = (βͺ π½ β (πβπ))) |
37 | 35, 36 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β ((π₯ β β β¦ (π β (πβπ₯)))βπ) = (βͺ π½ β (πβπ))) |
38 | 37 | fveq2d 6847 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β ((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) = ((intβπ½)β(βͺ π½ β (πβπ)))) |
39 | 26, 38 | eqtr4d 2780 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β (βͺ π½
β (βͺ π½ β ((intβπ½)β(βͺ π½ β (πβπ))))) = ((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ))) |
40 | 39 | eqeq1d 2739 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β ((βͺ π½
β (βͺ π½ β ((intβπ½)β(βͺ π½ β (πβπ))))) = β
β ((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) = β
)) |
41 | 19, 40 | imbitrid 243 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β ((βͺ π½
β ((intβπ½)β(βͺ π½ β (πβπ)))) = βͺ π½ β ((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) = β
)) |
42 | 16, 41 | sylbid 239 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β (((clsβπ½)β(πβπ)) = π β ((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) = β
)) |
43 | 42 | ralimdva 3165 |
. . . 4
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β (βπ β β ((clsβπ½)β(πβπ)) = π β βπ β β ((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) = β
)) |
44 | 3, 43 | sylan 581 |
. . 3
β’ ((π· β (CMetβπ) β§ π:ββΆπ½) β (βπ β β ((clsβπ½)β(πβπ)) = π β βπ β β ((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) = β
)) |
45 | | ffvelcdm 7033 |
. . . . . . . . 9
β’ ((π:ββΆπ½ β§ π₯ β β) β (πβπ₯) β π½) |
46 | 14 | difeq1d 4082 |
. . . . . . . . . . 11
β’ (π· β (βMetβπ) β (π β (πβπ₯)) = (βͺ π½ β (πβπ₯))) |
47 | 46 | adantr 482 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ (πβπ₯) β π½) β (π β (πβπ₯)) = (βͺ π½ β (πβπ₯))) |
48 | 11 | opncld 22387 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ (πβπ₯) β π½) β (βͺ π½ β (πβπ₯)) β (Clsdβπ½)) |
49 | 5, 48 | sylan 581 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ (πβπ₯) β π½) β (βͺ π½ β (πβπ₯)) β (Clsdβπ½)) |
50 | 47, 49 | eqeltrd 2838 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ (πβπ₯) β π½) β (π β (πβπ₯)) β (Clsdβπ½)) |
51 | 45, 50 | sylan2 594 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ (π:ββΆπ½ β§ π₯ β β)) β (π β (πβπ₯)) β (Clsdβπ½)) |
52 | 51 | anassrs 469 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π₯ β β) β (π β (πβπ₯)) β (Clsdβπ½)) |
53 | 52 | ralrimiva 3144 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β βπ₯ β β (π β (πβπ₯)) β (Clsdβπ½)) |
54 | 3, 53 | sylan 581 |
. . . . 5
β’ ((π· β (CMetβπ) β§ π:ββΆπ½) β βπ₯ β β (π β (πβπ₯)) β (Clsdβπ½)) |
55 | 33 | fmpt 7059 |
. . . . 5
β’
(βπ₯ β
β (π β (πβπ₯)) β (Clsdβπ½) β (π₯ β β β¦ (π β (πβπ₯))):ββΆ(Clsdβπ½)) |
56 | 54, 55 | sylib 217 |
. . . 4
β’ ((π· β (CMetβπ) β§ π:ββΆπ½) β (π₯ β β β¦ (π β (πβπ₯))):ββΆ(Clsdβπ½)) |
57 | | nne 2948 |
. . . . . . 7
β’ (Β¬
((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) β β
β ((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) = β
) |
58 | 57 | ralbii 3097 |
. . . . . 6
β’
(βπ β
β Β¬ ((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) β β
β βπ β β
((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) = β
) |
59 | | ralnex 3076 |
. . . . . 6
β’
(βπ β
β Β¬ ((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) β β
β Β¬ βπ β β
((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) β β
) |
60 | 58, 59 | bitr3i 277 |
. . . . 5
β’
(βπ β
β ((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) = β
β Β¬ βπ β β
((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) β β
) |
61 | 4 | bcth 24696 |
. . . . . . 7
β’ ((π· β (CMetβπ) β§ (π₯ β β β¦ (π β (πβπ₯))):ββΆ(Clsdβπ½) β§ ((intβπ½)ββͺ ran (π₯ β β β¦ (π β (πβπ₯)))) β β
) β βπ β β
((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) β β
) |
62 | 61 | 3expia 1122 |
. . . . . 6
β’ ((π· β (CMetβπ) β§ (π₯ β β β¦ (π β (πβπ₯))):ββΆ(Clsdβπ½)) β (((intβπ½)ββͺ ran (π₯ β β β¦ (π β (πβπ₯)))) β β
β βπ β β
((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) β β
)) |
63 | 62 | necon1bd 2962 |
. . . . 5
β’ ((π· β (CMetβπ) β§ (π₯ β β β¦ (π β (πβπ₯))):ββΆ(Clsdβπ½)) β (Β¬ βπ β β
((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) β β
β ((intβπ½)ββͺ ran (π₯ β β β¦ (π β (πβπ₯)))) = β
)) |
64 | 60, 63 | biimtrid 241 |
. . . 4
β’ ((π· β (CMetβπ) β§ (π₯ β β β¦ (π β (πβπ₯))):ββΆ(Clsdβπ½)) β (βπ β β
((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) = β
β ((intβπ½)ββͺ ran (π₯ β β β¦ (π β (πβπ₯)))) = β
)) |
65 | 56, 64 | syldan 592 |
. . 3
β’ ((π· β (CMetβπ) β§ π:ββΆπ½) β (βπ β β ((intβπ½)β((π₯ β β β¦ (π β (πβπ₯)))βπ)) = β
β ((intβπ½)ββͺ ran (π₯ β β β¦ (π β (πβπ₯)))) = β
)) |
66 | | difeq2 4077 |
. . . . 5
β’
(((intβπ½)ββͺ ran
(π₯ β β β¦
(π β (πβπ₯)))) = β
β (βͺ π½
β ((intβπ½)ββͺ ran
(π₯ β β β¦
(π β (πβπ₯))))) = (βͺ π½ β
β
)) |
67 | 28 | difexd 5287 |
. . . . . . . . . . . . . . 15
β’ (π· β (βMetβπ) β (π β (πβπ₯)) β V) |
68 | 67 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π₯ β β) β (π β (πβπ₯)) β V) |
69 | 68 | ralrimiva 3144 |
. . . . . . . . . . . . 13
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β βπ₯ β β (π β (πβπ₯)) β V) |
70 | 33 | fnmpt 6642 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
β (π β (πβπ₯)) β V β (π₯ β β β¦ (π β (πβπ₯))) Fn β) |
71 | | fniunfv 7195 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β¦ (π β (πβπ₯))) Fn β β βͺ π β β ((π₯ β β β¦ (π β (πβπ₯)))βπ) = βͺ ran (π₯ β β β¦ (π β (πβπ₯)))) |
72 | 69, 70, 71 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β βͺ
π β β ((π₯ β β β¦ (π β (πβπ₯)))βπ) = βͺ ran (π₯ β β β¦ (π β (πβπ₯)))) |
73 | 35 | iuneq2dv 4979 |
. . . . . . . . . . . . 13
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β βͺ
π β β ((π₯ β β β¦ (π β (πβπ₯)))βπ) = βͺ π β β (π β (πβπ))) |
74 | 32 | cbviunv 5001 |
. . . . . . . . . . . . 13
β’ βͺ π₯ β β (π β (πβπ₯)) = βͺ
π β β (π β (πβπ)) |
75 | 73, 74 | eqtr4di 2795 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β βͺ
π β β ((π₯ β β β¦ (π β (πβπ₯)))βπ) = βͺ π₯ β β (π β (πβπ₯))) |
76 | 72, 75 | eqtr3d 2779 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β βͺ ran
(π₯ β β β¦
(π β (πβπ₯))) = βͺ
π₯ β β (π β (πβπ₯))) |
77 | | iundif2 5035 |
. . . . . . . . . . 11
β’ βͺ π₯ β β (π β (πβπ₯)) = (π β β©
π₯ β β (πβπ₯)) |
78 | 76, 77 | eqtrdi 2793 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β βͺ ran
(π₯ β β β¦
(π β (πβπ₯))) = (π β β©
π₯ β β (πβπ₯))) |
79 | | ffn 6669 |
. . . . . . . . . . . . 13
β’ (π:ββΆπ½ β π Fn β) |
80 | 79 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β π Fn β) |
81 | | fniinfv 6920 |
. . . . . . . . . . . 12
β’ (π Fn β β β© π₯ β β (πβπ₯) = β© ran π) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β β©
π₯ β β (πβπ₯) = β© ran π) |
83 | 82 | difeq2d 4083 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β (π β β©
π₯ β β (πβπ₯)) = (π β β© ran
π)) |
84 | 14 | adantr 482 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β π = βͺ π½) |
85 | 84 | difeq1d 4082 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β (π β β© ran
π) = (βͺ π½
β β© ran π)) |
86 | 78, 83, 85 | 3eqtrd 2781 |
. . . . . . . . 9
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β βͺ ran
(π₯ β β β¦
(π β (πβπ₯))) = (βͺ π½ β β© ran π)) |
87 | 86 | fveq2d 6847 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β ((intβπ½)ββͺ ran
(π₯ β β β¦
(π β (πβπ₯)))) = ((intβπ½)β(βͺ π½ β β© ran π))) |
88 | 87 | difeq2d 4083 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β (βͺ π½ β ((intβπ½)ββͺ ran (π₯ β β β¦ (π β (πβπ₯))))) = (βͺ π½ β ((intβπ½)β(βͺ π½
β β© ran π)))) |
89 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β π½ β Top) |
90 | | 1nn 12165 |
. . . . . . . . 9
β’ 1 β
β |
91 | | biidd 262 |
. . . . . . . . . 10
β’ (π = 1 β (((π· β (βMetβπ) β§ π:ββΆπ½) β β© ran
π β βͺ π½)
β ((π· β
(βMetβπ) β§
π:ββΆπ½) β β© ran π β βͺ π½))) |
92 | | fnfvelrn 7032 |
. . . . . . . . . . . . . 14
β’ ((π Fn β β§ π β β) β (πβπ) β ran π) |
93 | 80, 92 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β (πβπ) β ran π) |
94 | | intss1 4925 |
. . . . . . . . . . . . 13
β’ ((πβπ) β ran π β β© ran
π β (πβπ)) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . 12
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β β© ran π β (πβπ)) |
96 | 95, 10 | sstrd 3955 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ π:ββΆπ½) β§ π β β) β β© ran π β βͺ π½) |
97 | 96 | expcom 415 |
. . . . . . . . . 10
β’ (π β β β ((π· β (βMetβπ) β§ π:ββΆπ½) β β© ran
π β βͺ π½)) |
98 | 91, 97 | vtoclga 3535 |
. . . . . . . . 9
β’ (1 β
β β ((π· β
(βMetβπ) β§
π:ββΆπ½) β β© ran π β βͺ π½)) |
99 | 90, 98 | ax-mp 5 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β β© ran
π β βͺ π½) |
100 | 11 | clsval2 22404 |
. . . . . . . 8
β’ ((π½ β Top β§ β© ran π β βͺ π½) β ((clsβπ½)ββ© ran π) = (βͺ π½ β ((intβπ½)β(βͺ π½
β β© ran π)))) |
101 | 89, 99, 100 | syl2anc 585 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β ((clsβπ½)ββ© ran
π) = (βͺ π½
β ((intβπ½)β(βͺ π½ β β© ran π)))) |
102 | 88, 101 | eqtr4d 2780 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β (βͺ π½ β ((intβπ½)ββͺ ran (π₯ β β β¦ (π β (πβπ₯))))) = ((clsβπ½)ββ© ran
π)) |
103 | | dif0 4333 |
. . . . . . 7
β’ (βͺ π½
β β
) = βͺ π½ |
104 | 103, 84 | eqtr4id 2796 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β (βͺ π½ β β
) = π) |
105 | 102, 104 | eqeq12d 2753 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β ((βͺ
π½ β ((intβπ½)ββͺ ran (π₯ β β β¦ (π β (πβπ₯))))) = (βͺ π½ β β
) β
((clsβπ½)ββ© ran π) = π)) |
106 | 66, 105 | imbitrid 243 |
. . . 4
β’ ((π· β (βMetβπ) β§ π:ββΆπ½) β (((intβπ½)ββͺ ran
(π₯ β β β¦
(π β (πβπ₯)))) = β
β ((clsβπ½)ββ© ran π) = π)) |
107 | 3, 106 | sylan 581 |
. . 3
β’ ((π· β (CMetβπ) β§ π:ββΆπ½) β (((intβπ½)ββͺ ran
(π₯ β β β¦
(π β (πβπ₯)))) = β
β ((clsβπ½)ββ© ran π) = π)) |
108 | 44, 65, 107 | 3syld 60 |
. 2
β’ ((π· β (CMetβπ) β§ π:ββΆπ½) β (βπ β β ((clsβπ½)β(πβπ)) = π β ((clsβπ½)ββ© ran
π) = π)) |
109 | 108 | 3impia 1118 |
1
β’ ((π· β (CMetβπ) β§ π:ββΆπ½ β§ βπ β β ((clsβπ½)β(πβπ)) = π) β ((clsβπ½)ββ© ran
π) = π) |