Step | Hyp | Ref
| Expression |
1 | | metust.1 |
. . . 4
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) |
2 | 1 | metustfbas 23936 |
. . 3
β’ ((π β β
β§ π· β (PsMetβπ)) β πΉ β (fBasβ(π Γ π))) |
3 | | fgcl 23252 |
. . 3
β’ (πΉ β (fBasβ(π Γ π)) β ((π Γ π)filGenπΉ) β (Filβ(π Γ π))) |
4 | | filsspw 23225 |
. . 3
β’ (((π Γ π)filGenπΉ) β (Filβ(π Γ π)) β ((π Γ π)filGenπΉ) β π« (π Γ π)) |
5 | 2, 3, 4 | 3syl 18 |
. 2
β’ ((π β β
β§ π· β (PsMetβπ)) β ((π Γ π)filGenπΉ) β π« (π Γ π)) |
6 | | filtop 23229 |
. . 3
β’ (((π Γ π)filGenπΉ) β (Filβ(π Γ π)) β (π Γ π) β ((π Γ π)filGenπΉ)) |
7 | 2, 3, 6 | 3syl 18 |
. 2
β’ ((π β β
β§ π· β (PsMetβπ)) β (π Γ π) β ((π Γ π)filGenπΉ)) |
8 | 2, 3 | syl 17 |
. . . . . . . 8
β’ ((π β β
β§ π· β (PsMetβπ)) β ((π Γ π)filGenπΉ) β (Filβ(π Γ π))) |
9 | 8 | ad3antrrr 729 |
. . . . . . 7
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π€ β π« (π Γ π)) β§ π£ β π€) β ((π Γ π)filGenπΉ) β (Filβ(π Γ π))) |
10 | | simpllr 775 |
. . . . . . 7
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π€ β π« (π Γ π)) β§ π£ β π€) β π£ β ((π Γ π)filGenπΉ)) |
11 | | simplr 768 |
. . . . . . . 8
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π€ β π« (π Γ π)) β§ π£ β π€) β π€ β π« (π Γ π)) |
12 | 11 | elpwid 4573 |
. . . . . . 7
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π€ β π« (π Γ π)) β§ π£ β π€) β π€ β (π Γ π)) |
13 | | simpr 486 |
. . . . . . 7
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π€ β π« (π Γ π)) β§ π£ β π€) β π£ β π€) |
14 | | filss 23227 |
. . . . . . 7
β’ ((((π Γ π)filGenπΉ) β (Filβ(π Γ π)) β§ (π£ β ((π Γ π)filGenπΉ) β§ π€ β (π Γ π) β§ π£ β π€)) β π€ β ((π Γ π)filGenπΉ)) |
15 | 9, 10, 12, 13, 14 | syl13anc 1373 |
. . . . . 6
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π€ β π« (π Γ π)) β§ π£ β π€) β π€ β ((π Γ π)filGenπΉ)) |
16 | 15 | ex 414 |
. . . . 5
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β§ π€ β π« (π Γ π)) β (π£ β π€ β π€ β ((π Γ π)filGenπΉ))) |
17 | 16 | ralrimiva 3140 |
. . . 4
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β βπ€ β π« (π Γ π)(π£ β π€ β π€ β ((π Γ π)filGenπΉ))) |
18 | 8 | ad2antrr 725 |
. . . . . 6
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β§ π€ β ((π Γ π)filGenπΉ)) β ((π Γ π)filGenπΉ) β (Filβ(π Γ π))) |
19 | | simplr 768 |
. . . . . 6
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β§ π€ β ((π Γ π)filGenπΉ)) β π£ β ((π Γ π)filGenπΉ)) |
20 | | simpr 486 |
. . . . . 6
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β§ π€ β ((π Γ π)filGenπΉ)) β π€ β ((π Γ π)filGenπΉ)) |
21 | | filin 23228 |
. . . . . 6
β’ ((((π Γ π)filGenπΉ) β (Filβ(π Γ π)) β§ π£ β ((π Γ π)filGenπΉ) β§ π€ β ((π Γ π)filGenπΉ)) β (π£ β© π€) β ((π Γ π)filGenπΉ)) |
22 | 18, 19, 20, 21 | syl3anc 1372 |
. . . . 5
β’ ((((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β§ π€ β ((π Γ π)filGenπΉ)) β (π£ β© π€) β ((π Γ π)filGenπΉ)) |
23 | 22 | ralrimiva 3140 |
. . . 4
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β βπ€ β ((π Γ π)filGenπΉ)(π£ β© π€) β ((π Γ π)filGenπΉ)) |
24 | 1 | metustid 23933 |
. . . . . . . 8
β’ ((π· β (PsMetβπ) β§ π’ β πΉ) β ( I βΎ π) β π’) |
25 | 24 | ad5ant24 760 |
. . . . . . 7
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β ( I βΎ π) β π’) |
26 | | simpr 486 |
. . . . . . 7
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β π’ β π£) |
27 | 25, 26 | sstrd 3958 |
. . . . . 6
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β ( I βΎ π) β π£) |
28 | | elfg 23245 |
. . . . . . . . 9
β’ (πΉ β (fBasβ(π Γ π)) β (π£ β ((π Γ π)filGenπΉ) β (π£ β (π Γ π) β§ βπ’ β πΉ π’ β π£))) |
29 | 28 | biimpa 478 |
. . . . . . . 8
β’ ((πΉ β (fBasβ(π Γ π)) β§ π£ β ((π Γ π)filGenπΉ)) β (π£ β (π Γ π) β§ βπ’ β πΉ π’ β π£)) |
30 | 29 | simprd 497 |
. . . . . . 7
β’ ((πΉ β (fBasβ(π Γ π)) β§ π£ β ((π Γ π)filGenπΉ)) β βπ’ β πΉ π’ β π£) |
31 | 2, 30 | sylan 581 |
. . . . . 6
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β βπ’ β πΉ π’ β π£) |
32 | 27, 31 | r19.29a 3156 |
. . . . 5
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β ( I βΎ π) β π£) |
33 | 8 | ad3antrrr 729 |
. . . . . . 7
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β ((π Γ π)filGenπΉ) β (Filβ(π Γ π))) |
34 | 2 | adantr 482 |
. . . . . . . . . 10
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β πΉ β (fBasβ(π Γ π))) |
35 | | ssfg 23246 |
. . . . . . . . . 10
β’ (πΉ β (fBasβ(π Γ π)) β πΉ β ((π Γ π)filGenπΉ)) |
36 | 34, 35 | syl 17 |
. . . . . . . . 9
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β πΉ β ((π Γ π)filGenπΉ)) |
37 | 36 | ad2antrr 725 |
. . . . . . . 8
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β πΉ β ((π Γ π)filGenπΉ)) |
38 | | simplr 768 |
. . . . . . . 8
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β π’ β πΉ) |
39 | 37, 38 | sseldd 3949 |
. . . . . . 7
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β π’ β ((π Γ π)filGenπΉ)) |
40 | 29 | simpld 496 |
. . . . . . . . . 10
β’ ((πΉ β (fBasβ(π Γ π)) β§ π£ β ((π Γ π)filGenπΉ)) β π£ β (π Γ π)) |
41 | 2, 40 | sylan 581 |
. . . . . . . . 9
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β π£ β (π Γ π)) |
42 | 41 | ad2antrr 725 |
. . . . . . . 8
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β π£ β (π Γ π)) |
43 | | cnvss 5832 |
. . . . . . . . 9
β’ (π£ β (π Γ π) β β‘π£ β β‘(π Γ π)) |
44 | | cnvxp 6113 |
. . . . . . . . 9
β’ β‘(π Γ π) = (π Γ π) |
45 | 43, 44 | sseqtrdi 3998 |
. . . . . . . 8
β’ (π£ β (π Γ π) β β‘π£ β (π Γ π)) |
46 | 42, 45 | syl 17 |
. . . . . . 7
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β β‘π£ β (π Γ π)) |
47 | 1 | metustsym 23934 |
. . . . . . . . 9
β’ ((π· β (PsMetβπ) β§ π’ β πΉ) β β‘π’ = π’) |
48 | 47 | ad5ant24 760 |
. . . . . . . 8
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β β‘π’ = π’) |
49 | | cnvss 5832 |
. . . . . . . . 9
β’ (π’ β π£ β β‘π’ β β‘π£) |
50 | 49 | adantl 483 |
. . . . . . . 8
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β β‘π’ β β‘π£) |
51 | 48, 50 | eqsstrrd 3987 |
. . . . . . 7
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β π’ β β‘π£) |
52 | | filss 23227 |
. . . . . . 7
β’ ((((π Γ π)filGenπΉ) β (Filβ(π Γ π)) β§ (π’ β ((π Γ π)filGenπΉ) β§ β‘π£ β (π Γ π) β§ π’ β β‘π£)) β β‘π£ β ((π Γ π)filGenπΉ)) |
53 | 33, 39, 46, 51, 52 | syl13anc 1373 |
. . . . . 6
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β β‘π£ β ((π Γ π)filGenπΉ)) |
54 | 53, 31 | r19.29a 3156 |
. . . . 5
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β β‘π£ β ((π Γ π)filGenπΉ)) |
55 | 1 | metustexhalf 23935 |
. . . . . . . . 9
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π’ β πΉ) β βπ€ β πΉ (π€ β π€) β π’) |
56 | 55 | ad4ant13 750 |
. . . . . . . 8
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β βπ€ β πΉ (π€ β π€) β π’) |
57 | | r19.41v 3182 |
. . . . . . . . 9
β’
(βπ€ β
πΉ ((π€ β π€) β π’ β§ π’ β π£) β (βπ€ β πΉ (π€ β π€) β π’ β§ π’ β π£)) |
58 | | sstr 3956 |
. . . . . . . . . 10
β’ (((π€ β π€) β π’ β§ π’ β π£) β (π€ β π€) β π£) |
59 | 58 | reximi 3084 |
. . . . . . . . 9
β’
(βπ€ β
πΉ ((π€ β π€) β π’ β§ π’ β π£) β βπ€ β πΉ (π€ β π€) β π£) |
60 | 57, 59 | sylbir 234 |
. . . . . . . 8
β’
((βπ€ β
πΉ (π€ β π€) β π’ β§ π’ β π£) β βπ€ β πΉ (π€ β π€) β π£) |
61 | 56, 60 | sylancom 589 |
. . . . . . 7
β’
(((((π β β
β§ π· β
(PsMetβπ)) β§
π£ β ((π Γ π)filGenπΉ)) β§ π’ β πΉ) β§ π’ β π£) β βπ€ β πΉ (π€ β π€) β π£) |
62 | 61, 31 | r19.29a 3156 |
. . . . . 6
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β βπ€ β πΉ (π€ β π€) β π£) |
63 | | ssrexv 4015 |
. . . . . 6
β’ (πΉ β ((π Γ π)filGenπΉ) β (βπ€ β πΉ (π€ β π€) β π£ β βπ€ β ((π Γ π)filGenπΉ)(π€ β π€) β π£)) |
64 | 36, 62, 63 | sylc 65 |
. . . . 5
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β βπ€ β ((π Γ π)filGenπΉ)(π€ β π€) β π£) |
65 | 32, 54, 64 | 3jca 1129 |
. . . 4
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β (( I βΎ π) β π£ β§ β‘π£ β ((π Γ π)filGenπΉ) β§ βπ€ β ((π Γ π)filGenπΉ)(π€ β π€) β π£)) |
66 | 17, 23, 65 | 3jca 1129 |
. . 3
β’ (((π β β
β§ π· β (PsMetβπ)) β§ π£ β ((π Γ π)filGenπΉ)) β (βπ€ β π« (π Γ π)(π£ β π€ β π€ β ((π Γ π)filGenπΉ)) β§ βπ€ β ((π Γ π)filGenπΉ)(π£ β© π€) β ((π Γ π)filGenπΉ) β§ (( I βΎ π) β π£ β§ β‘π£ β ((π Γ π)filGenπΉ) β§ βπ€ β ((π Γ π)filGenπΉ)(π€ β π€) β π£))) |
67 | 66 | ralrimiva 3140 |
. 2
β’ ((π β β
β§ π· β (PsMetβπ)) β βπ£ β ((π Γ π)filGenπΉ)(βπ€ β π« (π Γ π)(π£ β π€ β π€ β ((π Γ π)filGenπΉ)) β§ βπ€ β ((π Γ π)filGenπΉ)(π£ β© π€) β ((π Γ π)filGenπΉ) β§ (( I βΎ π) β π£ β§ β‘π£ β ((π Γ π)filGenπΉ) β§ βπ€ β ((π Γ π)filGenπΉ)(π€ β π€) β π£))) |
68 | | elfvex 6884 |
. . . 4
β’ (π· β (PsMetβπ) β π β V) |
69 | 68 | adantl 483 |
. . 3
β’ ((π β β
β§ π· β (PsMetβπ)) β π β V) |
70 | | isust 23578 |
. . 3
β’ (π β V β (((π Γ π)filGenπΉ) β (UnifOnβπ) β (((π Γ π)filGenπΉ) β π« (π Γ π) β§ (π Γ π) β ((π Γ π)filGenπΉ) β§ βπ£ β ((π Γ π)filGenπΉ)(βπ€ β π« (π Γ π)(π£ β π€ β π€ β ((π Γ π)filGenπΉ)) β§ βπ€ β ((π Γ π)filGenπΉ)(π£ β© π€) β ((π Γ π)filGenπΉ) β§ (( I βΎ π) β π£ β§ β‘π£ β ((π Γ π)filGenπΉ) β§ βπ€ β ((π Γ π)filGenπΉ)(π€ β π€) β π£))))) |
71 | 69, 70 | syl 17 |
. 2
β’ ((π β β
β§ π· β (PsMetβπ)) β (((π Γ π)filGenπΉ) β (UnifOnβπ) β (((π Γ π)filGenπΉ) β π« (π Γ π) β§ (π Γ π) β ((π Γ π)filGenπΉ) β§ βπ£ β ((π Γ π)filGenπΉ)(βπ€ β π« (π Γ π)(π£ β π€ β π€ β ((π Γ π)filGenπΉ)) β§ βπ€ β ((π Γ π)filGenπΉ)(π£ β© π€) β ((π Γ π)filGenπΉ) β§ (( I βΎ π) β π£ β§ β‘π£ β ((π Γ π)filGenπΉ) β§ βπ€ β ((π Γ π)filGenπΉ)(π€ β π€) β π£))))) |
72 | 5, 7, 67, 71 | mpbir3and 1343 |
1
β’ ((π β β
β§ π· β (PsMetβπ)) β ((π Γ π)filGenπΉ) β (UnifOnβπ)) |