Step | Hyp | Ref
| Expression |
1 | | alexsubALT.1 |
. . 3
β’ π = βͺ
π½ |
2 | 1 | alexsubALTlem1 23414 |
. 2
β’ (π½ β Comp β βπ₯(π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) |
3 | 1 | alexsubALTlem4 23417 |
. . . . 5
β’ (π½ = (topGenβ(fiβπ₯)) β (βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β βπ β π«
(fiβπ₯)(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π))) |
4 | | velpw 4566 |
. . . . . . . . 9
β’ (π β π« π½ β π β π½) |
5 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = βͺ
π β (π‘ β π β π‘ β βͺ π)) |
6 | 5 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . 18
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (π‘ β π β π‘ β βͺ π)) |
7 | | eluni 4869 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π‘ β βͺ π
β βπ€(π‘ β π€ β§ π€ β π)) |
8 | | ssel 3938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π½ β (π€ β π β π€ β π½)) |
9 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π½ = (topGenβ(fiβπ₯)) β (π€ β π½ β π€ β (topGenβ(fiβπ₯)))) |
10 | | tg2 22331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π€ β
(topGenβ(fiβπ₯))
β§ π‘ β π€) β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ π¦ β π€)) |
11 | 10 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π€ β
(topGenβ(fiβπ₯))
β (π‘ β π€ β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ π¦ β π€))) |
12 | 9, 11 | syl6bi 253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π½ = (topGenβ(fiβπ₯)) β (π€ β π½ β (π‘ β π€ β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ π¦ β π€)))) |
13 | 8, 12 | sylan9r 510 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½) β (π€ β π β (π‘ β π€ β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ π¦ β π€)))) |
14 | 13 | 3impia 1118 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π€ β π) β (π‘ β π€ β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ π¦ β π€))) |
15 | | sseq2 3971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π§ = π€ β (π¦ β π§ β π¦ β π€)) |
16 | 15 | rspcev 3580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π€ β π β§ π¦ β π€) β βπ§ β π π¦ β π§) |
17 | 16 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π€ β π β (π¦ β π€ β βπ§ β π π¦ β π§)) |
18 | 17 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π€ β π) β (π¦ β π€ β βπ§ β π π¦ β π§)) |
19 | 18 | anim2d 613 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π€ β π) β ((π‘ β π¦ β§ π¦ β π€) β (π‘ β π¦ β§ βπ§ β π π¦ β π§))) |
20 | 19 | reximdv 3164 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π€ β π) β (βπ¦ β (fiβπ₯)(π‘ β π¦ β§ π¦ β π€) β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ βπ§ β π π¦ β π§))) |
21 | 14, 20 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π€ β π) β (π‘ β π€ β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ βπ§ β π π¦ β π§))) |
22 | 21 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½) β (π€ β π β (π‘ β π€ β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ βπ§ β π π¦ β π§)))) |
23 | 22 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½) β (π‘ β π€ β (π€ β π β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ βπ§ β π π¦ β π§)))) |
24 | 23 | impd 412 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½) β ((π‘ β π€ β§ π€ β π) β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ βπ§ β π π¦ β π§))) |
25 | 24 | exlimdv 1937 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½) β (βπ€(π‘ β π€ β§ π€ β π) β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ βπ§ β π π¦ β π§))) |
26 | 7, 25 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½) β (π‘ β βͺ π β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ βπ§ β π π¦ β π§))) |
27 | 26 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . 18
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (π‘ β βͺ π β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ βπ§ β π π¦ β π§))) |
28 | 6, 27 | sylbid 239 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (π‘ β π β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ βπ§ β π π¦ β π§))) |
29 | | ssel 3938 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ β π§ β (π‘ β π¦ β π‘ β π§)) |
30 | | elunii 4871 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π‘ β π§ β§ π§ β π) β π‘ β βͺ π) |
31 | 30 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π§ β π β (π‘ β π§ β π‘ β βͺ π)) |
32 | 6 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (π‘ β βͺ π β π‘ β π)) |
33 | 31, 32 | sylan9r 510 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π§ β π) β (π‘ β π§ β π‘ β π)) |
34 | 29, 33 | syl9r 78 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π§ β π) β (π¦ β π§ β (π‘ β π¦ β π‘ β π))) |
35 | 34 | rexlimdva 3149 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (βπ§ β π π¦ β π§ β (π‘ β π¦ β π‘ β π))) |
36 | 35 | com23 86 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (π‘ β π¦ β (βπ§ β π π¦ β π§ β π‘ β π))) |
37 | 36 | impd 412 |
. . . . . . . . . . . . . . . . . 18
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β ((π‘ β π¦ β§ βπ§ β π π¦ β π§) β π‘ β π)) |
38 | 37 | rexlimdvw 3154 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (βπ¦ β (fiβπ₯)(π‘ β π¦ β§ βπ§ β π π¦ β π§) β π‘ β π)) |
39 | 28, 38 | impbid 211 |
. . . . . . . . . . . . . . . 16
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (π‘ β π β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ βπ§ β π π¦ β π§))) |
40 | | elunirab 4882 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β βͺ {π¦
β (fiβπ₯) β£
βπ§ β π π¦ β π§} β βπ¦ β (fiβπ₯)(π‘ β π¦ β§ βπ§ β π π¦ β π§)) |
41 | 39, 40 | bitr4di 289 |
. . . . . . . . . . . . . . 15
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (π‘ β π β π‘ β βͺ {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§})) |
42 | 41 | eqrdv 2731 |
. . . . . . . . . . . . . 14
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β π = βͺ {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§}) |
43 | | ssrab2 4038 |
. . . . . . . . . . . . . . . 16
β’ {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β (fiβπ₯) |
44 | | fvex 6856 |
. . . . . . . . . . . . . . . . 17
β’
(fiβπ₯) β
V |
45 | 44 | elpw2 5303 |
. . . . . . . . . . . . . . . 16
β’ ({π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β π« (fiβπ₯) β {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β (fiβπ₯)) |
46 | 43, 45 | mpbir 230 |
. . . . . . . . . . . . . . 15
β’ {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β π« (fiβπ₯) |
47 | | unieq 4877 |
. . . . . . . . . . . . . . . . . 18
β’ (π = {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β βͺ π = βͺ
{π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§}) |
48 | 47 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . 17
β’ (π = {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β (π = βͺ π β π = βͺ {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§})) |
49 | | pweq 4575 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β π« π = π« {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§}) |
50 | 49 | ineq1d 4172 |
. . . . . . . . . . . . . . . . . 18
β’ (π = {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β (π« π β© Fin) = (π« {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β© Fin)) |
51 | 50 | rexeqdv 3313 |
. . . . . . . . . . . . . . . . 17
β’ (π = {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β (βπ β (π« π β© Fin)π = βͺ π β βπ β (π« {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β© Fin)π = βͺ π)) |
52 | 48, 51 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
β’ (π = {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β ((π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β (π = βͺ {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β βπ β (π« {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β© Fin)π = βͺ π))) |
53 | 52 | rspcv 3576 |
. . . . . . . . . . . . . . 15
β’ ({π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β π« (fiβπ₯) β (βπ β π«
(fiβπ₯)(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (π = βͺ {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β βπ β (π« {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β© Fin)π = βͺ π))) |
54 | 46, 53 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
(βπ β
π« (fiβπ₯)(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β (π = βͺ {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β βπ β (π« {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β© Fin)π = βͺ π)) |
55 | 42, 54 | syl5com 31 |
. . . . . . . . . . . . 13
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (βπ β π«
(fiβπ₯)(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β βπ β (π« {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β© Fin)π = βͺ π)) |
56 | | elfpw 9301 |
. . . . . . . . . . . . . . 15
β’ (π β (π« {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β© Fin) β (π β {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β§ π β Fin)) |
57 | | ssel 3938 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β (π‘ β π β π‘ β {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§})) |
58 | | sseq1 3970 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ = π‘ β (π¦ β π§ β π‘ β π§)) |
59 | 58 | rexbidv 3172 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ = π‘ β (βπ§ β π π¦ β π§ β βπ§ β π π‘ β π§)) |
60 | 59 | elrab 3646 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π‘ β {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β (π‘ β (fiβπ₯) β§ βπ§ β π π‘ β π§)) |
61 | 60 | simprbi 498 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π‘ β {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β βπ§ β π π‘ β π§) |
62 | 57, 61 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β (π‘ β π β βπ§ β π π‘ β π§)) |
63 | 62 | ralrimiv 3139 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β βπ‘ β π βπ§ β π π‘ β π§) |
64 | | sseq2 3971 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π§ = (πβπ‘) β (π‘ β π§ β π‘ β (πβπ‘))) |
65 | 64 | ac6sfi 9234 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Fin β§ βπ‘ β π βπ§ β π π‘ β π§) β βπ(π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘))) |
66 | 65 | ex 414 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Fin β
(βπ‘ β π βπ§ β π π‘ β π§ β βπ(π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)))) |
67 | 63, 66 | syl5 34 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β Fin β (π β {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β βπ(π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)))) |
68 | 67 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β (π β {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β βπ(π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)))) |
69 | | simprll 778 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β π:πβΆπ) |
70 | | frn 6676 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π:πβΆπ β ran π β π) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β ran π β π) |
72 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β π β Fin) |
73 | | ffn 6669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π:πβΆπ β π Fn π) |
74 | | dffn4 6763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π Fn π β π:πβontoβran π) |
75 | 73, 74 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π:πβΆπ β π:πβontoβran π) |
76 | 75 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β π:πβontoβran π) |
77 | 76 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β π:πβontoβran π) |
78 | | fodomfi 9272 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β Fin β§ π:πβontoβran π) β ran π βΌ π) |
79 | 72, 77, 78 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β ran π βΌ π) |
80 | | domfi 9139 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β Fin β§ ran π βΌ π) β ran π β Fin) |
81 | 72, 79, 80 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β ran π β Fin) |
82 | 71, 81 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β (ran π β π β§ ran π β Fin)) |
83 | | elin 3927 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (ran
π β (π« π β© Fin) β (ran π β π« π β§ ran π β Fin)) |
84 | | vex 3448 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ π β V |
85 | 84 | elpw2 5303 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (ran
π β π« π β ran π β π) |
86 | 85 | anbi1i 625 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((ran
π β π« π β§ ran π β Fin) β (ran π β π β§ ran π β Fin)) |
87 | 83, 86 | bitr2i 276 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((ran
π β π β§ ran π β Fin) β ran π β (π« π β© Fin)) |
88 | 82, 87 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β ran π β (π« π β© Fin)) |
89 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β π = βͺ π) |
90 | | uniiun 5019 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ βͺ π =
βͺ π‘ β π π‘ |
91 | | simprlr 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β βπ‘ β π π‘ β (πβπ‘)) |
92 | | ss2iun 4973 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(βπ‘ β
π π‘ β (πβπ‘) β βͺ
π‘ β π π‘ β βͺ
π‘ β π (πβπ‘)) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β βͺ π‘ β π π‘ β βͺ
π‘ β π (πβπ‘)) |
94 | 90, 93 | eqsstrid 3993 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β βͺ π
β βͺ π‘ β π (πβπ‘)) |
95 | | fniunfv 7195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π Fn π β βͺ
π‘ β π (πβπ‘) = βͺ ran π) |
96 | 69, 73, 95 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β βͺ π‘ β π (πβπ‘) = βͺ ran π) |
97 | 94, 96 | sseqtrd 3985 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β βͺ π
β βͺ ran π) |
98 | 89, 97 | eqsstrd 3983 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β π β βͺ ran
π) |
99 | | simpll2 1214 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β π β π½) |
100 | 71, 99 | sstrd 3955 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β ran π β π½) |
101 | | uniss 4874 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (ran
π β π½ β βͺ ran
π β βͺ π½) |
102 | 101, 1 | sseqtrrdi 3996 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (ran
π β π½ β βͺ ran
π β π) |
103 | 100, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β βͺ ran π β π) |
104 | 98, 103 | eqssd 3962 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β π = βͺ ran π) |
105 | | unieq 4877 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = ran π β βͺ π = βͺ
ran π) |
106 | 105 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = ran π β (π = βͺ π β π = βͺ ran π)) |
107 | 106 | rspcev 3580 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((ran
π β (π« π β© Fin) β§ π = βͺ
ran π) β βπ β (π« π β© Fin)π = βͺ π) |
108 | 88, 104, 107 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β§ ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β§ π = βͺ π)) β βπ β (π« π β© Fin)π = βͺ π) |
109 | 108 | exp32 422 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β ((π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) |
110 | 109 | exlimdv 1937 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β (βπ(π:πβΆπ β§ βπ‘ β π π‘ β (πβπ‘)) β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) |
111 | 68, 110 | syld 47 |
. . . . . . . . . . . . . . . . . 18
β’ (((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β§ π β Fin) β (π β {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) |
112 | 111 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (π β Fin β (π β {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)))) |
113 | 112 | com23 86 |
. . . . . . . . . . . . . . . 16
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (π β {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β (π β Fin β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)))) |
114 | 113 | impd 412 |
. . . . . . . . . . . . . . 15
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β ((π β {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β§ π β Fin) β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) |
115 | 56, 114 | biimtrid 241 |
. . . . . . . . . . . . . 14
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (π β (π« {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β© Fin) β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) |
116 | 115 | rexlimdv 3147 |
. . . . . . . . . . . . 13
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (βπ β (π« {π¦ β (fiβπ₯) β£ βπ§ β π π¦ β π§} β© Fin)π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)) |
117 | 55, 116 | syld 47 |
. . . . . . . . . . . 12
β’ ((π½ = (topGenβ(fiβπ₯)) β§ π β π½ β§ π = βͺ π) β (βπ β π«
(fiβπ₯)(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β βπ β (π« π β© Fin)π = βͺ π)) |
118 | 117 | 3exp 1120 |
. . . . . . . . . . 11
β’ (π½ = (topGenβ(fiβπ₯)) β (π β π½ β (π = βͺ π β (βπ β π«
(fiβπ₯)(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β βπ β (π« π β© Fin)π = βͺ π)))) |
119 | 118 | com34 91 |
. . . . . . . . . 10
β’ (π½ = (topGenβ(fiβπ₯)) β (π β π½ β (βπ β π« (fiβπ₯)(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)))) |
120 | 119 | com23 86 |
. . . . . . . . 9
β’ (π½ = (topGenβ(fiβπ₯)) β (βπ β π«
(fiβπ₯)(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (π β π½ β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)))) |
121 | 4, 120 | syl7bi 255 |
. . . . . . . 8
β’ (π½ = (topGenβ(fiβπ₯)) β (βπ β π«
(fiβπ₯)(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (π β π« π½ β (π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)))) |
122 | 121 | ralrimdv 3146 |
. . . . . . 7
β’ (π½ = (topGenβ(fiβπ₯)) β (βπ β π«
(fiβπ₯)(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β βπ β π« π½(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) |
123 | | fibas 22343 |
. . . . . . . . 9
β’
(fiβπ₯) β
TopBases |
124 | | tgcl 22335 |
. . . . . . . . 9
β’
((fiβπ₯) β
TopBases β (topGenβ(fiβπ₯)) β Top) |
125 | 123, 124 | ax-mp 5 |
. . . . . . . 8
β’
(topGenβ(fiβπ₯)) β Top |
126 | | eleq1 2822 |
. . . . . . . 8
β’ (π½ = (topGenβ(fiβπ₯)) β (π½ β Top β
(topGenβ(fiβπ₯))
β Top)) |
127 | 125, 126 | mpbiri 258 |
. . . . . . 7
β’ (π½ = (topGenβ(fiβπ₯)) β π½ β Top) |
128 | 122, 127 | jctild 527 |
. . . . . 6
β’ (π½ = (topGenβ(fiβπ₯)) β (βπ β π«
(fiβπ₯)(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β (π½ β Top β§ βπ β π« π½(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)))) |
129 | 1 | iscmp 22755 |
. . . . . 6
β’ (π½ β Comp β (π½ β Top β§ βπ β π« π½(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) |
130 | 128, 129 | syl6ibr 252 |
. . . . 5
β’ (π½ = (topGenβ(fiβπ₯)) β (βπ β π«
(fiβπ₯)(π = βͺ
π β βπ β (π« π β© Fin)π = βͺ π) β π½ β Comp)) |
131 | 3, 130 | syld 47 |
. . . 4
β’ (π½ = (topGenβ(fiβπ₯)) β (βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β π½ β Comp)) |
132 | 131 | imp 408 |
. . 3
β’ ((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)) β π½ β Comp) |
133 | 132 | exlimiv 1934 |
. 2
β’
(βπ₯(π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π)) β π½ β Comp) |
134 | 2, 133 | impbii 208 |
1
β’ (π½ β Comp β βπ₯(π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) |