Step | Hyp | Ref
| Expression |
1 | | indif1 4232 |
. . . . . . 7
β’ ((π΅ β {β
}) β©
π« π₯) = ((π΅ β© π« π₯) β
{β
}) |
2 | 1 | unieqi 4879 |
. . . . . 6
β’ βͺ ((π΅
β {β
}) β© π« π₯) = βͺ ((π΅ β© π« π₯) β
{β
}) |
3 | | unidif0 5316 |
. . . . . 6
β’ βͺ ((π΅
β© π« π₯) β
{β
}) = βͺ (π΅ β© π« π₯) |
4 | 2, 3 | eqtri 2761 |
. . . . 5
β’ βͺ ((π΅
β {β
}) β© π« π₯) = βͺ (π΅ β© π« π₯) |
5 | 4 | sseq2i 3974 |
. . . 4
β’ (π₯ β βͺ ((π΅
β {β
}) β© π« π₯) β π₯ β βͺ (π΅ β© π« π₯)) |
6 | 5 | abbii 2803 |
. . 3
β’ {π₯ β£ π₯ β βͺ ((π΅ β {β
}) β©
π« π₯)} = {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)} |
7 | | difexg 5285 |
. . . 4
β’ (π΅ β V β (π΅ β {β
}) β
V) |
8 | | tgval 22321 |
. . . 4
β’ ((π΅ β {β
}) β V
β (topGenβ(π΅
β {β
})) = {π₯
β£ π₯ β βͺ ((π΅
β {β
}) β© π« π₯)}) |
9 | 7, 8 | syl 17 |
. . 3
β’ (π΅ β V β
(topGenβ(π΅ β
{β
})) = {π₯ β£
π₯ β βͺ ((π΅
β {β
}) β© π« π₯)}) |
10 | | tgval 22321 |
. . 3
β’ (π΅ β V β
(topGenβπ΅) = {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)}) |
11 | 6, 9, 10 | 3eqtr4a 2799 |
. 2
β’ (π΅ β V β
(topGenβ(π΅ β
{β
})) = (topGenβπ΅)) |
12 | | difsnexi 7696 |
. . . 4
β’ ((π΅ β {β
}) β V
β π΅ β
V) |
13 | | fvprc 6835 |
. . . 4
β’ (Β¬
(π΅ β {β
})
β V β (topGenβ(π΅ β {β
})) =
β
) |
14 | 12, 13 | nsyl5 159 |
. . 3
β’ (Β¬
π΅ β V β
(topGenβ(π΅ β
{β
})) = β
) |
15 | | fvprc 6835 |
. . 3
β’ (Β¬
π΅ β V β
(topGenβπ΅) =
β
) |
16 | 14, 15 | eqtr4d 2776 |
. 2
β’ (Β¬
π΅ β V β
(topGenβ(π΅ β
{β
})) = (topGenβπ΅)) |
17 | 11, 16 | pm2.61i 182 |
1
β’
(topGenβ(π΅
β {β
})) = (topGenβπ΅) |