Step | Hyp | Ref
| Expression |
1 | | ptcmp.3 |
. . . . . . 7
β’ (π β π΄ β π) |
2 | | ptcmp.4 |
. . . . . . . 8
β’ (π β πΉ:π΄βΆComp) |
3 | 2 | ffnd 6673 |
. . . . . . 7
β’ (π β πΉ Fn π΄) |
4 | | eqid 2733 |
. . . . . . . 8
β’ {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} |
5 | 4 | ptval 22944 |
. . . . . . 7
β’ ((π΄ β π β§ πΉ Fn π΄) β (βtβπΉ) = (topGenβ{π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))})) |
6 | 1, 3, 5 | syl2anc 585 |
. . . . . 6
β’ (π β
(βtβπΉ) = (topGenβ{π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))})) |
7 | | cmptop 22769 |
. . . . . . . . . . 11
β’ (π₯ β Comp β π₯ β Top) |
8 | 7 | ssriv 3952 |
. . . . . . . . . 10
β’ Comp
β Top |
9 | | fss 6689 |
. . . . . . . . . 10
β’ ((πΉ:π΄βΆComp β§ Comp β Top) β
πΉ:π΄βΆTop) |
10 | 2, 8, 9 | sylancl 587 |
. . . . . . . . 9
β’ (π β πΉ:π΄βΆTop) |
11 | | ptcmp.2 |
. . . . . . . . . 10
β’ π = Xπ β π΄ βͺ (πΉβπ) |
12 | 4, 11 | ptbasfi 22955 |
. . . . . . . . 9
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} = (fiβ({π} βͺ ran (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’))))) |
13 | 1, 10, 12 | syl2anc 585 |
. . . . . . . 8
β’ (π β {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} = (fiβ({π} βͺ ran (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’))))) |
14 | | uncom 4117 |
. . . . . . . . . 10
β’ (ran
π βͺ {π}) = ({π} βͺ ran π) |
15 | | ptcmp.1 |
. . . . . . . . . . . 12
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) |
16 | 15 | rneqi 5896 |
. . . . . . . . . . 11
β’ ran π = ran (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) |
17 | 16 | uneq2i 4124 |
. . . . . . . . . 10
β’ ({π} βͺ ran π) = ({π} βͺ ran (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’))) |
18 | 14, 17 | eqtri 2761 |
. . . . . . . . 9
β’ (ran
π βͺ {π}) = ({π} βͺ ran (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’))) |
19 | 18 | fveq2i 6849 |
. . . . . . . 8
β’
(fiβ(ran π
βͺ {π})) =
(fiβ({π} βͺ ran
(π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)))) |
20 | 13, 19 | eqtr4di 2791 |
. . . . . . 7
β’ (π β {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} = (fiβ(ran π βͺ {π}))) |
21 | 20 | fveq2d 6850 |
. . . . . 6
β’ (π β (topGenβ{π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))}) = (topGenβ(fiβ(ran π βͺ {π})))) |
22 | 6, 21 | eqtrd 2773 |
. . . . 5
β’ (π β
(βtβπΉ) = (topGenβ(fiβ(ran π βͺ {π})))) |
23 | 22 | unieqd 4883 |
. . . 4
β’ (π β βͺ (βtβπΉ) = βͺ
(topGenβ(fiβ(ran π βͺ {π})))) |
24 | | fibas 22350 |
. . . . 5
β’
(fiβ(ran π
βͺ {π})) β
TopBases |
25 | | unitg 22340 |
. . . . 5
β’
((fiβ(ran π
βͺ {π})) β TopBases
β βͺ (topGenβ(fiβ(ran π βͺ {π}))) = βͺ
(fiβ(ran π βͺ
{π}))) |
26 | 24, 25 | ax-mp 5 |
. . . 4
β’ βͺ (topGenβ(fiβ(ran π βͺ {π}))) = βͺ
(fiβ(ran π βͺ
{π})) |
27 | 23, 26 | eqtrdi 2789 |
. . 3
β’ (π β βͺ (βtβπΉ) = βͺ
(fiβ(ran π βͺ
{π}))) |
28 | | eqid 2733 |
. . . . . 6
β’
(βtβπΉ) = (βtβπΉ) |
29 | 28 | ptuni 22968 |
. . . . 5
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β Xπ β
π΄ βͺ (πΉβπ) = βͺ
(βtβπΉ)) |
30 | 1, 10, 29 | syl2anc 585 |
. . . 4
β’ (π β Xπ β
π΄ βͺ (πΉβπ) = βͺ
(βtβπΉ)) |
31 | 11, 30 | eqtrid 2785 |
. . 3
β’ (π β π = βͺ
(βtβπΉ)) |
32 | | ptcmp.5 |
. . . . . . 7
β’ (π β π β (UFL β© dom
card)) |
33 | 32 | pwexd 5338 |
. . . . . 6
β’ (π β π« π β V) |
34 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π€ β π β¦ (π€βπ)) = (π€ β π β¦ (π€βπ)) |
35 | 34 | mptpreima 6194 |
. . . . . . . . . . 11
β’ (β‘(π€ β π β¦ (π€βπ)) β π’) = {π€ β π β£ (π€βπ) β π’} |
36 | 35 | ssrab3 4044 |
. . . . . . . . . 10
β’ (β‘(π€ β π β¦ (π€βπ)) β π’) β π |
37 | 32 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΄ β§ π’ β (πΉβπ))) β π β (UFL β© dom
card)) |
38 | | elpw2g 5305 |
. . . . . . . . . . 11
β’ (π β (UFL β© dom card)
β ((β‘(π€ β π β¦ (π€βπ)) β π’) β π« π β (β‘(π€ β π β¦ (π€βπ)) β π’) β π)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ (π β π΄ β§ π’ β (πΉβπ))) β ((β‘(π€ β π β¦ (π€βπ)) β π’) β π« π β (β‘(π€ β π β¦ (π€βπ)) β π’) β π)) |
40 | 36, 39 | mpbiri 258 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ π’ β (πΉβπ))) β (β‘(π€ β π β¦ (π€βπ)) β π’) β π« π) |
41 | 40 | ralrimivva 3194 |
. . . . . . . 8
β’ (π β βπ β π΄ βπ’ β (πΉβπ)(β‘(π€ β π β¦ (π€βπ)) β π’) β π« π) |
42 | 15 | fmpox 8003 |
. . . . . . . 8
β’
(βπ β
π΄ βπ’ β (πΉβπ)(β‘(π€ β π β¦ (π€βπ)) β π’) β π« π β π:βͺ π β π΄ ({π} Γ (πΉβπ))βΆπ« π) |
43 | 41, 42 | sylib 217 |
. . . . . . 7
β’ (π β π:βͺ π β π΄ ({π} Γ (πΉβπ))βΆπ« π) |
44 | 43 | frnd 6680 |
. . . . . 6
β’ (π β ran π β π« π) |
45 | 33, 44 | ssexd 5285 |
. . . . 5
β’ (π β ran π β V) |
46 | | snex 5392 |
. . . . 5
β’ {π} β V |
47 | | unexg 7687 |
. . . . 5
β’ ((ran
π β V β§ {π} β V) β (ran π βͺ {π}) β V) |
48 | 45, 46, 47 | sylancl 587 |
. . . 4
β’ (π β (ran π βͺ {π}) β V) |
49 | | fiuni 9372 |
. . . 4
β’ ((ran
π βͺ {π}) β V β βͺ (ran π βͺ {π}) = βͺ
(fiβ(ran π βͺ
{π}))) |
50 | 48, 49 | syl 17 |
. . 3
β’ (π β βͺ (ran π βͺ {π}) = βͺ
(fiβ(ran π βͺ
{π}))) |
51 | 27, 31, 50 | 3eqtr4d 2783 |
. 2
β’ (π β π = βͺ (ran π βͺ {π})) |
52 | 51, 22 | jca 513 |
1
β’ (π β (π = βͺ (ran π βͺ {π}) β§ (βtβπΉ) = (topGenβ(fiβ(ran
π βͺ {π}))))) |