Step | Hyp | Ref
| Expression |
1 | | 2ndctop 22821 |
. 2
β’ (π½ β 2ndΟ
β π½ β
Top) |
2 | | is2ndc 22820 |
. . . 4
β’ (π½ β 2ndΟ
β βπ β
TopBases (π βΌ Ο
β§ (topGenβπ) =
π½)) |
3 | | ssrab2 4041 |
. . . . . . . . . . 11
β’ {π β π β£ π₯ β π} β π |
4 | | bastg 22339 |
. . . . . . . . . . . 12
β’ (π β TopBases β π β (topGenβπ)) |
5 | 4 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β π β (topGenβπ)) |
6 | 3, 5 | sstrid 3959 |
. . . . . . . . . 10
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β {π β π β£ π₯ β π} β (topGenβπ)) |
7 | | fvex 6859 |
. . . . . . . . . . 11
β’
(topGenβπ)
β V |
8 | 7 | elpw2 5306 |
. . . . . . . . . 10
β’ ({π β π β£ π₯ β π} β π« (topGenβπ) β {π β π β£ π₯ β π} β (topGenβπ)) |
9 | 6, 8 | sylibr 233 |
. . . . . . . . 9
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β {π β π β£ π₯ β π} β π« (topGenβπ)) |
10 | | vex 3451 |
. . . . . . . . . . 11
β’ π β V |
11 | | ssdomg 8946 |
. . . . . . . . . . 11
β’ (π β V β ({π β π β£ π₯ β π} β π β {π β π β£ π₯ β π} βΌ π)) |
12 | 10, 3, 11 | mp2 9 |
. . . . . . . . . 10
β’ {π β π β£ π₯ β π} βΌ π |
13 | | simp2 1138 |
. . . . . . . . . 10
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β π βΌ Ο) |
14 | | domtr 8953 |
. . . . . . . . . 10
β’ (({π β π β£ π₯ β π} βΌ π β§ π βΌ Ο) β {π β π β£ π₯ β π} βΌ Ο) |
15 | 12, 13, 14 | sylancr 588 |
. . . . . . . . 9
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β {π β π β£ π₯ β π} βΌ Ο) |
16 | | eltg2b 22332 |
. . . . . . . . . . . 12
β’ (π β TopBases β (π β (topGenβπ) β βπ¦ β π βπ‘ β π (π¦ β π‘ β§ π‘ β π))) |
17 | 16 | 3ad2ant1 1134 |
. . . . . . . . . . 11
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β (π β (topGenβπ) β βπ¦ β π βπ‘ β π (π¦ β π‘ β§ π‘ β π))) |
18 | | elequ1 2114 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π₯ β (π¦ β π‘ β π₯ β π‘)) |
19 | 18 | anbi1d 631 |
. . . . . . . . . . . . . 14
β’ (π¦ = π₯ β ((π¦ β π‘ β§ π‘ β π) β (π₯ β π‘ β§ π‘ β π))) |
20 | 19 | rexbidv 3172 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β (βπ‘ β π (π¦ β π‘ β§ π‘ β π) β βπ‘ β π (π₯ β π‘ β§ π‘ β π))) |
21 | 20 | rspccv 3580 |
. . . . . . . . . . . 12
β’
(βπ¦ β
π βπ‘ β π (π¦ β π‘ β§ π‘ β π) β (π₯ β π β βπ‘ β π (π₯ β π‘ β§ π‘ β π))) |
22 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ ((π‘ β π β§ π₯ β π‘) β (π‘ β π β§ π₯ β π‘)) |
23 | 22 | adantrr 716 |
. . . . . . . . . . . . . . 15
β’ ((π‘ β π β§ (π₯ β π‘ β§ π‘ β π)) β (π‘ β π β§ π₯ β π‘)) |
24 | | elequ2 2122 |
. . . . . . . . . . . . . . . 16
β’ (π = π‘ β (π₯ β π β π₯ β π‘)) |
25 | 24 | elrab 3649 |
. . . . . . . . . . . . . . 15
β’ (π‘ β {π β π β£ π₯ β π} β (π‘ β π β§ π₯ β π‘)) |
26 | 23, 25 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ ((π‘ β π β§ (π₯ β π‘ β§ π‘ β π)) β π‘ β {π β π β£ π₯ β π}) |
27 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ (((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β§ (π‘ β π β§ (π₯ β π‘ β§ π‘ β π))) β (π₯ β π‘ β§ π‘ β π)) |
28 | | elequ2 2122 |
. . . . . . . . . . . . . . . 16
β’ (π = π‘ β (π₯ β π β π₯ β π‘)) |
29 | | sseq1 3973 |
. . . . . . . . . . . . . . . 16
β’ (π = π‘ β (π β π β π‘ β π)) |
30 | 28, 29 | anbi12d 632 |
. . . . . . . . . . . . . . 15
β’ (π = π‘ β ((π₯ β π β§ π β π) β (π₯ β π‘ β§ π‘ β π))) |
31 | 30 | rspcev 3583 |
. . . . . . . . . . . . . 14
β’ ((π‘ β {π β π β£ π₯ β π} β§ (π₯ β π‘ β§ π‘ β π)) β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π)) |
32 | 26, 27, 31 | syl2an2 685 |
. . . . . . . . . . . . 13
β’ (((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β§ (π‘ β π β§ (π₯ β π‘ β§ π‘ β π))) β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π)) |
33 | 32 | rexlimdvaa 3150 |
. . . . . . . . . . . 12
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β (βπ‘ β π (π₯ β π‘ β§ π‘ β π) β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π))) |
34 | 21, 33 | syl9r 78 |
. . . . . . . . . . 11
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β (βπ¦ β π βπ‘ β π (π¦ β π‘ β§ π‘ β π) β (π₯ β π β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π)))) |
35 | 17, 34 | sylbid 239 |
. . . . . . . . . 10
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β (π β (topGenβπ) β (π₯ β π β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π)))) |
36 | 35 | ralrimiv 3139 |
. . . . . . . . 9
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β βπ β (topGenβπ)(π₯ β π β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π))) |
37 | | breq1 5112 |
. . . . . . . . . . 11
β’ (π = {π β π β£ π₯ β π} β (π βΌ Ο β {π β π β£ π₯ β π} βΌ Ο)) |
38 | | rexeq 3309 |
. . . . . . . . . . . . 13
β’ (π = {π β π β£ π₯ β π} β (βπ β π (π₯ β π β§ π β π) β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π))) |
39 | 38 | imbi2d 341 |
. . . . . . . . . . . 12
β’ (π = {π β π β£ π₯ β π} β ((π₯ β π β βπ β π (π₯ β π β§ π β π)) β (π₯ β π β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π)))) |
40 | 39 | ralbidv 3171 |
. . . . . . . . . . 11
β’ (π = {π β π β£ π₯ β π} β (βπ β (topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π)) β βπ β (topGenβπ)(π₯ β π β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π)))) |
41 | 37, 40 | anbi12d 632 |
. . . . . . . . . 10
β’ (π = {π β π β£ π₯ β π} β ((π βΌ Ο β§ βπ β (topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π))) β ({π β π β£ π₯ β π} βΌ Ο β§ βπ β (topGenβπ)(π₯ β π β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π))))) |
42 | 41 | rspcev 3583 |
. . . . . . . . 9
β’ (({π β π β£ π₯ β π} β π« (topGenβπ) β§ ({π β π β£ π₯ β π} βΌ Ο β§ βπ β (topGenβπ)(π₯ β π β βπ β {π β π β£ π₯ β π} (π₯ β π β§ π β π)))) β βπ β π« (topGenβπ)(π βΌ Ο β§ βπ β (topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π)))) |
43 | 9, 15, 36, 42 | syl12anc 836 |
. . . . . . . 8
β’ ((π β TopBases β§ π βΌ Ο β§ π₯ β βͺ (topGenβπ)) β βπ β π« (topGenβπ)(π βΌ Ο β§ βπ β (topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π)))) |
44 | 43 | 3expia 1122 |
. . . . . . 7
β’ ((π β TopBases β§ π βΌ Ο) β (π₯ β βͺ (topGenβπ) β βπ β π« (topGenβπ)(π βΌ Ο β§ βπ β (topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π))))) |
45 | | unieq 4880 |
. . . . . . . . 9
β’
((topGenβπ) =
π½ β βͺ (topGenβπ) = βͺ π½) |
46 | 45 | eleq2d 2820 |
. . . . . . . 8
β’
((topGenβπ) =
π½ β (π₯ β βͺ (topGenβπ) β π₯ β βͺ π½)) |
47 | | pweq 4578 |
. . . . . . . . 9
β’
((topGenβπ) =
π½ β π«
(topGenβπ) =
π« π½) |
48 | | raleq 3308 |
. . . . . . . . . 10
β’
((topGenβπ) =
π½ β (βπ β (topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π)) β βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π)))) |
49 | 48 | anbi2d 630 |
. . . . . . . . 9
β’
((topGenβπ) =
π½ β ((π βΌ Ο β§
βπ β
(topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π))) β (π βΌ Ο β§ βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π))))) |
50 | 47, 49 | rexeqbidv 3319 |
. . . . . . . 8
β’
((topGenβπ) =
π½ β (βπ β π«
(topGenβπ)(π βΌ Ο β§
βπ β
(topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π))) β βπ β π« π½(π βΌ Ο β§ βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π))))) |
51 | 46, 50 | imbi12d 345 |
. . . . . . 7
β’
((topGenβπ) =
π½ β ((π₯ β βͺ (topGenβπ) β βπ β π« (topGenβπ)(π βΌ Ο β§ βπ β (topGenβπ)(π₯ β π β βπ β π (π₯ β π β§ π β π)))) β (π₯ β βͺ π½ β βπ β π« π½(π βΌ Ο β§ βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π)))))) |
52 | 44, 51 | syl5ibcom 244 |
. . . . . 6
β’ ((π β TopBases β§ π βΌ Ο) β
((topGenβπ) = π½ β (π₯ β βͺ π½ β βπ β π« π½(π βΌ Ο β§ βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π)))))) |
53 | 52 | expimpd 455 |
. . . . 5
β’ (π β TopBases β ((π βΌ Ο β§
(topGenβπ) = π½) β (π₯ β βͺ π½ β βπ β π« π½(π βΌ Ο β§ βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π)))))) |
54 | 53 | rexlimiv 3142 |
. . . 4
β’
(βπ β
TopBases (π βΌ Ο
β§ (topGenβπ) =
π½) β (π₯ β βͺ π½
β βπ β
π« π½(π βΌ Ο β§
βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π))))) |
55 | 2, 54 | sylbi 216 |
. . 3
β’ (π½ β 2ndΟ
β (π₯ β βͺ π½
β βπ β
π« π½(π βΌ Ο β§
βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π))))) |
56 | 55 | ralrimiv 3139 |
. 2
β’ (π½ β 2ndΟ
β βπ₯ β
βͺ π½βπ β π« π½(π βΌ Ο β§ βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π)))) |
57 | | eqid 2733 |
. . 3
β’ βͺ π½ =
βͺ π½ |
58 | 57 | is1stc2 22816 |
. 2
β’ (π½ β 1stΟ
β (π½ β Top β§
βπ₯ β βͺ π½βπ β π« π½(π βΌ Ο β§ βπ β π½ (π₯ β π β βπ β π (π₯ β π β§ π β π))))) |
59 | 1, 56, 58 | sylanbrc 584 |
1
β’ (π½ β 2ndΟ
β π½ β
1stΟ) |