Step | Hyp | Ref
| Expression |
1 | | pwexg 5334 |
. 2
β’ (π΅ β π β π« π΅ β V) |
2 | | inss1 4189 |
. . . . 5
β’ (π΅ β© π« π₯) β π΅ |
3 | | vpwex 5333 |
. . . . . . 7
β’ π«
π₯ β V |
4 | 3 | inex2 5276 |
. . . . . 6
β’ (π΅ β© π« π₯) β V |
5 | 4 | elpw 4565 |
. . . . 5
β’ ((π΅ β© π« π₯) β π« π΅ β (π΅ β© π« π₯) β π΅) |
6 | 2, 5 | mpbir 230 |
. . . 4
β’ (π΅ β© π« π₯) β π« π΅ |
7 | 6 | a1i 11 |
. . 3
β’ (π₯ β (topGenβπ΅) β (π΅ β© π« π₯) β π« π΅) |
8 | | unieq 4877 |
. . . . . . 7
β’ ((π΅ β© π« π₯) = (π΅ β© π« π¦) β βͺ (π΅ β© π« π₯) = βͺ
(π΅ β© π« π¦)) |
9 | 8 | adantl 483 |
. . . . . 6
β’ (((π₯ β (topGenβπ΅) β§ π¦ β (topGenβπ΅)) β§ (π΅ β© π« π₯) = (π΅ β© π« π¦)) β βͺ (π΅ β© π« π₯) = βͺ
(π΅ β© π« π¦)) |
10 | | eltg4i 22326 |
. . . . . . 7
β’ (π₯ β (topGenβπ΅) β π₯ = βͺ (π΅ β© π« π₯)) |
11 | 10 | ad2antrr 725 |
. . . . . 6
β’ (((π₯ β (topGenβπ΅) β§ π¦ β (topGenβπ΅)) β§ (π΅ β© π« π₯) = (π΅ β© π« π¦)) β π₯ = βͺ (π΅ β© π« π₯)) |
12 | | eltg4i 22326 |
. . . . . . 7
β’ (π¦ β (topGenβπ΅) β π¦ = βͺ (π΅ β© π« π¦)) |
13 | 12 | ad2antlr 726 |
. . . . . 6
β’ (((π₯ β (topGenβπ΅) β§ π¦ β (topGenβπ΅)) β§ (π΅ β© π« π₯) = (π΅ β© π« π¦)) β π¦ = βͺ (π΅ β© π« π¦)) |
14 | 9, 11, 13 | 3eqtr4d 2783 |
. . . . 5
β’ (((π₯ β (topGenβπ΅) β§ π¦ β (topGenβπ΅)) β§ (π΅ β© π« π₯) = (π΅ β© π« π¦)) β π₯ = π¦) |
15 | 14 | ex 414 |
. . . 4
β’ ((π₯ β (topGenβπ΅) β§ π¦ β (topGenβπ΅)) β ((π΅ β© π« π₯) = (π΅ β© π« π¦) β π₯ = π¦)) |
16 | | pweq 4575 |
. . . . 5
β’ (π₯ = π¦ β π« π₯ = π« π¦) |
17 | 16 | ineq2d 4173 |
. . . 4
β’ (π₯ = π¦ β (π΅ β© π« π₯) = (π΅ β© π« π¦)) |
18 | 15, 17 | impbid1 224 |
. . 3
β’ ((π₯ β (topGenβπ΅) β§ π¦ β (topGenβπ΅)) β ((π΅ β© π« π₯) = (π΅ β© π« π¦) β π₯ = π¦)) |
19 | 7, 18 | dom2 8938 |
. 2
β’
(π« π΅ β
V β (topGenβπ΅)
βΌ π« π΅) |
20 | 1, 19 | syl 17 |
1
β’ (π΅ β π β (topGenβπ΅) βΌ π« π΅) |