| Step | Hyp | Ref
| Expression |
|---|
| 1 | | indif1 4272 |
. . . . . . 7
β’ ((π΅ β {β
}) β©
π« π₯) = ((π΅ β© π« π₯) β
{β
}) |
| 2 | 1 | unieqi 4922 |
. . . . . 6
β’ βͺ ((π΅
β {β
}) β© π« π₯) = βͺ ((π΅ β© π« π₯) β
{β
}) |
| 3 | | unidif0 5359 |
. . . . . 6
β’ βͺ ((π΅
β© π« π₯) β
{β
}) = βͺ (π΅ β© π« π₯) |
| 4 | 2, 3 | eqtri 2761 |
. . . . 5
β’ βͺ ((π΅
β {β
}) β© π« π₯) = βͺ (π΅ β© π« π₯) |
| 5 | 4 | sseq2i 4012 |
. . . 4
β’ (π₯ β βͺ ((π΅
β {β
}) β© π« π₯) β π₯ β βͺ (π΅ β© π« π₯)) |
| 6 | 5 | abbii 2803 |
. . 3
β’ {π₯ β£ π₯ β βͺ ((π΅ β {β
}) β©
π« π₯)} = {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)} |
| 7 | | difexg 5328 |
. . . 4
β’ (π΅ β V β (π΅ β {β
}) β
V) |
| 8 | | tgval 22458 |
. . . 4
β’ ((π΅ β {β
}) β V
β (topGenβ(π΅
β {β
})) = {π₯
β£ π₯ β βͺ ((π΅
β {β
}) β© π« π₯)}) |
| 9 | 7, 8 | syl 17 |
. . 3
β’ (π΅ β V β
(topGenβ(π΅ β
{β
})) = {π₯ β£
π₯ β βͺ ((π΅
β {β
}) β© π« π₯)}) |
| 10 | | tgval 22458 |
. . 3
β’ (π΅ β V β
(topGenβπ΅) = {π₯ β£ π₯ β βͺ (π΅ β© π« π₯)}) |
| 11 | 6, 9, 10 | 3eqtr4a 2799 |
. 2
β’ (π΅ β V β
(topGenβ(π΅ β
{β
})) = (topGenβπ΅)) |
| 12 | | difsnexi 7748 |
. . . 4
β’ ((π΅ β {β
}) β V
β π΅ β
V) |
| 13 | | fvprc 6884 |
. . . 4
β’ (Β¬
(π΅ β {β
})
β V β (topGenβ(π΅ β {β
})) =
β
) |
| 14 | 12, 13 | nsyl5 159 |
. . 3
β’ (Β¬
π΅ β V β
(topGenβ(π΅ β
{β
})) = β
) |
| 15 | | fvprc 6884 |
. . 3
β’ (Β¬
π΅ β V β
(topGenβπ΅) =
β
) |
| 16 | 14, 15 | eqtr4d 2776 |
. 2
β’ (Β¬
π΅ β V β
(topGenβ(π΅ β
{β
})) = (topGenβπ΅)) |
| 17 | 11, 16 | pm2.61i 182 |
1
β’
(topGenβ(π΅
β {β
})) = (topGenβπ΅) |
