Step | Hyp | Ref
| Expression |
1 | | simpr 110 |
. . . . 5
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β βͺ π΅ =
βͺ πΆ) |
2 | | uniexg 4439 |
. . . . . 6
β’ (π΅ β π β βͺ π΅ β V) |
3 | 2 | adantr 276 |
. . . . 5
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β βͺ π΅
β V) |
4 | 1, 3 | eqeltrrd 2255 |
. . . 4
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β βͺ πΆ
β V) |
5 | | uniexb 4473 |
. . . 4
β’ (πΆ β V β βͺ πΆ
β V) |
6 | 4, 5 | sylibr 134 |
. . 3
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β πΆ β V) |
7 | | tgss3 13548 |
. . 3
β’ ((π΅ β π β§ πΆ β V) β ((topGenβπ΅) β (topGenβπΆ) β π΅ β (topGenβπΆ))) |
8 | 6, 7 | syldan 282 |
. 2
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β
((topGenβπ΅) β
(topGenβπΆ) β
π΅ β
(topGenβπΆ))) |
9 | | eltg2b 13524 |
. . . . . . 7
β’ (πΆ β V β (π¦ β (topGenβπΆ) β βπ₯ β π¦ βπ§ β πΆ (π₯ β π§ β§ π§ β π¦))) |
10 | 6, 9 | syl 14 |
. . . . . 6
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β (π¦ β (topGenβπΆ) β βπ₯ β π¦ βπ§ β πΆ (π₯ β π§ β§ π§ β π¦))) |
11 | | elunii 3814 |
. . . . . . . . 9
β’ ((π₯ β π¦ β§ π¦ β π΅) β π₯ β βͺ π΅) |
12 | 11 | ancoms 268 |
. . . . . . . 8
β’ ((π¦ β π΅ β§ π₯ β π¦) β π₯ β βͺ π΅) |
13 | | biimt 241 |
. . . . . . . 8
β’ (π₯ β βͺ π΅
β (βπ§ β
πΆ (π₯ β π§ β§ π§ β π¦) β (π₯ β βͺ π΅ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |
14 | 12, 13 | syl 14 |
. . . . . . 7
β’ ((π¦ β π΅ β§ π₯ β π¦) β (βπ§ β πΆ (π₯ β π§ β§ π§ β π¦) β (π₯ β βͺ π΅ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |
15 | 14 | ralbidva 2473 |
. . . . . 6
β’ (π¦ β π΅ β (βπ₯ β π¦ βπ§ β πΆ (π₯ β π§ β§ π§ β π¦) β βπ₯ β π¦ (π₯ β βͺ π΅ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |
16 | 10, 15 | sylan9bb 462 |
. . . . 5
β’ (((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β§ π¦ β π΅) β (π¦ β (topGenβπΆ) β βπ₯ β π¦ (π₯ β βͺ π΅ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |
17 | | ralcom3 2644 |
. . . . 5
β’
(βπ₯ β
π¦ (π₯ β βͺ π΅ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)) β βπ₯ β βͺ π΅(π₯ β π¦ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦))) |
18 | 16, 17 | bitrdi 196 |
. . . 4
β’ (((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β§ π¦ β π΅) β (π¦ β (topGenβπΆ) β βπ₯ β βͺ π΅(π₯ β π¦ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |
19 | 18 | ralbidva 2473 |
. . 3
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β (βπ¦ β π΅ π¦ β (topGenβπΆ) β βπ¦ β π΅ βπ₯ β βͺ π΅(π₯ β π¦ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |
20 | | dfss3 3145 |
. . 3
β’ (π΅ β (topGenβπΆ) β βπ¦ β π΅ π¦ β (topGenβπΆ)) |
21 | | ralcom 2640 |
. . 3
β’
(βπ₯ β
βͺ π΅βπ¦ β π΅ (π₯ β π¦ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)) β βπ¦ β π΅ βπ₯ β βͺ π΅(π₯ β π¦ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦))) |
22 | 19, 20, 21 | 3bitr4g 223 |
. 2
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β (π΅ β (topGenβπΆ) β βπ₯ β βͺ π΅βπ¦ β π΅ (π₯ β π¦ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |
23 | 8, 22 | bitrd 188 |
1
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β
((topGenβπ΅) β
(topGenβπΆ) β
βπ₯ β βͺ π΅βπ¦ β π΅ (π₯ β π¦ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |