| Step | Hyp | Ref
| Expression |
|---|
| 1 | | simpll 527 |
. . 3
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π· β (βMetβπ)) |
| 2 | | simprl 529 |
. . 3
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π΅ β ran (ballβπ·)) |
| 3 | | simplr 528 |
. . . 4
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π β (π΅ β© πΆ)) |
| 4 | 3 | elin1d 3325 |
. . 3
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π β π΅) |
| 5 | | blss 13931 |
. . 3
β’ ((π· β (βMetβπ) β§ π΅ β ran (ballβπ·) β§ π β π΅) β βπ¦ β β+ (π(ballβπ·)π¦) β π΅) |
| 6 | 1, 2, 4, 5 | syl3anc 1238 |
. 2
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β βπ¦ β β+ (π(ballβπ·)π¦) β π΅) |
| 7 | | simprr 531 |
. . 3
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β πΆ β ran (ballβπ·)) |
| 8 | 3 | elin2d 3326 |
. . 3
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π β πΆ) |
| 9 | | blss 13931 |
. . 3
β’ ((π· β (βMetβπ) β§ πΆ β ran (ballβπ·) β§ π β πΆ) β βπ§ β β+ (π(ballβπ·)π§) β πΆ) |
| 10 | 1, 7, 8, 9 | syl3anc 1238 |
. 2
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β βπ§ β β+ (π(ballβπ·)π§) β πΆ) |
| 11 | | reeanv 2647 |
. . 3
β’
(βπ¦ β
β+ βπ§ β β+ ((π(ballβπ·)π¦) β π΅ β§ (π(ballβπ·)π§) β πΆ) β (βπ¦ β β+ (π(ballβπ·)π¦) β π΅ β§ βπ§ β β+ (π(ballβπ·)π§) β πΆ)) |
| 12 | | ss2in 3364 |
. . . . 5
β’ (((π(ballβπ·)π¦) β π΅ β§ (π(ballβπ·)π§) β πΆ) β ((π(ballβπ·)π¦) β© (π(ballβπ·)π§)) β (π΅ β© πΆ)) |
| 13 | | inss1 3356 |
. . . . . . . . . . 11
β’ (π΅ β© πΆ) β π΅ |
| 14 | | blf 13913 |
. . . . . . . . . . . . . 14
β’ (π· β (βMetβπ) β (ballβπ·):(π Γ
β*)βΆπ« π) |
| 15 | | frn 5375 |
. . . . . . . . . . . . . 14
β’
((ballβπ·):(π Γ
β*)βΆπ« π β ran (ballβπ·) β π« π) |
| 16 | 1, 14, 15 | 3syl 17 |
. . . . . . . . . . . . 13
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β ran (ballβπ·) β π« π) |
| 17 | 16, 2 | sseldd 3157 |
. . . . . . . . . . . 12
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π΅ β π« π) |
| 18 | 17 | elpwid 3587 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π΅ β π) |
| 19 | 13, 18 | sstrid 3167 |
. . . . . . . . . 10
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β (π΅ β© πΆ) β π) |
| 20 | 19, 3 | sseldd 3157 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β π β π) |
| 21 | 1, 20 | jca 306 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β (π· β (βMetβπ) β§ π β π)) |
| 22 | | rpxr 9661 |
. . . . . . . . 9
β’ (π¦ β β+
β π¦ β
β*) |
| 23 | | rpxr 9661 |
. . . . . . . . 9
β’ (π§ β β+
β π§ β
β*) |
| 24 | 22, 23 | anim12i 338 |
. . . . . . . 8
β’ ((π¦ β β+
β§ π§ β
β+) β (π¦ β β* β§ π§ β
β*)) |
| 25 | | blininf 13927 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π β π) β§ (π¦ β β* β§ π§ β β*))
β ((π(ballβπ·)π¦) β© (π(ballβπ·)π§)) = (π(ballβπ·)inf({π¦, π§}, β*, <
))) |
| 26 | 21, 24, 25 | syl2an 289 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β§ (π¦ β β+ β§ π§ β β+))
β ((π(ballβπ·)π¦) β© (π(ballβπ·)π§)) = (π(ballβπ·)inf({π¦, π§}, β*, <
))) |
| 27 | 26 | sseq1d 3185 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β§ (π¦ β β+ β§ π§ β β+))
β (((π(ballβπ·)π¦) β© (π(ballβπ·)π§)) β (π΅ β© πΆ) β (π(ballβπ·)inf({π¦, π§}, β*, < )) β
(π΅ β© πΆ))) |
| 28 | | xrminrpcl 11282 |
. . . . . . . 8
β’ ((π¦ β β+
β§ π§ β
β+) β inf({π¦, π§}, β*, < ) β
β+) |
| 29 | | oveq2 5883 |
. . . . . . . . . . 11
β’ (π₯ = inf({π¦, π§}, β*, < ) β (π(ballβπ·)π₯) = (π(ballβπ·)inf({π¦, π§}, β*, <
))) |
| 30 | 29 | sseq1d 3185 |
. . . . . . . . . 10
β’ (π₯ = inf({π¦, π§}, β*, < ) β ((π(ballβπ·)π₯) β (π΅ β© πΆ) β (π(ballβπ·)inf({π¦, π§}, β*, < )) β
(π΅ β© πΆ))) |
| 31 | 30 | rspcev 2842 |
. . . . . . . . 9
β’
((inf({π¦, π§}, β*, < )
β β+ β§ (π(ballβπ·)inf({π¦, π§}, β*, < )) β
(π΅ β© πΆ)) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ)) |
| 32 | 31 | ex 115 |
. . . . . . . 8
β’
(inf({π¦, π§}, β*, < )
β β+ β ((π(ballβπ·)inf({π¦, π§}, β*, < )) β
(π΅ β© πΆ) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ))) |
| 33 | 28, 32 | syl 14 |
. . . . . . 7
β’ ((π¦ β β+
β§ π§ β
β+) β ((π(ballβπ·)inf({π¦, π§}, β*, < )) β
(π΅ β© πΆ) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ))) |
| 34 | 33 | adantl 277 |
. . . . . 6
β’ ((((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β§ (π¦ β β+ β§ π§ β β+))
β ((π(ballβπ·)inf({π¦, π§}, β*, < )) β
(π΅ β© πΆ) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ))) |
| 35 | 27, 34 | sylbid 150 |
. . . . 5
β’ ((((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β§ (π¦ β β+ β§ π§ β β+))
β (((π(ballβπ·)π¦) β© (π(ballβπ·)π§)) β (π΅ β© πΆ) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ))) |
| 36 | 12, 35 | syl5 32 |
. . . 4
β’ ((((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β§ (π¦ β β+ β§ π§ β β+))
β (((π(ballβπ·)π¦) β π΅ β§ (π(ballβπ·)π§) β πΆ) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ))) |
| 37 | 36 | rexlimdvva 2602 |
. . 3
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β (βπ¦ β β+ βπ§ β β+
((π(ballβπ·)π¦) β π΅ β§ (π(ballβπ·)π§) β πΆ) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ))) |
| 38 | 11, 37 | biimtrrid 153 |
. 2
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β ((βπ¦ β β+ (π(ballβπ·)π¦) β π΅ β§ βπ§ β β+ (π(ballβπ·)π§) β πΆ) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ))) |
| 39 | 6, 10, 38 | mp2and 433 |
1
β’ (((π· β (βMetβπ) β§ π β (π΅ β© πΆ)) β§ (π΅ β ran (ballβπ·) β§ πΆ β ran (ballβπ·))) β βπ₯ β β+ (π(ballβπ·)π₯) β (π΅ β© πΆ)) |
