| Step | Hyp | Ref
| Expression |
|---|
| 1 | | blin2 24157 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π§ β (π₯ β© π¦)) β§ (π₯ β ran (ballβπ·) β§ π¦ β ran (ballβπ·))) β βπ β β+ (π§(ballβπ·)π) β (π₯ β© π¦)) |
| 2 | | simpll 763 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π§ β (π₯ β© π¦)) β§ (π₯ β ran (ballβπ·) β§ π¦ β ran (ballβπ·))) β π· β (βMetβπ)) |
| 3 | | elinel1 4196 |
. . . . . . . . . 10
β’ (π§ β (π₯ β© π¦) β π§ β π₯) |
| 4 | | elunii 4914 |
. . . . . . . . . 10
β’ ((π§ β π₯ β§ π₯ β ran (ballβπ·)) β π§ β βͺ ran
(ballβπ·)) |
| 5 | 3, 4 | sylan 578 |
. . . . . . . . 9
β’ ((π§ β (π₯ β© π¦) β§ π₯ β ran (ballβπ·)) β π§ β βͺ ran
(ballβπ·)) |
| 6 | 5 | ad2ant2lr 744 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π§ β (π₯ β© π¦)) β§ (π₯ β ran (ballβπ·) β§ π¦ β ran (ballβπ·))) β π§ β βͺ ran
(ballβπ·)) |
| 7 | | unirnbl 24148 |
. . . . . . . . 9
β’ (π· β (βMetβπ) β βͺ ran (ballβπ·) = π) |
| 8 | 7 | ad2antrr 722 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π§ β (π₯ β© π¦)) β§ (π₯ β ran (ballβπ·) β§ π¦ β ran (ballβπ·))) β βͺ ran
(ballβπ·) = π) |
| 9 | 6, 8 | eleqtrd 2833 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π§ β (π₯ β© π¦)) β§ (π₯ β ran (ballβπ·) β§ π¦ β ran (ballβπ·))) β π§ β π) |
| 10 | | blssex 24155 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π§ β π) β (βπ β ran (ballβπ·)(π§ β π β§ π β (π₯ β© π¦)) β βπ β β+ (π§(ballβπ·)π) β (π₯ β© π¦))) |
| 11 | 2, 9, 10 | syl2anc 582 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π§ β (π₯ β© π¦)) β§ (π₯ β ran (ballβπ·) β§ π¦ β ran (ballβπ·))) β (βπ β ran (ballβπ·)(π§ β π β§ π β (π₯ β© π¦)) β βπ β β+ (π§(ballβπ·)π) β (π₯ β© π¦))) |
| 12 | 1, 11 | mpbird 256 |
. . . . 5
β’ (((π· β (βMetβπ) β§ π§ β (π₯ β© π¦)) β§ (π₯ β ran (ballβπ·) β§ π¦ β ran (ballβπ·))) β βπ β ran (ballβπ·)(π§ β π β§ π β (π₯ β© π¦))) |
| 13 | 12 | ex 411 |
. . . 4
β’ ((π· β (βMetβπ) β§ π§ β (π₯ β© π¦)) β ((π₯ β ran (ballβπ·) β§ π¦ β ran (ballβπ·)) β βπ β ran (ballβπ·)(π§ β π β§ π β (π₯ β© π¦)))) |
| 14 | 13 | ralrimdva 3152 |
. . 3
β’ (π· β (βMetβπ) β ((π₯ β ran (ballβπ·) β§ π¦ β ran (ballβπ·)) β βπ§ β (π₯ β© π¦)βπ β ran (ballβπ·)(π§ β π β§ π β (π₯ β© π¦)))) |
| 15 | 14 | ralrimivv 3196 |
. 2
β’ (π· β (βMetβπ) β βπ₯ β ran (ballβπ·)βπ¦ β ran (ballβπ·)βπ§ β (π₯ β© π¦)βπ β ran (ballβπ·)(π§ β π β§ π β (π₯ β© π¦))) |
| 16 | | fvex 6905 |
. . . 4
β’
(ballβπ·)
β V |
| 17 | 16 | rnex 7907 |
. . 3
β’ ran
(ballβπ·) β
V |
| 18 | | isbasis2g 22673 |
. . 3
β’ (ran
(ballβπ·) β V
β (ran (ballβπ·)
β TopBases β βπ₯ β ran (ballβπ·)βπ¦ β ran (ballβπ·)βπ§ β (π₯ β© π¦)βπ β ran (ballβπ·)(π§ β π β§ π β (π₯ β© π¦)))) |
| 19 | 17, 18 | ax-mp 5 |
. 2
β’ (ran
(ballβπ·) β
TopBases β βπ₯
β ran (ballβπ·)βπ¦ β ran (ballβπ·)βπ§ β (π₯ β© π¦)βπ β ran (ballβπ·)(π§ β π β§ π β (π₯ β© π¦))) |
| 20 | 15, 19 | sylibr 233 |
1
β’ (π· β (βMetβπ) β ran (ballβπ·) β
TopBases) |
