Step | Hyp | Ref
| Expression |
1 | | sstotbnd.2 |
. . . 4
β’ π = (π βΎ (π Γ π)) |
2 | 1 | sstotbnd2 37155 |
. . 3
β’ ((π β (Metβπ) β§ π β π) β (π β (TotBndβπ) β βπ β β+ βπ£ β (π« π β© Fin)π β βͺ
π₯ β π£ (π₯(ballβπ)π))) |
3 | | elin 3959 |
. . . . . . . . 9
β’ (π£ β (π« π β© Fin) β (π£ β π« π β§ π£ β Fin)) |
4 | | rabfi 9271 |
. . . . . . . . . 10
β’ (π£ β Fin β {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β Fin) |
5 | 4 | anim2i 616 |
. . . . . . . . 9
β’ ((π£ β π« π β§ π£ β Fin) β (π£ β π« π β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β
Fin)) |
6 | 3, 5 | sylbi 216 |
. . . . . . . 8
β’ (π£ β (π« π β© Fin) β (π£ β π« π β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β
Fin)) |
7 | 6 | anim2i 616 |
. . . . . . 7
β’ ((π β βͺ π₯ β π£ (π₯(ballβπ)π) β§ π£ β (π« π β© Fin)) β (π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ (π£ β π« π β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β
Fin))) |
8 | 7 | ancoms 458 |
. . . . . 6
β’ ((π£ β (π« π β© Fin) β§ π β βͺ π₯ β π£ (π₯(ballβπ)π)) β (π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ (π£ β π« π β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β
Fin))) |
9 | | an12 642 |
. . . . . 6
β’ ((π β βͺ π₯ β π£ (π₯(ballβπ)π) β§ (π£ β π« π β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β Fin)) β (π£ β π« π β§ (π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β
Fin))) |
10 | 8, 9 | sylib 217 |
. . . . 5
β’ ((π£ β (π« π β© Fin) β§ π β βͺ π₯ β π£ (π₯(ballβπ)π)) β (π£ β π« π β§ (π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β
Fin))) |
11 | 10 | reximi2 3073 |
. . . 4
β’
(βπ£ β
(π« π β©
Fin)π β βͺ π₯ β π£ (π₯(ballβπ)π) β βπ£ β π« π(π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β
Fin)) |
12 | 11 | ralimi 3077 |
. . 3
β’
(βπ β
β+ βπ£ β (π« π β© Fin)π β βͺ
π₯ β π£ (π₯(ballβπ)π) β βπ β β+ βπ£ β π« π(π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β
Fin)) |
13 | 2, 12 | syl6bi 253 |
. 2
β’ ((π β (Metβπ) β§ π β π) β (π β (TotBndβπ) β βπ β β+ βπ£ β π« π(π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β
Fin))) |
14 | | ssrab2 4072 |
. . . . . . . 8
β’ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β π£ |
15 | | elpwi 4604 |
. . . . . . . . 9
β’ (π£ β π« π β π£ β π) |
16 | 15 | ad2antlr 724 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ π β π) β§ π£ β π« π) β§ (π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β Fin)) β π£ β π) |
17 | 14, 16 | sstrid 3988 |
. . . . . . 7
β’ ((((π β (Metβπ) β§ π β π) β§ π£ β π« π) β§ (π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β Fin)) β {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β π) |
18 | | simprr 770 |
. . . . . . 7
β’ ((((π β (Metβπ) β§ π β π) β§ π£ β π« π) β§ (π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β Fin)) β {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β Fin) |
19 | | elfpw 9356 |
. . . . . . 7
β’ ({π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β (π« π β© Fin) β ({π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β π β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β
Fin)) |
20 | 17, 18, 19 | sylanbrc 582 |
. . . . . 6
β’ ((((π β (Metβπ) β§ π β π) β§ π£ β π« π) β§ (π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β Fin)) β {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β (π« π β© Fin)) |
21 | | ssel2 3972 |
. . . . . . . . . . . 12
β’ ((π β βͺ π₯ β π£ (π₯(ballβπ)π) β§ π§ β π) β π§ β βͺ
π₯ β π£ (π₯(ballβπ)π)) |
22 | | eliun 4994 |
. . . . . . . . . . . 12
β’ (π§ β βͺ π₯ β π£ (π₯(ballβπ)π) β βπ₯ β π£ π§ β (π₯(ballβπ)π)) |
23 | 21, 22 | sylib 217 |
. . . . . . . . . . 11
β’ ((π β βͺ π₯ β π£ (π₯(ballβπ)π) β§ π§ β π) β βπ₯ β π£ π§ β (π₯(ballβπ)π)) |
24 | | inelcm 4459 |
. . . . . . . . . . . . . . 15
β’ ((π§ β (π₯(ballβπ)π) β§ π§ β π) β ((π₯(ballβπ)π) β© π) β β
) |
25 | 24 | expcom 413 |
. . . . . . . . . . . . . 14
β’ (π§ β π β (π§ β (π₯(ballβπ)π) β ((π₯(ballβπ)π) β© π) β β
)) |
26 | 25 | ancrd 551 |
. . . . . . . . . . . . 13
β’ (π§ β π β (π§ β (π₯(ballβπ)π) β (((π₯(ballβπ)π) β© π) β β
β§ π§ β (π₯(ballβπ)π)))) |
27 | 26 | reximdv 3164 |
. . . . . . . . . . . 12
β’ (π§ β π β (βπ₯ β π£ π§ β (π₯(ballβπ)π) β βπ₯ β π£ (((π₯(ballβπ)π) β© π) β β
β§ π§ β (π₯(ballβπ)π)))) |
28 | 27 | impcom 407 |
. . . . . . . . . . 11
β’
((βπ₯ β
π£ π§ β (π₯(ballβπ)π) β§ π§ β π) β βπ₯ β π£ (((π₯(ballβπ)π) β© π) β β
β§ π§ β (π₯(ballβπ)π))) |
29 | 23, 28 | sylancom 587 |
. . . . . . . . . 10
β’ ((π β βͺ π₯ β π£ (π₯(ballβπ)π) β§ π§ β π) β βπ₯ β π£ (((π₯(ballβπ)π) β© π) β β
β§ π§ β (π₯(ballβπ)π))) |
30 | | eliun 4994 |
. . . . . . . . . . 11
β’ (π§ β βͺ π¦ β {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} (π¦(ballβπ)π) β βπ¦ β {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
}π§ β (π¦(ballβπ)π)) |
31 | | oveq1 7412 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β (π¦(ballβπ)π) = (π₯(ballβπ)π)) |
32 | 31 | eleq2d 2813 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β (π§ β (π¦(ballβπ)π) β π§ β (π₯(ballβπ)π))) |
33 | 32 | rexrab2 3691 |
. . . . . . . . . . 11
β’
(βπ¦ β
{π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
}π§ β (π¦(ballβπ)π) β βπ₯ β π£ (((π₯(ballβπ)π) β© π) β β
β§ π§ β (π₯(ballβπ)π))) |
34 | 30, 33 | bitri 275 |
. . . . . . . . . 10
β’ (π§ β βͺ π¦ β {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} (π¦(ballβπ)π) β βπ₯ β π£ (((π₯(ballβπ)π) β© π) β β
β§ π§ β (π₯(ballβπ)π))) |
35 | 29, 34 | sylibr 233 |
. . . . . . . . 9
β’ ((π β βͺ π₯ β π£ (π₯(ballβπ)π) β§ π§ β π) β π§ β βͺ
π¦ β {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} (π¦(ballβπ)π)) |
36 | 35 | ex 412 |
. . . . . . . 8
β’ (π β βͺ π₯ β π£ (π₯(ballβπ)π) β (π§ β π β π§ β βͺ
π¦ β {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} (π¦(ballβπ)π))) |
37 | 36 | ssrdv 3983 |
. . . . . . 7
β’ (π β βͺ π₯ β π£ (π₯(ballβπ)π) β π β βͺ
π¦ β {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} (π¦(ballβπ)π)) |
38 | 37 | ad2antrl 725 |
. . . . . 6
β’ ((((π β (Metβπ) β§ π β π) β§ π£ β π« π) β§ (π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β Fin)) β π β βͺ π¦ β {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} (π¦(ballβπ)π)) |
39 | | iuneq1 5006 |
. . . . . . . 8
β’ (π€ = {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β βͺ π¦ β π€ (π¦(ballβπ)π) = βͺ π¦ β {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} (π¦(ballβπ)π)) |
40 | 39 | sseq2d 4009 |
. . . . . . 7
β’ (π€ = {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β (π β βͺ
π¦ β π€ (π¦(ballβπ)π) β π β βͺ
π¦ β {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} (π¦(ballβπ)π))) |
41 | 40 | rspcev 3606 |
. . . . . 6
β’ (({π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β (π« π β© Fin) β§ π β βͺ π¦ β {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} (π¦(ballβπ)π)) β βπ€ β (π« π β© Fin)π β βͺ
π¦ β π€ (π¦(ballβπ)π)) |
42 | 20, 38, 41 | syl2anc 583 |
. . . . 5
β’ ((((π β (Metβπ) β§ π β π) β§ π£ β π« π) β§ (π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β Fin)) β
βπ€ β (π«
π β© Fin)π β βͺ π¦ β π€ (π¦(ballβπ)π)) |
43 | 42 | rexlimdva2 3151 |
. . . 4
β’ ((π β (Metβπ) β§ π β π) β (βπ£ β π« π(π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β Fin) β
βπ€ β (π«
π β© Fin)π β βͺ π¦ β π€ (π¦(ballβπ)π))) |
44 | 43 | ralimdv 3163 |
. . 3
β’ ((π β (Metβπ) β§ π β π) β (βπ β β+ βπ£ β π« π(π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β Fin) β
βπ β
β+ βπ€ β (π« π β© Fin)π β βͺ
π¦ β π€ (π¦(ballβπ)π))) |
45 | 1 | sstotbnd2 37155 |
. . 3
β’ ((π β (Metβπ) β§ π β π) β (π β (TotBndβπ) β βπ β β+ βπ€ β (π« π β© Fin)π β βͺ
π¦ β π€ (π¦(ballβπ)π))) |
46 | 44, 45 | sylibrd 259 |
. 2
β’ ((π β (Metβπ) β§ π β π) β (βπ β β+ βπ£ β π« π(π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β Fin) β π β (TotBndβπ))) |
47 | 13, 46 | impbid 211 |
1
β’ ((π β (Metβπ) β§ π β π) β (π β (TotBndβπ) β βπ β β+ βπ£ β π« π(π β βͺ
π₯ β π£ (π₯(ballβπ)π) β§ {π₯ β π£ β£ ((π₯(ballβπ)π) β© π) β β
} β
Fin))) |