Step | Hyp | Ref
| Expression |
1 | | istotbnd 36274 |
. 2
β’ (π β (TotBndβπ) β (π β (Metβπ) β§ βπ β β+ βπ€ β Fin (βͺ π€ =
π β§ βπ β π€ βπ₯ β π π = (π₯(ballβπ)π)))) |
2 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π₯ = (πβπ) β (π₯(ballβπ)π) = ((πβπ)(ballβπ)π)) |
3 | 2 | eqeq2d 2744 |
. . . . . . . . . . 11
β’ (π₯ = (πβπ) β (π = (π₯(ballβπ)π) β π = ((πβπ)(ballβπ)π))) |
4 | 3 | ac6sfi 9234 |
. . . . . . . . . 10
β’ ((π€ β Fin β§ βπ β π€ βπ₯ β π π = (π₯(ballβπ)π)) β βπ(π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π))) |
5 | 4 | ex 414 |
. . . . . . . . 9
β’ (π€ β Fin β
(βπ β π€ βπ₯ β π π = (π₯(ballβπ)π) β βπ(π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) |
6 | 5 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ π€ β Fin) β§ βͺ π€ =
π) β (βπ β π€ βπ₯ β π π = (π₯(ballβπ)π) β βπ(π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) |
7 | | simprrl 780 |
. . . . . . . . . . . . 13
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β π:π€βΆπ) |
8 | 7 | frnd 6677 |
. . . . . . . . . . . 12
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β ran π β π) |
9 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β π€ β Fin) |
10 | 7 | ffnd 6670 |
. . . . . . . . . . . . . 14
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β π Fn π€) |
11 | | dffn4 6763 |
. . . . . . . . . . . . . 14
β’ (π Fn π€ β π:π€βontoβran π) |
12 | 10, 11 | sylib 217 |
. . . . . . . . . . . . 13
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β π:π€βontoβran π) |
13 | | fofi 9285 |
. . . . . . . . . . . . 13
β’ ((π€ β Fin β§ π:π€βontoβran π) β ran π β Fin) |
14 | 9, 12, 13 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β ran π β Fin) |
15 | | elfpw 9301 |
. . . . . . . . . . . 12
β’ (ran
π β (π« π β© Fin) β (ran π β π β§ ran π β Fin)) |
16 | 8, 14, 15 | sylanbrc 584 |
. . . . . . . . . . 11
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β ran π β (π« π β© Fin)) |
17 | 2 | eleq2d 2820 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = (πβπ) β (π£ β (π₯(ballβπ)π) β π£ β ((πβπ)(ballβπ)π))) |
18 | 17 | rexrn 7038 |
. . . . . . . . . . . . . . 15
β’ (π Fn π€ β (βπ₯ β ran π π£ β (π₯(ballβπ)π) β βπ β π€ π£ β ((πβπ)(ballβπ)π))) |
19 | 10, 18 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β (βπ₯ β ran π π£ β (π₯(ballβπ)π) β βπ β π€ π£ β ((πβπ)(ballβπ)π))) |
20 | | eliun 4959 |
. . . . . . . . . . . . . 14
β’ (π£ β βͺ π₯ β ran π(π₯(ballβπ)π) β βπ₯ β ran π π£ β (π₯(ballβπ)π)) |
21 | | eliun 4959 |
. . . . . . . . . . . . . 14
β’ (π£ β βͺ π β π€ ((πβπ)(ballβπ)π) β βπ β π€ π£ β ((πβπ)(ballβπ)π)) |
22 | 19, 20, 21 | 3bitr4g 314 |
. . . . . . . . . . . . 13
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β (π£ β βͺ
π₯ β ran π(π₯(ballβπ)π) β π£ β βͺ
π β π€ ((πβπ)(ballβπ)π))) |
23 | 22 | eqrdv 2731 |
. . . . . . . . . . . 12
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β βͺ π₯ β ran π(π₯(ballβπ)π) = βͺ π β π€ ((πβπ)(ballβπ)π)) |
24 | | simprrr 781 |
. . . . . . . . . . . . 13
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β βπ β π€ π = ((πβπ)(ballβπ)π)) |
25 | | iuneq2 4974 |
. . . . . . . . . . . . 13
β’
(βπ β
π€ π = ((πβπ)(ballβπ)π) β βͺ
π β π€ π = βͺ π β π€ ((πβπ)(ballβπ)π)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β βͺ π β π€ π = βͺ π β π€ ((πβπ)(ballβπ)π)) |
27 | | uniiun 5019 |
. . . . . . . . . . . . 13
β’ βͺ π€ =
βͺ π β π€ π |
28 | | simprl 770 |
. . . . . . . . . . . . 13
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β βͺ
π€ = π) |
29 | 27, 28 | eqtr3id 2787 |
. . . . . . . . . . . 12
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β βͺ π β π€ π = π) |
30 | 23, 26, 29 | 3eqtr2d 2779 |
. . . . . . . . . . 11
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β βͺ π₯ β ran π(π₯(ballβπ)π) = π) |
31 | | iuneq1 4971 |
. . . . . . . . . . . . 13
β’ (π£ = ran π β βͺ
π₯ β π£ (π₯(ballβπ)π) = βͺ π₯ β ran π(π₯(ballβπ)π)) |
32 | 31 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ (π£ = ran π β (βͺ
π₯ β π£ (π₯(ballβπ)π) = π β βͺ
π₯ β ran π(π₯(ballβπ)π) = π)) |
33 | 32 | rspcev 3580 |
. . . . . . . . . . 11
β’ ((ran
π β (π« π β© Fin) β§ βͺ π₯ β ran π(π₯(ballβπ)π) = π) β βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π) |
34 | 16, 30, 33 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β (Metβπ) β§ π€ β Fin) β§ (βͺ π€ =
π β§ (π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)))) β βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π) |
35 | 34 | expr 458 |
. . . . . . . . 9
β’ (((π β (Metβπ) β§ π€ β Fin) β§ βͺ π€ =
π) β ((π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)) β βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π)) |
36 | 35 | exlimdv 1937 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ π€ β Fin) β§ βͺ π€ =
π) β (βπ(π:π€βΆπ β§ βπ β π€ π = ((πβπ)(ballβπ)π)) β βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π)) |
37 | 6, 36 | syld 47 |
. . . . . . 7
β’ (((π β (Metβπ) β§ π€ β Fin) β§ βͺ π€ =
π) β (βπ β π€ βπ₯ β π π = (π₯(ballβπ)π) β βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π)) |
38 | 37 | expimpd 455 |
. . . . . 6
β’ ((π β (Metβπ) β§ π€ β Fin) β ((βͺ π€ =
π β§ βπ β π€ βπ₯ β π π = (π₯(ballβπ)π)) β βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π)) |
39 | 38 | rexlimdva 3149 |
. . . . 5
β’ (π β (Metβπ) β (βπ€ β Fin (βͺ π€ =
π β§ βπ β π€ βπ₯ β π π = (π₯(ballβπ)π)) β βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π)) |
40 | | elfpw 9301 |
. . . . . . . . . . 11
β’ (π£ β (π« π β© Fin) β (π£ β π β§ π£ β Fin)) |
41 | 40 | simprbi 498 |
. . . . . . . . . 10
β’ (π£ β (π« π β© Fin) β π£ β Fin) |
42 | 41 | ad2antrl 727 |
. . . . . . . . 9
β’ ((π β (Metβπ) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)π) = π)) β π£ β Fin) |
43 | | mptfi 9298 |
. . . . . . . . 9
β’ (π£ β Fin β (π₯ β π£ β¦ (π₯(ballβπ)π)) β Fin) |
44 | | rnfi 9282 |
. . . . . . . . 9
β’ ((π₯ β π£ β¦ (π₯(ballβπ)π)) β Fin β ran (π₯ β π£ β¦ (π₯(ballβπ)π)) β Fin) |
45 | 42, 43, 44 | 3syl 18 |
. . . . . . . 8
β’ ((π β (Metβπ) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)π) = π)) β ran (π₯ β π£ β¦ (π₯(ballβπ)π)) β Fin) |
46 | | ovex 7391 |
. . . . . . . . . 10
β’ (π₯(ballβπ)π) β V |
47 | 46 | dfiun3 5922 |
. . . . . . . . 9
β’ βͺ π₯ β π£ (π₯(ballβπ)π) = βͺ ran (π₯ β π£ β¦ (π₯(ballβπ)π)) |
48 | | simprr 772 |
. . . . . . . . 9
β’ ((π β (Metβπ) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)π) = π)) β βͺ π₯ β π£ (π₯(ballβπ)π) = π) |
49 | 47, 48 | eqtr3id 2787 |
. . . . . . . 8
β’ ((π β (Metβπ) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)π) = π)) β βͺ ran
(π₯ β π£ β¦ (π₯(ballβπ)π)) = π) |
50 | | eqid 2733 |
. . . . . . . . . 10
β’ (π₯ β π£ β¦ (π₯(ballβπ)π)) = (π₯ β π£ β¦ (π₯(ballβπ)π)) |
51 | 50 | rnmpt 5911 |
. . . . . . . . 9
β’ ran
(π₯ β π£ β¦ (π₯(ballβπ)π)) = {π β£ βπ₯ β π£ π = (π₯(ballβπ)π)} |
52 | 40 | simplbi 499 |
. . . . . . . . . . . 12
β’ (π£ β (π« π β© Fin) β π£ β π) |
53 | 52 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((π β (Metβπ) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)π) = π)) β π£ β π) |
54 | | ssrexv 4012 |
. . . . . . . . . . 11
β’ (π£ β π β (βπ₯ β π£ π = (π₯(ballβπ)π) β βπ₯ β π π = (π₯(ballβπ)π))) |
55 | 53, 54 | syl 17 |
. . . . . . . . . 10
β’ ((π β (Metβπ) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)π) = π)) β (βπ₯ β π£ π = (π₯(ballβπ)π) β βπ₯ β π π = (π₯(ballβπ)π))) |
56 | 55 | ss2abdv 4021 |
. . . . . . . . 9
β’ ((π β (Metβπ) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)π) = π)) β {π β£ βπ₯ β π£ π = (π₯(ballβπ)π)} β {π β£ βπ₯ β π π = (π₯(ballβπ)π)}) |
57 | 51, 56 | eqsstrid 3993 |
. . . . . . . 8
β’ ((π β (Metβπ) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)π) = π)) β ran (π₯ β π£ β¦ (π₯(ballβπ)π)) β {π β£ βπ₯ β π π = (π₯(ballβπ)π)}) |
58 | | unieq 4877 |
. . . . . . . . . . 11
β’ (π€ = ran (π₯ β π£ β¦ (π₯(ballβπ)π)) β βͺ π€ = βͺ
ran (π₯ β π£ β¦ (π₯(ballβπ)π))) |
59 | 58 | eqeq1d 2735 |
. . . . . . . . . 10
β’ (π€ = ran (π₯ β π£ β¦ (π₯(ballβπ)π)) β (βͺ π€ = π β βͺ ran
(π₯ β π£ β¦ (π₯(ballβπ)π)) = π)) |
60 | | ssabral 4020 |
. . . . . . . . . . 11
β’ (π€ β {π β£ βπ₯ β π π = (π₯(ballβπ)π)} β βπ β π€ βπ₯ β π π = (π₯(ballβπ)π)) |
61 | | sseq1 3970 |
. . . . . . . . . . 11
β’ (π€ = ran (π₯ β π£ β¦ (π₯(ballβπ)π)) β (π€ β {π β£ βπ₯ β π π = (π₯(ballβπ)π)} β ran (π₯ β π£ β¦ (π₯(ballβπ)π)) β {π β£ βπ₯ β π π = (π₯(ballβπ)π)})) |
62 | 60, 61 | bitr3id 285 |
. . . . . . . . . 10
β’ (π€ = ran (π₯ β π£ β¦ (π₯(ballβπ)π)) β (βπ β π€ βπ₯ β π π = (π₯(ballβπ)π) β ran (π₯ β π£ β¦ (π₯(ballβπ)π)) β {π β£ βπ₯ β π π = (π₯(ballβπ)π)})) |
63 | 59, 62 | anbi12d 632 |
. . . . . . . . 9
β’ (π€ = ran (π₯ β π£ β¦ (π₯(ballβπ)π)) β ((βͺ
π€ = π β§ βπ β π€ βπ₯ β π π = (π₯(ballβπ)π)) β (βͺ ran
(π₯ β π£ β¦ (π₯(ballβπ)π)) = π β§ ran (π₯ β π£ β¦ (π₯(ballβπ)π)) β {π β£ βπ₯ β π π = (π₯(ballβπ)π)}))) |
64 | 63 | rspcev 3580 |
. . . . . . . 8
β’ ((ran
(π₯ β π£ β¦ (π₯(ballβπ)π)) β Fin β§ (βͺ ran (π₯ β π£ β¦ (π₯(ballβπ)π)) = π β§ ran (π₯ β π£ β¦ (π₯(ballβπ)π)) β {π β£ βπ₯ β π π = (π₯(ballβπ)π)})) β βπ€ β Fin (βͺ
π€ = π β§ βπ β π€ βπ₯ β π π = (π₯(ballβπ)π))) |
65 | 45, 49, 57, 64 | syl12anc 836 |
. . . . . . 7
β’ ((π β (Metβπ) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)π) = π)) β βπ€ β Fin (βͺ
π€ = π β§ βπ β π€ βπ₯ β π π = (π₯(ballβπ)π))) |
66 | 65 | expr 458 |
. . . . . 6
β’ ((π β (Metβπ) β§ π£ β (π« π β© Fin)) β (βͺ π₯ β π£ (π₯(ballβπ)π) = π β βπ€ β Fin (βͺ
π€ = π β§ βπ β π€ βπ₯ β π π = (π₯(ballβπ)π)))) |
67 | 66 | rexlimdva 3149 |
. . . . 5
β’ (π β (Metβπ) β (βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π β βπ€ β Fin (βͺ
π€ = π β§ βπ β π€ βπ₯ β π π = (π₯(ballβπ)π)))) |
68 | 39, 67 | impbid 211 |
. . . 4
β’ (π β (Metβπ) β (βπ€ β Fin (βͺ π€ =
π β§ βπ β π€ βπ₯ β π π = (π₯(ballβπ)π)) β βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π)) |
69 | 68 | ralbidv 3171 |
. . 3
β’ (π β (Metβπ) β (βπ β β+
βπ€ β Fin (βͺ π€ =
π β§ βπ β π€ βπ₯ β π π = (π₯(ballβπ)π)) β βπ β β+ βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π)) |
70 | 69 | pm5.32i 576 |
. 2
β’ ((π β (Metβπ) β§ βπ β β+
βπ€ β Fin (βͺ π€ =
π β§ βπ β π€ βπ₯ β π π = (π₯(ballβπ)π))) β (π β (Metβπ) β§ βπ β β+ βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π)) |
71 | 1, 70 | bitri 275 |
1
β’ (π β (TotBndβπ) β (π β (Metβπ) β§ βπ β β+ βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π)) |