Step | Hyp | Ref
| Expression |
1 | | tgval 22321 |
. 2
β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)}) |
2 | | inss1 4189 |
. . . . . . . . 9
β’ (π΅ β© π« π₯) β π΅ |
3 | 2 | unissi 4875 |
. . . . . . . 8
β’ βͺ (π΅
β© π« π₯) β
βͺ π΅ |
4 | 3 | sseli 3941 |
. . . . . . 7
β’ (π¦ β βͺ (π΅
β© π« π₯) β
π¦ β βͺ π΅) |
5 | 4 | pm4.71ri 562 |
. . . . . 6
β’ (π¦ β βͺ (π΅
β© π« π₯) β
(π¦ β βͺ π΅
β§ π¦ β βͺ (π΅
β© π« π₯))) |
6 | 5 | ralbii 3093 |
. . . . 5
β’
(βπ¦ β
π₯ π¦ β βͺ (π΅ β© π« π₯) β βπ¦ β π₯ (π¦ β βͺ π΅ β§ π¦ β βͺ (π΅ β© π« π₯))) |
7 | | r19.26 3111 |
. . . . 5
β’
(βπ¦ β
π₯ (π¦ β βͺ π΅ β§ π¦ β βͺ (π΅ β© π« π₯)) β (βπ¦ β π₯ π¦ β βͺ π΅ β§ βπ¦ β π₯ π¦ β βͺ (π΅ β© π« π₯))) |
8 | 6, 7 | bitri 275 |
. . . 4
β’
(βπ¦ β
π₯ π¦ β βͺ (π΅ β© π« π₯) β (βπ¦ β π₯ π¦ β βͺ π΅ β§ βπ¦ β π₯ π¦ β βͺ (π΅ β© π« π₯))) |
9 | | dfss3 3933 |
. . . 4
β’ (π₯ β βͺ (π΅
β© π« π₯) β
βπ¦ β π₯ π¦ β βͺ (π΅ β© π« π₯)) |
10 | | dfss3 3933 |
. . . . 5
β’ (π₯ β βͺ π΅
β βπ¦ β
π₯ π¦ β βͺ π΅) |
11 | | elin 3927 |
. . . . . . . . . . 11
β’ (π§ β (π΅ β© π« π₯) β (π§ β π΅ β§ π§ β π« π₯)) |
12 | 11 | anbi2i 624 |
. . . . . . . . . 10
β’ ((π¦ β π§ β§ π§ β (π΅ β© π« π₯)) β (π¦ β π§ β§ (π§ β π΅ β§ π§ β π« π₯))) |
13 | | an12 644 |
. . . . . . . . . 10
β’ ((π¦ β π§ β§ (π§ β π΅ β§ π§ β π« π₯)) β (π§ β π΅ β§ (π¦ β π§ β§ π§ β π« π₯))) |
14 | 12, 13 | bitri 275 |
. . . . . . . . 9
β’ ((π¦ β π§ β§ π§ β (π΅ β© π« π₯)) β (π§ β π΅ β§ (π¦ β π§ β§ π§ β π« π₯))) |
15 | 14 | exbii 1851 |
. . . . . . . 8
β’
(βπ§(π¦ β π§ β§ π§ β (π΅ β© π« π₯)) β βπ§(π§ β π΅ β§ (π¦ β π§ β§ π§ β π« π₯))) |
16 | | eluni 4869 |
. . . . . . . 8
β’ (π¦ β βͺ (π΅
β© π« π₯) β
βπ§(π¦ β π§ β§ π§ β (π΅ β© π« π₯))) |
17 | | df-rex 3071 |
. . . . . . . 8
β’
(βπ§ β
π΅ (π¦ β π§ β§ π§ β π« π₯) β βπ§(π§ β π΅ β§ (π¦ β π§ β§ π§ β π« π₯))) |
18 | 15, 16, 17 | 3bitr4i 303 |
. . . . . . 7
β’ (π¦ β βͺ (π΅
β© π« π₯) β
βπ§ β π΅ (π¦ β π§ β§ π§ β π« π₯)) |
19 | | velpw 4566 |
. . . . . . . . 9
β’ (π§ β π« π₯ β π§ β π₯) |
20 | 19 | anbi2i 624 |
. . . . . . . 8
β’ ((π¦ β π§ β§ π§ β π« π₯) β (π¦ β π§ β§ π§ β π₯)) |
21 | 20 | rexbii 3094 |
. . . . . . 7
β’
(βπ§ β
π΅ (π¦ β π§ β§ π§ β π« π₯) β βπ§ β π΅ (π¦ β π§ β§ π§ β π₯)) |
22 | 18, 21 | bitr2i 276 |
. . . . . 6
β’
(βπ§ β
π΅ (π¦ β π§ β§ π§ β π₯) β π¦ β βͺ (π΅ β© π« π₯)) |
23 | 22 | ralbii 3093 |
. . . . 5
β’
(βπ¦ β
π₯ βπ§ β π΅ (π¦ β π§ β§ π§ β π₯) β βπ¦ β π₯ π¦ β βͺ (π΅ β© π« π₯)) |
24 | 10, 23 | anbi12i 628 |
. . . 4
β’ ((π₯ β βͺ π΅
β§ βπ¦ β
π₯ βπ§ β π΅ (π¦ β π§ β§ π§ β π₯)) β (βπ¦ β π₯ π¦ β βͺ π΅ β§ βπ¦ β π₯ π¦ β βͺ (π΅ β© π« π₯))) |
25 | 8, 9, 24 | 3bitr4i 303 |
. . 3
β’ (π₯ β βͺ (π΅
β© π« π₯) β
(π₯ β βͺ π΅
β§ βπ¦ β
π₯ βπ§ β π΅ (π¦ β π§ β§ π§ β π₯))) |
26 | 25 | abbii 2803 |
. 2
β’ {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)} = {π₯ β£ (π₯ β βͺ π΅ β§ βπ¦ β π₯ βπ§ β π΅ (π¦ β π§ β§ π§ β π₯))} |
27 | 1, 26 | eqtrdi 2789 |
1
β’ (π΅ β π β (topGenβπ΅) = {π₯ β£ (π₯ β βͺ π΅ β§ βπ¦ β π₯ βπ§ β π΅ (π¦ β π§ β§ π§ β π₯))}) |