Step | Hyp | Ref
| Expression |
1 | | 2ndctop 22950 |
. 2
β’ (π½ β 2ndΟ
β π½ β
Top) |
2 | | is2ndc 22949 |
. . . 4
β’ (π½ β 2ndΟ
β βπ β
TopBases (π βΌ Ο
β§ (topGenβπ) =
π½)) |
3 | | ssrab2 4077 |
. . . . . . . . . . 11
β’ {π β π β£ π₯ β π} β π |
4 | | bastg 22468 |
. . . . . . . . . . . 12
β’ (π β TopBases β π β (topGenβπ)) |
5 | 4 | 3ad2ant1 1133 |
. . . . . . . . . . 11
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β π β (topGenβπ)) |
6 | 3, 5 | sstrid 3993 |
. . . . . . . . . 10
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β {π β π β£ π₯ β π} β (topGenβπ)) |
7 | | fvex 6904 |
. . . . . . . . . . 11
β’
(topGenβπ)
β V |
8 | 7 | elpw2 5345 |
. . . . . . . . . 10
β’ ({π β π β£ π₯ β π} β π« (topGenβπ) β {π β π β£ π₯ β π} β (topGenβπ)) |
9 | 6, 8 | sylibr 233 |
. . . . . . . . 9
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β {π β π β£ π₯ β π} β π« (topGenβπ)) |
10 | | vex 3478 |
. . . . . . . . . . 11
β’ π β V |
11 | | ssdomg 8995 |
. . . . . . . . . . 11
β’ (π β V β ({π β π β£ π₯ β π} β π β {π β π β£ π₯ β π} βΌ π)) |
12 | 10, 3, 11 | mp2 9 |
. . . . . . . . . 10
β’ {π β π β£ π₯ β π} βΌ π |
13 | | simp2 1137 |
. . . . . . . . . 10
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β π βΌ Ο) |
14 | | domtr 9002 |
. . . . . . . . . 10
β’ (({π β π β£ π₯ β π} βΌ π β§ π βΌ Ο) β {π β π β£ π₯ β π} βΌ Ο) |
15 | 12, 13, 14 | sylancr 587 |
. . . . . . . . 9
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β {π β π β£ π₯ β π} βΌ Ο) |
16 | | eltg2b 22461 |
. . . . . . . . . . . 12
β’ (π β TopBases β (π β (topGenβπ) β βπ¦ β π βπ‘ β π (π¦ β π‘ β§ π‘ β π))) |
17 | 16 | 3ad2ant1 1133 |
. . . . . . . . . . 11
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β (π β (topGenβπ) β βπ¦ β π βπ‘ β π (π¦ β π‘ β§ π‘ β π))) |
18 | | elequ1 2113 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π₯ β (π¦ β π‘ β π₯ β π‘)) |
19 | 18 | anbi1d 630 |
. . . . . . . . . . . . . 14
β’ (π¦ = π₯ β ((π¦ β π‘ β§ π‘ β π) β (π₯ β π‘ β§ π‘ β π))) |
20 | 19 | rexbidv 3178 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β (βπ‘ β π (π¦ β π‘ β§ π‘ β π) β βπ‘ β π (π₯ β π‘ β§ π‘ β π))) |
21 | 20 | rspccv 3609 |
. . . . . . . . . . . 12
β’
(βπ¦ β
π βπ‘ β π (π¦ β π‘ β§ π‘ β π) β (π₯ β π β βπ‘ β π (π₯ β π‘ β§ π‘ β π))) |
22 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ ((π‘ β π β§ π₯ β π‘) β (π‘ β π β§ π₯ β π‘)) |
23 | 22 | adantrr 715 |
. . . . . . . . . . . . . . 15
β’ ((π‘ β π β§ (π₯ β π‘ β§ π‘ β π)) β (π‘ β π β§ π₯ β π‘)) |
24 | | elequ2 2121 |
. . . . . . . . . . . . . . . 16
β’ (π = π‘ β (π₯ β π β π₯ β π‘)) |
25 | 24 | elrab 3683 |
. . . . . . . . . . . . . . 15
β’ (π‘ β {π β π β£ π₯ β π} β (π‘ β π β§ π₯ β π‘)) |
26 | 23, 25 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ ((π‘ β π β§ (π₯ β π‘ β§ π‘ β π)) β π‘ β {π β π β£ π₯ β π}) |
27 | | simprr 771 |
. . . . . . . . . . . . . 14
β’ (((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β§ (π‘ β π β§ (π₯ β π‘ β§ π‘ β π))) β (π₯ β π‘ β§ π‘ β π)) |
28 | | elequ2 2121 |
. . . . . . . . . . . . . . . 16
β’ (π = π‘ β (π₯ β π β π₯ β π‘)) |
29 | | sseq1 4007 |
. . . . . . . . . . . . . . . 16
β’ (π = π‘ β (π β π β π‘ β π)) |
30 | 28, 29 | anbi12d 631 |
. . . . . . . . . . . . . . 15
β’ (π = π‘ β ((π₯ β π β§ π β π) β (π₯ β π‘ β§ π‘ β π))) |
31 | 30 | rspcev 3612 |
. . . . . . . . . . . . . 14
β’ ((π‘ β {π β π β£ π₯ β π} β§ (π₯ β π‘ β§ π‘ β π)) β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π)) |
32 | 26, 27, 31 | syl2an2 684 |
. . . . . . . . . . . . 13
β’ (((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β§ (π‘ β π β§ (π₯ β π‘ β§ π‘ β π))) β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π)) |
33 | 32 | rexlimdvaa 3156 |
. . . . . . . . . . . 12
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β (βπ‘ β π (π₯ β π‘ β§ π‘ β π) β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π))) |
34 | 21, 33 | syl9r 78 |
. . . . . . . . . . 11
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β (βπ¦ β π βπ‘ β π (π¦ β π‘ β§ π‘ β π) β (π₯ β π β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π)))) |
35 | 17, 34 | sylbid 239 |
. . . . . . . . . 10
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β (π β (topGenβπ) β (π₯ β π β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π)))) |
36 | 35 | ralrimiv 3145 |
. . . . . . . . 9
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β βπ β (topGenβπ)(π₯ β π β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π))) |
37 | | breq1 5151 |
. . . . . . . . . . 11
β’ (π = {π β π β£ π₯ β π} β (π βΌ Ο β {π β π β£ π₯ β π} βΌ Ο)) |
38 | | rexeq 3321 |
. . . . . . . . . . . . 13
β’ (π = {π β π β£ π₯ β π} β (βπ β π (π₯ β π β§ π β π) β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π))) |
39 | 38 | imbi2d 340 |
. . . . . . . . . . . 12
β’ (π = {π β π β£ π₯ β π} β ((π₯ β π β βπ β π (π₯ β π β§ π β π)) β (π₯ β π β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π)))) |
40 | 39 | ralbidv 3177 |
. . . . . . . . . . 11
β’ (π = {π β π β£ π₯ β π} β (βπ β (topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π)) β βπ β (topGenβπ)(π₯ β π β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π)))) |
41 | 37, 40 | anbi12d 631 |
. . . . . . . . . 10
β’ (π = {π β π β£ π₯ β π} β ((π βΌ Ο β§ βπ β (topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π))) β ({π β π β£ π₯ β π} βΌ Ο β§ βπ β (topGenβπ)(π₯ β π β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π))))) |
42 | 41 | rspcev 3612 |
. . . . . . . . 9
β’ (({π β π β£ π₯ β π} β π« (topGenβπ) β§ ({π β π β£ π₯ β π} βΌ Ο β§ βπ β (topGenβπ)(π₯ β π β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π)))) β βπ β π« (topGenβπ)(π βΌ Ο β§ βπ β (topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π)))) |
43 | 9, 15, 36, 42 | syl12anc 835 |
. . . . . . . 8
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β βπ β π« (topGenβπ)(π βΌ Ο β§ βπ β (topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π)))) |
44 | 43 | 3expia 1121 |
. . . . . . 7
β’ ((π β TopBases β§ π βΌ Ο) β (π₯ β βͺ (topGenβπ) β βπ β π« (topGenβπ)(π βΌ Ο β§ βπ β (topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π))))) |
45 | | unieq 4919 |
. . . . . . . . 9
β’
((topGenβπ) =
π½ β βͺ (topGenβπ) = βͺ π½) |
46 | 45 | eleq2d 2819 |
. . . . . . . 8
β’
((topGenβπ) =
π½ β (π₯ β βͺ (topGenβπ) β π₯ β βͺ π½)) |
47 | | pweq 4616 |
. . . . . . . . 9
β’
((topGenβπ) =
π½ β π«
(topGenβπ) =
π« π½) |
48 | | raleq 3322 |
. . . . . . . . . 10
β’
((topGenβπ) =
π½ β (βπ β (topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π)) β βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π)))) |
49 | 48 | anbi2d 629 |
. . . . . . . . 9
β’
((topGenβπ) =
π½ β ((π βΌ Ο β§
βπ β
(topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π))) β (π βΌ Ο β§ βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π))))) |
50 | 47, 49 | rexeqbidv 3343 |
. . . . . . . 8
β’
((topGenβπ) =
π½ β (βπ β π«
(topGenβπ)(π βΌ Ο β§
βπ β
(topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π))) β βπ β π« π½(π βΌ Ο β§ βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π))))) |
51 | 46, 50 | imbi12d 344 |
. . . . . . 7
β’
((topGenβπ) =
π½ β ((π₯ β βͺ (topGenβπ) β βπ β π« (topGenβπ)(π βΌ Ο β§ βπ β (topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π)))) β (π₯ β βͺ π½ β βπ β π« π½(π βΌ Ο β§ βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π)))))) |
52 | 44, 51 | syl5ibcom 244 |
. . . . . 6
β’ ((π β TopBases β§ π βΌ Ο) β
((topGenβπ) = π½ β (π₯ β βͺ π½ β βπ β π« π½(π βΌ Ο β§ βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π)))))) |
53 | 52 | expimpd 454 |
. . . . 5
β’ (π β TopBases β ((π βΌ Ο β§
(topGenβπ) = π½) β (π₯ β βͺ π½ β βπ β π« π½(π βΌ Ο β§ βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π)))))) |
54 | 53 | rexlimiv 3148 |
. . . 4
β’
(βπ β
TopBases (π βΌ Ο
β§ (topGenβπ) =
π½) β (π₯ β βͺ π½
β βπ β
π« π½(π βΌ Ο β§
βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π))))) |
55 | 2, 54 | sylbi 216 |
. . 3
β’ (π½ β 2ndΟ
β (π₯ β βͺ π½
β βπ β
π« π½(π βΌ Ο β§
βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π))))) |
56 | 55 | ralrimiv 3145 |
. 2
β’ (π½ β 2ndΟ
β βπ₯ β
βͺ π½βπ β π« π½(π βΌ Ο β§ βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π)))) |
57 | | eqid 2732 |
. . 3
β’ βͺ π½ =
βͺ π½ |
58 | 57 | is1stc2 22945 |
. 2
β’ (π½ β 1stΟ
β (π½ β Top β§
βπ₯ β βͺ π½βπ β π« π½(π βΌ Ο β§ βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π))))) |
59 | 1, 56, 58 | sylanbrc 583 |
1
β’ (π½ β 2ndΟ
β π½ β
1stΟ) |