Step | Hyp | Ref
| Expression |
1 | | topgele 22653 |
. . . 4
β’ (π΅ β (TopOnβπ΄) β ({β
, π΄} β π΅ β§ π΅ β π« π΄)) |
2 | 1 | adantl 481 |
. . 3
β’ ((πΆ β π΅ β§ π΅ β (TopOnβπ΄)) β ({β
, π΄} β π΅ β§ π΅ β π« π΄)) |
3 | 2 | simprd 495 |
. 2
β’ ((πΆ β π΅ β§ π΅ β (TopOnβπ΄)) β π΅ β π« π΄) |
4 | | velpw 4608 |
. . . . . . 7
β’ (π₯ β π« π΄ β π₯ β π΄) |
5 | | simp3 1137 |
. . . . . . . . . 10
β’ ((πΆ β π΅ β§ π₯ β π΄ β§ π΅ β (TopOnβπ΄)) β π΅ β (TopOnβπ΄)) |
6 | | df-ima 5690 |
. . . . . . . . . . . . . . . . . 18
β’ ((π§ β π΄ β¦ {π§}) β π₯) = ran ((π§ β π΄ β¦ {π§}) βΎ π₯) |
7 | | resmpt 6038 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β π΄ β ((π§ β π΄ β¦ {π§}) βΎ π₯) = (π§ β π₯ β¦ {π§})) |
8 | 7 | rneqd 5938 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β π΄ β ran ((π§ β π΄ β¦ {π§}) βΎ π₯) = ran (π§ β π₯ β¦ {π§})) |
9 | 6, 8 | eqtrid 2783 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π΄ β ((π§ β π΄ β¦ {π§}) β π₯) = ran (π§ β π₯ β¦ {π§})) |
10 | | rnmptsn 36520 |
. . . . . . . . . . . . . . . . 17
β’ ran
(π§ β π₯ β¦ {π§}) = {π’ β£ βπ§ β π₯ π’ = {π§}} |
11 | 9, 10 | eqtrdi 2787 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π΄ β ((π§ β π΄ β¦ {π§}) β π₯) = {π’ β£ βπ§ β π₯ π’ = {π§}}) |
12 | | imassrn 6071 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β π΄ β¦ {π§}) β π₯) β ran (π§ β π΄ β¦ {π§}) |
13 | 11, 12 | eqsstrrdi 4038 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π΄ β {π’ β£ βπ§ β π₯ π’ = {π§}} β ran (π§ β π΄ β¦ {π§})) |
14 | | rnmptsn 36520 |
. . . . . . . . . . . . . . 15
β’ ran
(π§ β π΄ β¦ {π§}) = {π’ β£ βπ§ β π΄ π’ = {π§}} |
15 | 13, 14 | sseqtrdi 4033 |
. . . . . . . . . . . . . 14
β’ (π₯ β π΄ β {π’ β£ βπ§ β π₯ π’ = {π§}} β {π’ β£ βπ§ β π΄ π’ = {π§}}) |
16 | | dissneq.c |
. . . . . . . . . . . . . . 15
β’ πΆ = {π’ β£ βπ₯ β π΄ π’ = {π₯}} |
17 | | sneq 4639 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π§ β {π₯} = {π§}) |
18 | 17 | eqeq2d 2742 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π§ β (π’ = {π₯} β π’ = {π§})) |
19 | 18 | cbvrexvw 3234 |
. . . . . . . . . . . . . . . 16
β’
(βπ₯ β
π΄ π’ = {π₯} β βπ§ β π΄ π’ = {π§}) |
20 | 19 | abbii 2801 |
. . . . . . . . . . . . . . 15
β’ {π’ β£ βπ₯ β π΄ π’ = {π₯}} = {π’ β£ βπ§ β π΄ π’ = {π§}} |
21 | 16, 20 | eqtri 2759 |
. . . . . . . . . . . . . 14
β’ πΆ = {π’ β£ βπ§ β π΄ π’ = {π§}} |
22 | 15, 21 | sseqtrrdi 4034 |
. . . . . . . . . . . . 13
β’ (π₯ β π΄ β {π’ β£ βπ§ β π₯ π’ = {π§}} β πΆ) |
23 | 22 | adantl 481 |
. . . . . . . . . . . 12
β’ ((πΆ β π΅ β§ π₯ β π΄) β {π’ β£ βπ§ β π₯ π’ = {π§}} β πΆ) |
24 | | sstr 3991 |
. . . . . . . . . . . . . 14
β’ (({π’ β£ βπ§ β π₯ π’ = {π§}} β πΆ β§ πΆ β π΅) β {π’ β£ βπ§ β π₯ π’ = {π§}} β π΅) |
25 | 24 | expcom 413 |
. . . . . . . . . . . . 13
β’ (πΆ β π΅ β ({π’ β£ βπ§ β π₯ π’ = {π§}} β πΆ β {π’ β£ βπ§ β π₯ π’ = {π§}} β π΅)) |
26 | 25 | adantr 480 |
. . . . . . . . . . . 12
β’ ((πΆ β π΅ β§ π₯ β π΄) β ({π’ β£ βπ§ β π₯ π’ = {π§}} β πΆ β {π’ β£ βπ§ β π₯ π’ = {π§}} β π΅)) |
27 | 23, 26 | mpd 15 |
. . . . . . . . . . 11
β’ ((πΆ β π΅ β§ π₯ β π΄) β {π’ β£ βπ§ β π₯ π’ = {π§}} β π΅) |
28 | 27 | 3adant3 1131 |
. . . . . . . . . 10
β’ ((πΆ β π΅ β§ π₯ β π΄ β§ π΅ β (TopOnβπ΄)) β {π’ β£ βπ§ β π₯ π’ = {π§}} β π΅) |
29 | 5, 28 | ssexd 5325 |
. . . . . . . . 9
β’ ((πΆ β π΅ β§ π₯ β π΄ β§ π΅ β (TopOnβπ΄)) β {π’ β£ βπ§ β π₯ π’ = {π§}} β V) |
30 | | isset 3486 |
. . . . . . . . 9
β’ ({π’ β£ βπ§ β π₯ π’ = {π§}} β V β βπ¦ π¦ = {π’ β£ βπ§ β π₯ π’ = {π§}}) |
31 | 29, 30 | sylib 217 |
. . . . . . . 8
β’ ((πΆ β π΅ β§ π₯ β π΄ β§ π΅ β (TopOnβπ΄)) β βπ¦ π¦ = {π’ β£ βπ§ β π₯ π’ = {π§}}) |
32 | | eqid 2731 |
. . . . . . . . . . . . . . 15
β’ (π§ β π΄ β¦ {π§}) = (π§ β π΄ β¦ {π§}) |
33 | | eqid 2731 |
. . . . . . . . . . . . . . 15
β’ {π’ β£ βπ§ β π΄ π’ = {π§}} = {π’ β£ βπ§ β π΄ π’ = {π§}} |
34 | 32, 33 | mptsnun 36524 |
. . . . . . . . . . . . . 14
β’ (π₯ β π΄ β π₯ = βͺ ((π§ β π΄ β¦ {π§}) β π₯)) |
35 | 11 | unieqd 4923 |
. . . . . . . . . . . . . 14
β’ (π₯ β π΄ β βͺ ((π§ β π΄ β¦ {π§}) β π₯) = βͺ {π’ β£ βπ§ β π₯ π’ = {π§}}) |
36 | 34, 35 | eqtrd 2771 |
. . . . . . . . . . . . 13
β’ (π₯ β π΄ β π₯ = βͺ {π’ β£ βπ§ β π₯ π’ = {π§}}) |
37 | 36 | adantl 481 |
. . . . . . . . . . . 12
β’ ((πΆ β π΅ β§ π₯ β π΄) β π₯ = βͺ {π’ β£ βπ§ β π₯ π’ = {π§}}) |
38 | 27, 37 | jca 511 |
. . . . . . . . . . 11
β’ ((πΆ β π΅ β§ π₯ β π΄) β ({π’ β£ βπ§ β π₯ π’ = {π§}} β π΅ β§ π₯ = βͺ {π’ β£ βπ§ β π₯ π’ = {π§}})) |
39 | | sseq1 4008 |
. . . . . . . . . . . 12
β’ (π¦ = {π’ β£ βπ§ β π₯ π’ = {π§}} β (π¦ β π΅ β {π’ β£ βπ§ β π₯ π’ = {π§}} β π΅)) |
40 | | unieq 4920 |
. . . . . . . . . . . . 13
β’ (π¦ = {π’ β£ βπ§ β π₯ π’ = {π§}} β βͺ π¦ = βͺ
{π’ β£ βπ§ β π₯ π’ = {π§}}) |
41 | 40 | eqeq2d 2742 |
. . . . . . . . . . . 12
β’ (π¦ = {π’ β£ βπ§ β π₯ π’ = {π§}} β (π₯ = βͺ π¦ β π₯ = βͺ {π’ β£ βπ§ β π₯ π’ = {π§}})) |
42 | 39, 41 | anbi12d 630 |
. . . . . . . . . . 11
β’ (π¦ = {π’ β£ βπ§ β π₯ π’ = {π§}} β ((π¦ β π΅ β§ π₯ = βͺ π¦) β ({π’ β£ βπ§ β π₯ π’ = {π§}} β π΅ β§ π₯ = βͺ {π’ β£ βπ§ β π₯ π’ = {π§}}))) |
43 | 38, 42 | syl5ibrcom 246 |
. . . . . . . . . 10
β’ ((πΆ β π΅ β§ π₯ β π΄) β (π¦ = {π’ β£ βπ§ β π₯ π’ = {π§}} β (π¦ β π΅ β§ π₯ = βͺ π¦))) |
44 | 43 | eximdv 1919 |
. . . . . . . . 9
β’ ((πΆ β π΅ β§ π₯ β π΄) β (βπ¦ π¦ = {π’ β£ βπ§ β π₯ π’ = {π§}} β βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦))) |
45 | 44 | 3adant3 1131 |
. . . . . . . 8
β’ ((πΆ β π΅ β§ π₯ β π΄ β§ π΅ β (TopOnβπ΄)) β (βπ¦ π¦ = {π’ β£ βπ§ β π₯ π’ = {π§}} β βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦))) |
46 | 31, 45 | mpd 15 |
. . . . . . 7
β’ ((πΆ β π΅ β§ π₯ β π΄ β§ π΅ β (TopOnβπ΄)) β βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)) |
47 | 4, 46 | syl3an2b 1403 |
. . . . . 6
β’ ((πΆ β π΅ β§ π₯ β π« π΄ β§ π΅ β (TopOnβπ΄)) β βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)) |
48 | 47 | 3com23 1125 |
. . . . 5
β’ ((πΆ β π΅ β§ π΅ β (TopOnβπ΄) β§ π₯ β π« π΄) β βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦)) |
49 | 48 | 3expia 1120 |
. . . 4
β’ ((πΆ β π΅ β§ π΅ β (TopOnβπ΄)) β (π₯ β π« π΄ β βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦))) |
50 | | topontop 22636 |
. . . . . . . 8
β’ (π΅ β (TopOnβπ΄) β π΅ β Top) |
51 | | tgtop 22697 |
. . . . . . . 8
β’ (π΅ β Top β
(topGenβπ΅) = π΅) |
52 | 50, 51 | syl 17 |
. . . . . . 7
β’ (π΅ β (TopOnβπ΄) β (topGenβπ΅) = π΅) |
53 | 52 | eleq2d 2818 |
. . . . . 6
β’ (π΅ β (TopOnβπ΄) β (π₯ β (topGenβπ΅) β π₯ β π΅)) |
54 | | eltg3 22686 |
. . . . . 6
β’ (π΅ β (TopOnβπ΄) β (π₯ β (topGenβπ΅) β βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦))) |
55 | 53, 54 | bitr3d 280 |
. . . . 5
β’ (π΅ β (TopOnβπ΄) β (π₯ β π΅ β βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦))) |
56 | 55 | adantl 481 |
. . . 4
β’ ((πΆ β π΅ β§ π΅ β (TopOnβπ΄)) β (π₯ β π΅ β βπ¦(π¦ β π΅ β§ π₯ = βͺ π¦))) |
57 | 49, 56 | sylibrd 258 |
. . 3
β’ ((πΆ β π΅ β§ π΅ β (TopOnβπ΄)) β (π₯ β π« π΄ β π₯ β π΅)) |
58 | 57 | ssrdv 3989 |
. 2
β’ ((πΆ β π΅ β§ π΅ β (TopOnβπ΄)) β π« π΄ β π΅) |
59 | 3, 58 | eqssd 4000 |
1
β’ ((πΆ β π΅ β§ π΅ β (TopOnβπ΄)) β π΅ = π« π΄) |