Step | Hyp | Ref
| Expression |
1 | | sstotbnd.2 |
. . 3
β’ π = (π βΎ (π Γ π)) |
2 | 1 | sstotbnd2 36262 |
. 2
β’ ((π β (Metβπ) β§ π β π) β (π β (TotBndβπ) β βπ β β+ βπ’ β (π« π β© Fin)π β βͺ
π₯ β π’ (π₯(ballβπ)π))) |
3 | | elfpw 9305 |
. . . . . . . . 9
β’ (π’ β (π« π β© Fin) β (π’ β π β§ π’ β Fin)) |
4 | 3 | simprbi 498 |
. . . . . . . 8
β’ (π’ β (π« π β© Fin) β π’ β Fin) |
5 | | mptfi 9302 |
. . . . . . . 8
β’ (π’ β Fin β (π₯ β π’ β¦ (π₯(ballβπ)π)) β Fin) |
6 | | rnfi 9286 |
. . . . . . . 8
β’ ((π₯ β π’ β¦ (π₯(ballβπ)π)) β Fin β ran (π₯ β π’ β¦ (π₯(ballβπ)π)) β Fin) |
7 | 4, 5, 6 | 3syl 18 |
. . . . . . 7
β’ (π’ β (π« π β© Fin) β ran (π₯ β π’ β¦ (π₯(ballβπ)π)) β Fin) |
8 | 7 | ad2antrl 727 |
. . . . . 6
β’ (((π β (Metβπ) β§ π β π) β§ (π’ β (π« π β© Fin) β§ π β βͺ
π₯ β π’ (π₯(ballβπ)π))) β ran (π₯ β π’ β¦ (π₯(ballβπ)π)) β Fin) |
9 | | simprr 772 |
. . . . . 6
β’ (((π β (Metβπ) β§ π β π) β§ (π’ β (π« π β© Fin) β§ π β βͺ
π₯ β π’ (π₯(ballβπ)π))) β π β βͺ
π₯ β π’ (π₯(ballβπ)π)) |
10 | | eqid 2737 |
. . . . . . . 8
β’ (π₯ β π’ β¦ (π₯(ballβπ)π)) = (π₯ β π’ β¦ (π₯(ballβπ)π)) |
11 | 10 | rnmpt 5915 |
. . . . . . 7
β’ ran
(π₯ β π’ β¦ (π₯(ballβπ)π)) = {π β£ βπ₯ β π’ π = (π₯(ballβπ)π)} |
12 | 3 | simplbi 499 |
. . . . . . . . . 10
β’ (π’ β (π« π β© Fin) β π’ β π) |
13 | | ssrexv 4016 |
. . . . . . . . . 10
β’ (π’ β π β (βπ₯ β π’ π = (π₯(ballβπ)π) β βπ₯ β π π = (π₯(ballβπ)π))) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
β’ (π’ β (π« π β© Fin) β (βπ₯ β π’ π = (π₯(ballβπ)π) β βπ₯ β π π = (π₯(ballβπ)π))) |
15 | 14 | ad2antrl 727 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ π β π) β§ (π’ β (π« π β© Fin) β§ π β βͺ
π₯ β π’ (π₯(ballβπ)π))) β (βπ₯ β π’ π = (π₯(ballβπ)π) β βπ₯ β π π = (π₯(ballβπ)π))) |
16 | 15 | ss2abdv 4025 |
. . . . . . 7
β’ (((π β (Metβπ) β§ π β π) β§ (π’ β (π« π β© Fin) β§ π β βͺ
π₯ β π’ (π₯(ballβπ)π))) β {π β£ βπ₯ β π’ π = (π₯(ballβπ)π)} β {π β£ βπ₯ β π π = (π₯(ballβπ)π)}) |
17 | 11, 16 | eqsstrid 3997 |
. . . . . 6
β’ (((π β (Metβπ) β§ π β π) β§ (π’ β (π« π β© Fin) β§ π β βͺ
π₯ β π’ (π₯(ballβπ)π))) β ran (π₯ β π’ β¦ (π₯(ballβπ)π)) β {π β£ βπ₯ β π π = (π₯(ballβπ)π)}) |
18 | | unieq 4881 |
. . . . . . . . . 10
β’ (π£ = ran (π₯ β π’ β¦ (π₯(ballβπ)π)) β βͺ π£ = βͺ
ran (π₯ β π’ β¦ (π₯(ballβπ)π))) |
19 | | ovex 7395 |
. . . . . . . . . . 11
β’ (π₯(ballβπ)π) β V |
20 | 19 | dfiun3 5926 |
. . . . . . . . . 10
β’ βͺ π₯ β π’ (π₯(ballβπ)π) = βͺ ran (π₯ β π’ β¦ (π₯(ballβπ)π)) |
21 | 18, 20 | eqtr4di 2795 |
. . . . . . . . 9
β’ (π£ = ran (π₯ β π’ β¦ (π₯(ballβπ)π)) β βͺ π£ = βͺ π₯ β π’ (π₯(ballβπ)π)) |
22 | 21 | sseq2d 3981 |
. . . . . . . 8
β’ (π£ = ran (π₯ β π’ β¦ (π₯(ballβπ)π)) β (π β βͺ π£ β π β βͺ
π₯ β π’ (π₯(ballβπ)π))) |
23 | | ssabral 4024 |
. . . . . . . . 9
β’ (π£ β {π β£ βπ₯ β π π = (π₯(ballβπ)π)} β βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)) |
24 | | sseq1 3974 |
. . . . . . . . 9
β’ (π£ = ran (π₯ β π’ β¦ (π₯(ballβπ)π)) β (π£ β {π β£ βπ₯ β π π = (π₯(ballβπ)π)} β ran (π₯ β π’ β¦ (π₯(ballβπ)π)) β {π β£ βπ₯ β π π = (π₯(ballβπ)π)})) |
25 | 23, 24 | bitr3id 285 |
. . . . . . . 8
β’ (π£ = ran (π₯ β π’ β¦ (π₯(ballβπ)π)) β (βπ β π£ βπ₯ β π π = (π₯(ballβπ)π) β ran (π₯ β π’ β¦ (π₯(ballβπ)π)) β {π β£ βπ₯ β π π = (π₯(ballβπ)π)})) |
26 | 22, 25 | anbi12d 632 |
. . . . . . 7
β’ (π£ = ran (π₯ β π’ β¦ (π₯(ballβπ)π)) β ((π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)) β (π β βͺ
π₯ β π’ (π₯(ballβπ)π) β§ ran (π₯ β π’ β¦ (π₯(ballβπ)π)) β {π β£ βπ₯ β π π = (π₯(ballβπ)π)}))) |
27 | 26 | rspcev 3584 |
. . . . . 6
β’ ((ran
(π₯ β π’ β¦ (π₯(ballβπ)π)) β Fin β§ (π β βͺ
π₯ β π’ (π₯(ballβπ)π) β§ ran (π₯ β π’ β¦ (π₯(ballβπ)π)) β {π β£ βπ₯ β π π = (π₯(ballβπ)π)})) β βπ£ β Fin (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π))) |
28 | 8, 9, 17, 27 | syl12anc 836 |
. . . . 5
β’ (((π β (Metβπ) β§ π β π) β§ (π’ β (π« π β© Fin) β§ π β βͺ
π₯ β π’ (π₯(ballβπ)π))) β βπ£ β Fin (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π))) |
29 | 28 | rexlimdvaa 3154 |
. . . 4
β’ ((π β (Metβπ) β§ π β π) β (βπ’ β (π« π β© Fin)π β βͺ
π₯ β π’ (π₯(ballβπ)π) β βπ£ β Fin (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) |
30 | | oveq1 7369 |
. . . . . . . . . 10
β’ (π₯ = (πβπ) β (π₯(ballβπ)π) = ((πβπ)(ballβπ)π)) |
31 | 30 | eqeq2d 2748 |
. . . . . . . . 9
β’ (π₯ = (πβπ) β (π = (π₯(ballβπ)π) β π = ((πβπ)(ballβπ)π))) |
32 | 31 | ac6sfi 9238 |
. . . . . . . 8
β’ ((π£ β Fin β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)) β βπ(π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) |
33 | 32 | adantrl 715 |
. . . . . . 7
β’ ((π£ β Fin β§ (π β βͺ π£
β§ βπ β
π£ βπ₯ β π π = (π₯(ballβπ)π))) β βπ(π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) |
34 | 33 | adantl 483 |
. . . . . 6
β’ (((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β βπ(π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) |
35 | | frn 6680 |
. . . . . . . . 9
β’ (π:π£βΆπ β ran π β π) |
36 | 35 | ad2antrl 727 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β§ (π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) β ran π β π) |
37 | | simplrl 776 |
. . . . . . . . 9
β’ ((((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β§ (π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) β π£ β Fin) |
38 | | ffn 6673 |
. . . . . . . . . . 11
β’ (π:π£βΆπ β π Fn π£) |
39 | 38 | ad2antrl 727 |
. . . . . . . . . 10
β’ ((((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β§ (π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) β π Fn π£) |
40 | | dffn4 6767 |
. . . . . . . . . 10
β’ (π Fn π£ β π:π£βontoβran π) |
41 | 39, 40 | sylib 217 |
. . . . . . . . 9
β’ ((((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β§ (π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) β π:π£βontoβran π) |
42 | | fofi 9289 |
. . . . . . . . 9
β’ ((π£ β Fin β§ π:π£βontoβran π) β ran π β Fin) |
43 | 37, 41, 42 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β§ (π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) β ran π β Fin) |
44 | | elfpw 9305 |
. . . . . . . 8
β’ (ran
π β (π« π β© Fin) β (ran π β π β§ ran π β Fin)) |
45 | 36, 43, 44 | sylanbrc 584 |
. . . . . . 7
β’ ((((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β§ (π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) β ran π β (π« π β© Fin)) |
46 | | simprrl 780 |
. . . . . . . . . 10
β’ (((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β π β βͺ π£) |
47 | 46 | adantr 482 |
. . . . . . . . 9
β’ ((((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β§ (π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) β π β βͺ π£) |
48 | | uniiun 5023 |
. . . . . . . . . . 11
β’ βͺ π£ =
βͺ π β π£ π |
49 | | iuneq2 4978 |
. . . . . . . . . . 11
β’
(βπ β
π£ π = ((πβπ)(ballβπ)π) β βͺ
π β π£ π = βͺ π β π£ ((πβπ)(ballβπ)π)) |
50 | 48, 49 | eqtrid 2789 |
. . . . . . . . . 10
β’
(βπ β
π£ π = ((πβπ)(ballβπ)π) β βͺ π£ = βͺ π β π£ ((πβπ)(ballβπ)π)) |
51 | 50 | ad2antll 728 |
. . . . . . . . 9
β’ ((((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β§ (π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) β βͺ π£ = βͺ π β π£ ((πβπ)(ballβπ)π)) |
52 | 47, 51 | sseqtrd 3989 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β§ (π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) β π β βͺ
π β π£ ((πβπ)(ballβπ)π)) |
53 | 30 | eleq2d 2824 |
. . . . . . . . . . . 12
β’ (π₯ = (πβπ) β (π¦ β (π₯(ballβπ)π) β π¦ β ((πβπ)(ballβπ)π))) |
54 | 53 | rexrn 7042 |
. . . . . . . . . . 11
β’ (π Fn π£ β (βπ₯ β ran π π¦ β (π₯(ballβπ)π) β βπ β π£ π¦ β ((πβπ)(ballβπ)π))) |
55 | | eliun 4963 |
. . . . . . . . . . 11
β’ (π¦ β βͺ π₯ β ran π(π₯(ballβπ)π) β βπ₯ β ran π π¦ β (π₯(ballβπ)π)) |
56 | | eliun 4963 |
. . . . . . . . . . 11
β’ (π¦ β βͺ π β π£ ((πβπ)(ballβπ)π) β βπ β π£ π¦ β ((πβπ)(ballβπ)π)) |
57 | 54, 55, 56 | 3bitr4g 314 |
. . . . . . . . . 10
β’ (π Fn π£ β (π¦ β βͺ
π₯ β ran π(π₯(ballβπ)π) β π¦ β βͺ
π β π£ ((πβπ)(ballβπ)π))) |
58 | 57 | eqrdv 2735 |
. . . . . . . . 9
β’ (π Fn π£ β βͺ
π₯ β ran π(π₯(ballβπ)π) = βͺ π β π£ ((πβπ)(ballβπ)π)) |
59 | 39, 58 | syl 17 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β§ (π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) β βͺ π₯ β ran π(π₯(ballβπ)π) = βͺ π β π£ ((πβπ)(ballβπ)π)) |
60 | 52, 59 | sseqtrrd 3990 |
. . . . . . 7
β’ ((((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β§ (π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) β π β βͺ
π₯ β ran π(π₯(ballβπ)π)) |
61 | | iuneq1 4975 |
. . . . . . . . 9
β’ (π’ = ran π β βͺ
π₯ β π’ (π₯(ballβπ)π) = βͺ π₯ β ran π(π₯(ballβπ)π)) |
62 | 61 | sseq2d 3981 |
. . . . . . . 8
β’ (π’ = ran π β (π β βͺ
π₯ β π’ (π₯(ballβπ)π) β π β βͺ
π₯ β ran π(π₯(ballβπ)π))) |
63 | 62 | rspcev 3584 |
. . . . . . 7
β’ ((ran
π β (π« π β© Fin) β§ π β βͺ π₯ β ran π(π₯(ballβπ)π)) β βπ’ β (π« π β© Fin)π β βͺ
π₯ β π’ (π₯(ballβπ)π)) |
64 | 45, 60, 63 | syl2anc 585 |
. . . . . 6
β’ ((((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β§ (π:π£βΆπ β§ βπ β π£ π = ((πβπ)(ballβπ)π))) β βπ’ β (π« π β© Fin)π β βͺ
π₯ β π’ (π₯(ballβπ)π)) |
65 | 34, 64 | exlimddv 1939 |
. . . . 5
β’ (((π β (Metβπ) β§ π β π) β§ (π£ β Fin β§ (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) β βπ’ β (π« π β© Fin)π β βͺ
π₯ β π’ (π₯(ballβπ)π)) |
66 | 65 | rexlimdvaa 3154 |
. . . 4
β’ ((π β (Metβπ) β§ π β π) β (βπ£ β Fin (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)) β βπ’ β (π« π β© Fin)π β βͺ
π₯ β π’ (π₯(ballβπ)π))) |
67 | 29, 66 | impbid 211 |
. . 3
β’ ((π β (Metβπ) β§ π β π) β (βπ’ β (π« π β© Fin)π β βͺ
π₯ β π’ (π₯(ballβπ)π) β βπ£ β Fin (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) |
68 | 67 | ralbidv 3175 |
. 2
β’ ((π β (Metβπ) β§ π β π) β (βπ β β+ βπ’ β (π« π β© Fin)π β βͺ
π₯ β π’ (π₯(ballβπ)π) β βπ β β+ βπ£ β Fin (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) |
69 | 2, 68 | bitrd 279 |
1
β’ ((π β (Metβπ) β§ π β π) β (π β (TotBndβπ) β βπ β β+ βπ£ β Fin (π β βͺ π£ β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) |