Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . 5
β’ βͺ (topGenβπ΅) = βͺ
(topGenβπ΅) |
2 | 1 | iscmp 22755 |
. . . 4
β’
((topGenβπ΅)
β Comp β ((topGenβπ΅) β Top β§ βπ¦ β π«
(topGenβπ΅)(βͺ (topGenβπ΅) = βͺ π¦ β βπ§ β (π« π¦ β© Fin)βͺ (topGenβπ΅) = βͺ π§))) |
3 | 2 | simprbi 498 |
. . 3
β’
((topGenβπ΅)
β Comp β βπ¦ β π« (topGenβπ΅)(βͺ
(topGenβπ΅) = βͺ π¦
β βπ§ β
(π« π¦ β©
Fin)βͺ (topGenβπ΅) = βͺ π§)) |
4 | | unitg 22333 |
. . . . . . . 8
β’ (π΅ β TopBases β βͺ (topGenβπ΅) = βͺ π΅) |
5 | | eqtr3 2763 |
. . . . . . . 8
β’ ((βͺ (topGenβπ΅) = βͺ π΅ β§ π = βͺ π΅) β βͺ (topGenβπ΅) = π) |
6 | 4, 5 | sylan 581 |
. . . . . . 7
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β βͺ (topGenβπ΅) = π) |
7 | 6 | eqeq1d 2739 |
. . . . . 6
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β (βͺ (topGenβπ΅) = βͺ π¦ β π = βͺ π¦)) |
8 | 6 | eqeq1d 2739 |
. . . . . . 7
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β (βͺ (topGenβπ΅) = βͺ π§ β π = βͺ π§)) |
9 | 8 | rexbidv 3176 |
. . . . . 6
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β (βπ§ β (π« π¦ β© Fin)βͺ (topGenβπ΅) = βͺ π§ β βπ§ β (π« π¦ β© Fin)π = βͺ π§)) |
10 | 7, 9 | imbi12d 345 |
. . . . 5
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β ((βͺ (topGenβπ΅) = βͺ π¦ β βπ§ β (π« π¦ β© Fin)βͺ (topGenβπ΅) = βͺ π§) β (π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) |
11 | 10 | ralbidv 3175 |
. . . 4
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β (βπ¦ β π«
(topGenβπ΅)(βͺ (topGenβπ΅) = βͺ π¦ β βπ§ β (π« π¦ β© Fin)βͺ (topGenβπ΅) = βͺ π§) β βπ¦ β π«
(topGenβπ΅)(π = βͺ
π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) |
12 | | bastg 22332 |
. . . . . . 7
β’ (π΅ β TopBases β π΅ β (topGenβπ΅)) |
13 | 12 | adantr 482 |
. . . . . 6
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β π΅ β (topGenβπ΅)) |
14 | 13 | sspwd 4578 |
. . . . 5
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β π« π΅ β π«
(topGenβπ΅)) |
15 | | ssralv 4015 |
. . . . 5
β’
(π« π΅ β
π« (topGenβπ΅)
β (βπ¦ β
π« (topGenβπ΅)(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§) β βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) |
16 | 14, 15 | syl 17 |
. . . 4
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β (βπ¦ β π«
(topGenβπ΅)(π = βͺ
π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§) β βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) |
17 | 11, 16 | sylbid 239 |
. . 3
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β (βπ¦ β π«
(topGenβπ΅)(βͺ (topGenβπ΅) = βͺ π¦ β βπ§ β (π« π¦ β© Fin)βͺ (topGenβπ΅) = βͺ π§) β βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) |
18 | 3, 17 | syl5 34 |
. 2
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β
((topGenβπ΅) β
Comp β βπ¦
β π« π΅(π = βͺ
π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) |
19 | | elpwi 4572 |
. . . . 5
β’ (π’ β π«
(topGenβπ΅) β
π’ β
(topGenβπ΅)) |
20 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β π = βͺ π’) |
21 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β π’ β (topGenβπ΅)) |
22 | 21 | sselda 3949 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β§ π‘ β π’) β π‘ β (topGenβπ΅)) |
23 | 22 | adantrr 716 |
. . . . . . . . . . . . . . . 16
β’ ((((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β§ (π‘ β π’ β§ π¦ β π‘)) β π‘ β (topGenβπ΅)) |
24 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ ((((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β§ (π‘ β π’ β§ π¦ β π‘)) β π¦ β π‘) |
25 | | tg2 22331 |
. . . . . . . . . . . . . . . 16
β’ ((π‘ β (topGenβπ΅) β§ π¦ β π‘) β βπ€ β π΅ (π¦ β π€ β§ π€ β π‘)) |
26 | 23, 24, 25 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β§ (π‘ β π’ β§ π¦ β π‘)) β βπ€ β π΅ (π¦ β π€ β§ π€ β π‘)) |
27 | 26 | expr 458 |
. . . . . . . . . . . . . 14
β’ ((((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β§ π‘ β π’) β (π¦ β π‘ β βπ€ β π΅ (π¦ β π€ β§ π€ β π‘))) |
28 | 27 | reximdva 3166 |
. . . . . . . . . . . . 13
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β (βπ‘ β π’ π¦ β π‘ β βπ‘ β π’ βπ€ β π΅ (π¦ β π€ β§ π€ β π‘))) |
29 | | eluni2 4874 |
. . . . . . . . . . . . 13
β’ (π¦ β βͺ π’
β βπ‘ β
π’ π¦ β π‘) |
30 | | elunirab 4886 |
. . . . . . . . . . . . . 14
β’ (π¦ β βͺ {π€
β π΅ β£
βπ‘ β π’ π€ β π‘} β βπ€ β π΅ (π¦ β π€ β§ βπ‘ β π’ π€ β π‘)) |
31 | | r19.42v 3188 |
. . . . . . . . . . . . . . 15
β’
(βπ‘ β
π’ (π¦ β π€ β§ π€ β π‘) β (π¦ β π€ β§ βπ‘ β π’ π€ β π‘)) |
32 | 31 | rexbii 3098 |
. . . . . . . . . . . . . 14
β’
(βπ€ β
π΅ βπ‘ β π’ (π¦ β π€ β§ π€ β π‘) β βπ€ β π΅ (π¦ β π€ β§ βπ‘ β π’ π€ β π‘)) |
33 | | rexcom 3276 |
. . . . . . . . . . . . . 14
β’
(βπ€ β
π΅ βπ‘ β π’ (π¦ β π€ β§ π€ β π‘) β βπ‘ β π’ βπ€ β π΅ (π¦ β π€ β§ π€ β π‘)) |
34 | 30, 32, 33 | 3bitr2i 299 |
. . . . . . . . . . . . 13
β’ (π¦ β βͺ {π€
β π΅ β£
βπ‘ β π’ π€ β π‘} β βπ‘ β π’ βπ€ β π΅ (π¦ β π€ β§ π€ β π‘)) |
35 | 28, 29, 34 | 3imtr4g 296 |
. . . . . . . . . . . 12
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β (π¦ β βͺ π’ β π¦ β βͺ {π€ β π΅ β£ βπ‘ β π’ π€ β π‘})) |
36 | 35 | ssrdv 3955 |
. . . . . . . . . . 11
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β βͺ π’
β βͺ {π€ β π΅ β£ βπ‘ β π’ π€ β π‘}) |
37 | 20, 36 | eqsstrd 3987 |
. . . . . . . . . 10
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β π β βͺ {π€ β π΅ β£ βπ‘ β π’ π€ β π‘}) |
38 | | ssrab2 4042 |
. . . . . . . . . . . 12
β’ {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β π΅ |
39 | 38 | unissi 4879 |
. . . . . . . . . . 11
β’ βͺ {π€
β π΅ β£
βπ‘ β π’ π€ β π‘} β βͺ π΅ |
40 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β π = βͺ π΅) |
41 | 39, 40 | sseqtrrid 4002 |
. . . . . . . . . 10
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β βͺ {π€
β π΅ β£
βπ‘ β π’ π€ β π‘} β π) |
42 | 37, 41 | eqssd 3966 |
. . . . . . . . 9
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β π = βͺ {π€ β π΅ β£ βπ‘ β π’ π€ β π‘}) |
43 | | elpw2g 5306 |
. . . . . . . . . . . 12
β’ (π΅ β TopBases β ({π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β π« π΅ β {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β π΅)) |
44 | 43 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β ({π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β π« π΅ β {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β π΅)) |
45 | 38, 44 | mpbiri 258 |
. . . . . . . . . 10
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β π« π΅) |
46 | | unieq 4881 |
. . . . . . . . . . . . 13
β’ (π¦ = {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β βͺ π¦ = βͺ
{π€ β π΅ β£ βπ‘ β π’ π€ β π‘}) |
47 | 46 | eqeq2d 2748 |
. . . . . . . . . . . 12
β’ (π¦ = {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β (π = βͺ π¦ β π = βͺ {π€ β π΅ β£ βπ‘ β π’ π€ β π‘})) |
48 | | pweq 4579 |
. . . . . . . . . . . . . 14
β’ (π¦ = {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β π« π¦ = π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘}) |
49 | 48 | ineq1d 4176 |
. . . . . . . . . . . . 13
β’ (π¦ = {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β (π« π¦ β© Fin) = (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin)) |
50 | 49 | rexeqdv 3317 |
. . . . . . . . . . . 12
β’ (π¦ = {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β (βπ§ β (π« π¦ β© Fin)π = βͺ π§ β βπ§ β (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin)π = βͺ π§)) |
51 | 47, 50 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π¦ = {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β ((π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§) β (π = βͺ {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β βπ§ β (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin)π = βͺ π§))) |
52 | 51 | rspcv 3580 |
. . . . . . . . . 10
β’ ({π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β π« π΅ β (βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§) β (π = βͺ {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β βπ§ β (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin)π = βͺ π§))) |
53 | 45, 52 | syl 17 |
. . . . . . . . 9
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β (βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§) β (π = βͺ {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β βπ§ β (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin)π = βͺ π§))) |
54 | 42, 53 | mpid 44 |
. . . . . . . 8
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β (βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§) β βπ§ β (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin)π = βͺ π§)) |
55 | | elfpw 9305 |
. . . . . . . . . . . . 13
β’ (π§ β (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β (π§ β {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β§ π§ β Fin)) |
56 | 55 | simprbi 498 |
. . . . . . . . . . . 12
β’ (π§ β (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β π§ β Fin) |
57 | 56 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β§ (π§ β (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β π§ β Fin) |
58 | 55 | simplbi 499 |
. . . . . . . . . . . . 13
β’ (π§ β (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β π§ β {π€ β π΅ β£ βπ‘ β π’ π€ β π‘}) |
59 | 58 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ ((((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β§ (π§ β (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β π§ β {π€ β π΅ β£ βπ‘ β π’ π€ β π‘}) |
60 | | ssrab 4035 |
. . . . . . . . . . . . 13
β’ (π§ β {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β (π§ β π΅ β§ βπ€ β π§ βπ‘ β π’ π€ β π‘)) |
61 | 60 | simprbi 498 |
. . . . . . . . . . . 12
β’ (π§ β {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β βπ€ β π§ βπ‘ β π’ π€ β π‘) |
62 | 59, 61 | syl 17 |
. . . . . . . . . . 11
β’ ((((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β§ (π§ β (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β βπ€ β π§ βπ‘ β π’ π€ β π‘) |
63 | | sseq2 3975 |
. . . . . . . . . . . 12
β’ (π‘ = (πβπ€) β (π€ β π‘ β π€ β (πβπ€))) |
64 | 63 | ac6sfi 9238 |
. . . . . . . . . . 11
β’ ((π§ β Fin β§ βπ€ β π§ βπ‘ β π’ π€ β π‘) β βπ(π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) |
65 | 57, 62, 64 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β§ (π§ β (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β βπ(π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) |
66 | | frn 6680 |
. . . . . . . . . . . . 13
β’ (π:π§βΆπ’ β ran π β π’) |
67 | 66 | ad2antrl 727 |
. . . . . . . . . . . 12
β’
(((((π΅ β
TopBases β§ π = βͺ π΅)
β§ (π’ β
(topGenβπ΅) β§
π = βͺ π’))
β§ (π§ β (π«
{π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β§ (π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) β ran π β π’) |
68 | | ffn 6673 |
. . . . . . . . . . . . . . 15
β’ (π:π§βΆπ’ β π Fn π§) |
69 | | dffn4 6767 |
. . . . . . . . . . . . . . 15
β’ (π Fn π§ β π:π§βontoβran π) |
70 | 68, 69 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (π:π§βΆπ’ β π:π§βontoβran π) |
71 | 70 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€)) β π:π§βontoβran π) |
72 | | fofi 9289 |
. . . . . . . . . . . . 13
β’ ((π§ β Fin β§ π:π§βontoβran π) β ran π β Fin) |
73 | 57, 71, 72 | syl2an 597 |
. . . . . . . . . . . 12
β’
(((((π΅ β
TopBases β§ π = βͺ π΅)
β§ (π’ β
(topGenβπ΅) β§
π = βͺ π’))
β§ (π§ β (π«
{π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β§ (π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) β ran π β Fin) |
74 | | elfpw 9305 |
. . . . . . . . . . . 12
β’ (ran
π β (π« π’ β© Fin) β (ran π β π’ β§ ran π β Fin)) |
75 | 67, 73, 74 | sylanbrc 584 |
. . . . . . . . . . 11
β’
(((((π΅ β
TopBases β§ π = βͺ π΅)
β§ (π’ β
(topGenβπ΅) β§
π = βͺ π’))
β§ (π§ β (π«
{π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β§ (π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) β ran π β (π« π’ β© Fin)) |
76 | | simplrr 777 |
. . . . . . . . . . . . 13
β’
(((((π΅ β
TopBases β§ π = βͺ π΅)
β§ (π’ β
(topGenβπ΅) β§
π = βͺ π’))
β§ (π§ β (π«
{π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β§ (π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) β π = βͺ π§) |
77 | | uniiun 5023 |
. . . . . . . . . . . . . . . 16
β’ βͺ π§ =
βͺ π€ β π§ π€ |
78 | | ss2iun 4977 |
. . . . . . . . . . . . . . . 16
β’
(βπ€ β
π§ π€ β (πβπ€) β βͺ
π€ β π§ π€ β βͺ
π€ β π§ (πβπ€)) |
79 | 77, 78 | eqsstrid 3997 |
. . . . . . . . . . . . . . 15
β’
(βπ€ β
π§ π€ β (πβπ€) β βͺ π§ β βͺ π€ β π§ (πβπ€)) |
80 | 79 | ad2antll 728 |
. . . . . . . . . . . . . 14
β’
(((((π΅ β
TopBases β§ π = βͺ π΅)
β§ (π’ β
(topGenβπ΅) β§
π = βͺ π’))
β§ (π§ β (π«
{π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β§ (π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) β βͺ π§ β βͺ π€ β π§ (πβπ€)) |
81 | | fniunfv 7199 |
. . . . . . . . . . . . . . . 16
β’ (π Fn π§ β βͺ
π€ β π§ (πβπ€) = βͺ ran π) |
82 | 68, 81 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π:π§βΆπ’ β βͺ
π€ β π§ (πβπ€) = βͺ ran π) |
83 | 82 | ad2antrl 727 |
. . . . . . . . . . . . . 14
β’
(((((π΅ β
TopBases β§ π = βͺ π΅)
β§ (π’ β
(topGenβπ΅) β§
π = βͺ π’))
β§ (π§ β (π«
{π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β§ (π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) β βͺ π€ β π§ (πβπ€) = βͺ ran π) |
84 | 80, 83 | sseqtrd 3989 |
. . . . . . . . . . . . 13
β’
(((((π΅ β
TopBases β§ π = βͺ π΅)
β§ (π’ β
(topGenβπ΅) β§
π = βͺ π’))
β§ (π§ β (π«
{π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β§ (π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) β βͺ π§ β βͺ ran π) |
85 | 76, 84 | eqsstrd 3987 |
. . . . . . . . . . . 12
β’
(((((π΅ β
TopBases β§ π = βͺ π΅)
β§ (π’ β
(topGenβπ΅) β§
π = βͺ π’))
β§ (π§ β (π«
{π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β§ (π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) β π β βͺ ran
π) |
86 | 67 | unissd 4880 |
. . . . . . . . . . . . 13
β’
(((((π΅ β
TopBases β§ π = βͺ π΅)
β§ (π’ β
(topGenβπ΅) β§
π = βͺ π’))
β§ (π§ β (π«
{π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β§ (π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) β βͺ ran
π β βͺ π’) |
87 | 20 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’
(((((π΅ β
TopBases β§ π = βͺ π΅)
β§ (π’ β
(topGenβπ΅) β§
π = βͺ π’))
β§ (π§ β (π«
{π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β§ (π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) β π = βͺ π’) |
88 | 86, 87 | sseqtrrd 3990 |
. . . . . . . . . . . 12
β’
(((((π΅ β
TopBases β§ π = βͺ π΅)
β§ (π’ β
(topGenβπ΅) β§
π = βͺ π’))
β§ (π§ β (π«
{π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β§ (π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) β βͺ ran
π β π) |
89 | 85, 88 | eqssd 3966 |
. . . . . . . . . . 11
β’
(((((π΅ β
TopBases β§ π = βͺ π΅)
β§ (π’ β
(topGenβπ΅) β§
π = βͺ π’))
β§ (π§ β (π«
{π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β§ (π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) β π = βͺ ran π) |
90 | | unieq 4881 |
. . . . . . . . . . . 12
β’ (π£ = ran π β βͺ π£ = βͺ
ran π) |
91 | 90 | rspceeqv 3600 |
. . . . . . . . . . 11
β’ ((ran
π β (π« π’ β© Fin) β§ π = βͺ
ran π) β βπ£ β (π« π’ β© Fin)π = βͺ π£) |
92 | 75, 89, 91 | syl2anc 585 |
. . . . . . . . . 10
β’
(((((π΅ β
TopBases β§ π = βͺ π΅)
β§ (π’ β
(topGenβπ΅) β§
π = βͺ π’))
β§ (π§ β (π«
{π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β§ (π:π§βΆπ’ β§ βπ€ β π§ π€ β (πβπ€))) β βπ£ β (π« π’ β© Fin)π = βͺ π£) |
93 | 65, 92 | exlimddv 1939 |
. . . . . . . . 9
β’ ((((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β§ (π§ β (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin) β§ π = βͺ π§)) β βπ£ β (π« π’ β© Fin)π = βͺ π£) |
94 | 93 | rexlimdvaa 3154 |
. . . . . . . 8
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β (βπ§ β (π« {π€ β π΅ β£ βπ‘ β π’ π€ β π‘} β© Fin)π = βͺ π§ β βπ£ β (π« π’ β© Fin)π = βͺ π£)) |
95 | 54, 94 | syld 47 |
. . . . . . 7
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ (π’ β (topGenβπ΅) β§ π = βͺ π’)) β (βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§) β βπ£ β (π« π’ β© Fin)π = βͺ π£)) |
96 | 95 | expr 458 |
. . . . . 6
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ π’ β (topGenβπ΅)) β (π = βͺ π’ β (βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§) β βπ£ β (π« π’ β© Fin)π = βͺ π£))) |
97 | 96 | com23 86 |
. . . . 5
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ π’ β (topGenβπ΅)) β (βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§) β (π = βͺ π’ β βπ£ β (π« π’ β© Fin)π = βͺ π£))) |
98 | 19, 97 | sylan2 594 |
. . . 4
β’ (((π΅ β TopBases β§ π = βͺ
π΅) β§ π’ β π« (topGenβπ΅)) β (βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§) β (π = βͺ π’ β βπ£ β (π« π’ β© Fin)π = βͺ π£))) |
99 | 98 | ralrimdva 3152 |
. . 3
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β (βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§) β βπ’ β π«
(topGenβπ΅)(π = βͺ
π’ β βπ£ β (π« π’ β© Fin)π = βͺ π£))) |
100 | | tgcl 22335 |
. . . . . 6
β’ (π΅ β TopBases β
(topGenβπ΅) β
Top) |
101 | 100 | adantr 482 |
. . . . 5
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β
(topGenβπ΅) β
Top) |
102 | 1 | iscmp 22755 |
. . . . . 6
β’
((topGenβπ΅)
β Comp β ((topGenβπ΅) β Top β§ βπ’ β π«
(topGenβπ΅)(βͺ (topGenβπ΅) = βͺ π’ β βπ£ β (π« π’ β© Fin)βͺ (topGenβπ΅) = βͺ π£))) |
103 | 102 | baib 537 |
. . . . 5
β’
((topGenβπ΅)
β Top β ((topGenβπ΅) β Comp β βπ’ β π«
(topGenβπ΅)(βͺ (topGenβπ΅) = βͺ π’ β βπ£ β (π« π’ β© Fin)βͺ (topGenβπ΅) = βͺ π£))) |
104 | 101, 103 | syl 17 |
. . . 4
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β
((topGenβπ΅) β
Comp β βπ’
β π« (topGenβπ΅)(βͺ
(topGenβπ΅) = βͺ π’
β βπ£ β
(π« π’ β©
Fin)βͺ (topGenβπ΅) = βͺ π£))) |
105 | 6 | eqeq1d 2739 |
. . . . . 6
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β (βͺ (topGenβπ΅) = βͺ π’ β π = βͺ π’)) |
106 | 6 | eqeq1d 2739 |
. . . . . . 7
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β (βͺ (topGenβπ΅) = βͺ π£ β π = βͺ π£)) |
107 | 106 | rexbidv 3176 |
. . . . . 6
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β (βπ£ β (π« π’ β© Fin)βͺ (topGenβπ΅) = βͺ π£ β βπ£ β (π« π’ β© Fin)π = βͺ π£)) |
108 | 105, 107 | imbi12d 345 |
. . . . 5
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β ((βͺ (topGenβπ΅) = βͺ π’ β βπ£ β (π« π’ β© Fin)βͺ (topGenβπ΅) = βͺ π£) β (π = βͺ π’ β βπ£ β (π« π’ β© Fin)π = βͺ π£))) |
109 | 108 | ralbidv 3175 |
. . . 4
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β (βπ’ β π«
(topGenβπ΅)(βͺ (topGenβπ΅) = βͺ π’ β βπ£ β (π« π’ β© Fin)βͺ (topGenβπ΅) = βͺ π£) β βπ’ β π«
(topGenβπ΅)(π = βͺ
π’ β βπ£ β (π« π’ β© Fin)π = βͺ π£))) |
110 | 104, 109 | bitrd 279 |
. . 3
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β
((topGenβπ΅) β
Comp β βπ’
β π« (topGenβπ΅)(π = βͺ π’ β βπ£ β (π« π’ β© Fin)π = βͺ π£))) |
111 | 99, 110 | sylibrd 259 |
. 2
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β (βπ¦ β π« π΅(π = βͺ π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§) β (topGenβπ΅) β Comp)) |
112 | 18, 111 | impbid 211 |
1
β’ ((π΅ β TopBases β§ π = βͺ
π΅) β
((topGenβπ΅) β
Comp β βπ¦
β π« π΅(π = βͺ
π¦ β βπ§ β (π« π¦ β© Fin)π = βͺ π§))) |