Step | Hyp | Ref
| Expression |
1 | | ima0 6077 |
. . . . . . . . 9
β’ (π β β
) =
β
|
2 | | 0ss 4397 |
. . . . . . . . 9
β’ β
β βͺ π |
3 | 1, 2 | eqsstri 4017 |
. . . . . . . 8
β’ (π β β
) β βͺ π |
4 | 3 | a1i 11 |
. . . . . . 7
β’ (((π
β Top β§ π β Top) β§ π β (π
Cn π)) β (π β β
) β βͺ π) |
5 | 4 | ralrimiva 3147 |
. . . . . 6
β’ ((π
β Top β§ π β Top) β
βπ β (π
Cn π)(π β β
) β βͺ π) |
6 | | rabid2 3465 |
. . . . . 6
β’ ((π
Cn π) = {π β (π
Cn π) β£ (π β β
) β βͺ π}
β βπ β
(π
Cn π)(π β β
) β βͺ π) |
7 | 5, 6 | sylibr 233 |
. . . . 5
β’ ((π
β Top β§ π β Top) β (π
Cn π) = {π β (π
Cn π) β£ (π β β
) β βͺ π}) |
8 | | eqid 2733 |
. . . . . 6
β’ βͺ π
=
βͺ π
|
9 | | simpl 484 |
. . . . . 6
β’ ((π
β Top β§ π β Top) β π
β Top) |
10 | | simpr 486 |
. . . . . 6
β’ ((π
β Top β§ π β Top) β π β Top) |
11 | | 0ss 4397 |
. . . . . . 7
β’ β
β βͺ π
|
12 | 11 | a1i 11 |
. . . . . 6
β’ ((π
β Top β§ π β Top) β β
β βͺ π
) |
13 | | rest0 22673 |
. . . . . . . 8
β’ (π
β Top β (π
βΎt β
) =
{β
}) |
14 | 13 | adantr 482 |
. . . . . . 7
β’ ((π
β Top β§ π β Top) β (π
βΎt β
) =
{β
}) |
15 | | 0cmp 22898 |
. . . . . . 7
β’ {β
}
β Comp |
16 | 14, 15 | eqeltrdi 2842 |
. . . . . 6
β’ ((π
β Top β§ π β Top) β (π
βΎt β
)
β Comp) |
17 | | eqid 2733 |
. . . . . . . 8
β’ βͺ π =
βͺ π |
18 | 17 | topopn 22408 |
. . . . . . 7
β’ (π β Top β βͺ π
β π) |
19 | 18 | adantl 483 |
. . . . . 6
β’ ((π
β Top β§ π β Top) β βͺ π
β π) |
20 | 8, 9, 10, 12, 16, 19 | xkoopn 23093 |
. . . . 5
β’ ((π
β Top β§ π β Top) β {π β (π
Cn π) β£ (π β β
) β βͺ π}
β (π
βko π
)) |
21 | 7, 20 | eqeltrd 2834 |
. . . 4
β’ ((π
β Top β§ π β Top) β (π
Cn π) β (π βko π
)) |
22 | | xkouni.1 |
. . . 4
β’ π½ = (π βko π
) |
23 | 21, 22 | eleqtrrdi 2845 |
. . 3
β’ ((π
β Top β§ π β Top) β (π
Cn π) β π½) |
24 | | elssuni 4942 |
. . 3
β’ ((π
Cn π) β π½ β (π
Cn π) β βͺ π½) |
25 | 23, 24 | syl 17 |
. 2
β’ ((π
β Top β§ π β Top) β (π
Cn π) β βͺ π½) |
26 | | eqid 2733 |
. . . . . 6
β’ {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp} = {π₯ β
π« βͺ π
β£ (π
βΎt π₯) β Comp} |
27 | | eqid 2733 |
. . . . . 6
β’ (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) = (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) |
28 | 8, 26, 27 | xkoval 23091 |
. . . . 5
β’ ((π
β Top β§ π β Top) β (π βko π
) = (topGenβ(fiβran
(π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£})))) |
29 | 28 | unieqd 4923 |
. . . 4
β’ ((π
β Top β§ π β Top) β βͺ (π
βko π
) =
βͺ (topGenβ(fiβran (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£})))) |
30 | 22 | unieqi 4922 |
. . . 4
β’ βͺ π½ =
βͺ (π βko π
) |
31 | | ovex 7442 |
. . . . . . . 8
β’ (π
Cn π) β V |
32 | 31 | pwex 5379 |
. . . . . . 7
β’ π«
(π
Cn π) β V |
33 | 8, 26, 27 | xkotf 23089 |
. . . . . . . 8
β’ (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}):({π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp} Γ π)βΆπ« (π
Cn π) |
34 | | frn 6725 |
. . . . . . . 8
β’ ((π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}):({π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp} Γ π)βΆπ« (π
Cn π) β ran (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β π« (π
Cn π)) |
35 | 33, 34 | ax-mp 5 |
. . . . . . 7
β’ ran
(π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β π« (π
Cn π) |
36 | 32, 35 | ssexi 5323 |
. . . . . 6
β’ ran
(π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β V |
37 | | fiuni 9423 |
. . . . . 6
β’ (ran
(π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β V β βͺ ran (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) = βͺ
(fiβran (π β
{π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}))) |
38 | 36, 37 | ax-mp 5 |
. . . . 5
β’ βͺ ran (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) = βͺ
(fiβran (π β
{π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£})) |
39 | | fvex 6905 |
. . . . . 6
β’
(fiβran (π
β {π₯ β π«
βͺ π
β£ (π
βΎt π₯) β Comp}, π£ β π β¦ {π β (π
Cn π) β£ (π β π) β π£})) β V |
40 | | unitg 22470 |
. . . . . 6
β’
((fiβran (π
β {π₯ β π«
βͺ π
β£ (π
βΎt π₯) β Comp}, π£ β π β¦ {π β (π
Cn π) β£ (π β π) β π£})) β V β βͺ (topGenβ(fiβran (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}))) = βͺ
(fiβran (π β
{π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}))) |
41 | 39, 40 | ax-mp 5 |
. . . . 5
β’ βͺ (topGenβ(fiβran (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}))) = βͺ
(fiβran (π β
{π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£})) |
42 | 38, 41 | eqtr4i 2764 |
. . . 4
β’ βͺ ran (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) = βͺ
(topGenβ(fiβran (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}))) |
43 | 29, 30, 42 | 3eqtr4g 2798 |
. . 3
β’ ((π
β Top β§ π β Top) β βͺ π½ =
βͺ ran (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£})) |
44 | 35 | a1i 11 |
. . . 4
β’ ((π
β Top β§ π β Top) β ran (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β π« (π
Cn π)) |
45 | | sspwuni 5104 |
. . . 4
β’ (ran
(π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β π« (π
Cn π) β βͺ ran
(π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β (π
Cn π)) |
46 | 44, 45 | sylib 217 |
. . 3
β’ ((π
β Top β§ π β Top) β βͺ ran (π β {π₯ β π« βͺ π
β£ (π
βΎt π₯)
β Comp}, π£ β
π β¦ {π β (π
Cn π) β£ (π β π) β π£}) β (π
Cn π)) |
47 | 43, 46 | eqsstrd 4021 |
. 2
β’ ((π
β Top β§ π β Top) β βͺ π½
β (π
Cn π)) |
48 | 25, 47 | eqssd 4000 |
1
β’ ((π
β Top β§ π β Top) β (π
Cn π) = βͺ π½) |