Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . . 5
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β βͺ π΅ =
βͺ πΆ) |
2 | | uniexg 7673 |
. . . . . 6
β’ (π΅ β π β βͺ π΅ β V) |
3 | 2 | adantr 481 |
. . . . 5
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β βͺ π΅
β V) |
4 | 1, 3 | eqeltrrd 2839 |
. . . 4
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β βͺ πΆ
β V) |
5 | | uniexb 7694 |
. . . 4
β’ (πΆ β V β βͺ πΆ
β V) |
6 | 4, 5 | sylibr 233 |
. . 3
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β πΆ β V) |
7 | | tgss3 22320 |
. . 3
β’ ((π΅ β π β§ πΆ β V) β ((topGenβπ΅) β (topGenβπΆ) β π΅ β (topGenβπΆ))) |
8 | 6, 7 | syldan 591 |
. 2
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β
((topGenβπ΅) β
(topGenβπΆ) β
π΅ β
(topGenβπΆ))) |
9 | | eltg2b 22293 |
. . . . . . 7
β’ (πΆ β V β (π¦ β (topGenβπΆ) β βπ₯ β π¦ βπ§ β πΆ (π₯ β π§ β§ π§ β π¦))) |
10 | 6, 9 | syl 17 |
. . . . . 6
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β (π¦ β (topGenβπΆ) β βπ₯ β π¦ βπ§ β πΆ (π₯ β π§ β§ π§ β π¦))) |
11 | | elunii 4868 |
. . . . . . . . 9
β’ ((π₯ β π¦ β§ π¦ β π΅) β π₯ β βͺ π΅) |
12 | 11 | ancoms 459 |
. . . . . . . 8
β’ ((π¦ β π΅ β§ π₯ β π¦) β π₯ β βͺ π΅) |
13 | | biimt 360 |
. . . . . . . 8
β’ (π₯ β βͺ π΅
β (βπ§ β
πΆ (π₯ β π§ β§ π§ β π¦) β (π₯ β βͺ π΅ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |
14 | 12, 13 | syl 17 |
. . . . . . 7
β’ ((π¦ β π΅ β§ π₯ β π¦) β (βπ§ β πΆ (π₯ β π§ β§ π§ β π¦) β (π₯ β βͺ π΅ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |
15 | 14 | ralbidva 3170 |
. . . . . 6
β’ (π¦ β π΅ β (βπ₯ β π¦ βπ§ β πΆ (π₯ β π§ β§ π§ β π¦) β βπ₯ β π¦ (π₯ β βͺ π΅ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |
16 | 10, 15 | sylan9bb 510 |
. . . . 5
β’ (((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β§ π¦ β π΅) β (π¦ β (topGenβπΆ) β βπ₯ β π¦ (π₯ β βͺ π΅ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |
17 | | ralcom3 3098 |
. . . . 5
β’
(βπ₯ β
π¦ (π₯ β βͺ π΅ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)) β βπ₯ β βͺ π΅(π₯ β π¦ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦))) |
18 | 16, 17 | bitrdi 286 |
. . . 4
β’ (((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β§ π¦ β π΅) β (π¦ β (topGenβπΆ) β βπ₯ β βͺ π΅(π₯ β π¦ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |
19 | 18 | ralbidva 3170 |
. . 3
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β (βπ¦ β π΅ π¦ β (topGenβπΆ) β βπ¦ β π΅ βπ₯ β βͺ π΅(π₯ β π¦ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |
20 | | dfss3 3930 |
. . 3
β’ (π΅ β (topGenβπΆ) β βπ¦ β π΅ π¦ β (topGenβπΆ)) |
21 | | ralcom 3270 |
. . 3
β’
(βπ₯ β
βͺ π΅βπ¦ β π΅ (π₯ β π¦ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)) β βπ¦ β π΅ βπ₯ β βͺ π΅(π₯ β π¦ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦))) |
22 | 19, 20, 21 | 3bitr4g 313 |
. 2
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β (π΅ β (topGenβπΆ) β βπ₯ β βͺ π΅βπ¦ β π΅ (π₯ β π¦ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |
23 | 8, 22 | bitrd 278 |
1
β’ ((π΅ β π β§ βͺ π΅ = βͺ
πΆ) β
((topGenβπ΅) β
(topGenβπΆ) β
βπ₯ β βͺ π΅βπ¦ β π΅ (π₯ β π¦ β βπ§ β πΆ (π₯ β π§ β§ π§ β π¦)))) |