Step | Hyp | Ref
| Expression |
1 | | metucn.u |
. . . . . 6
metUnif |
2 | | metucn.c |
. . . . . . 7
PsMet |
3 | | metuval 22354 |
. . . . . . 7
PsMet
metUnif |
4 | 2, 3 | syl 17 |
. . . . . 6
metUnif |
5 | 1, 4 | syl5eq 2668 |
. . . . 5
|
6 | | metucn.v |
. . . . . 6
metUnif |
7 | | metucn.d |
. . . . . . 7
PsMet |
8 | | metuval 22354 |
. . . . . . 7
PsMet
metUnif |
9 | 7, 8 | syl 17 |
. . . . . 6
metUnif |
10 | 6, 9 | syl5eq 2668 |
. . . . 5
|
11 | 5, 10 | oveq12d 6668 |
. . . 4
Cnu
Cnu |
12 | 11 | eleq2d 2687 |
. . 3
Cnu
Cnu |
13 | | eqid 2622 |
. . . 4
|
14 | | eqid 2622 |
. . . 4
|
15 | | metucn.x |
. . . . 5
|
16 | | oveq2 6658 |
. . . . . . . . 9
|
17 | 16 | imaeq2d 5466 |
. . . . . . . 8
|
18 | 17 | cbvmptv 4750 |
. . . . . . 7
|
19 | 18 | rneqi 5352 |
. . . . . 6
|
20 | 19 | metust 22363 |
. . . . 5
PsMet
UnifOn |
21 | 15, 2, 20 | syl2anc 693 |
. . . 4
UnifOn |
22 | | metucn.y |
. . . . 5
|
23 | | oveq2 6658 |
. . . . . . . . 9
|
24 | 23 | imaeq2d 5466 |
. . . . . . . 8
|
25 | 24 | cbvmptv 4750 |
. . . . . . 7
|
26 | 25 | rneqi 5352 |
. . . . . 6
|
27 | 26 | metust 22363 |
. . . . 5
PsMet
UnifOn |
28 | 22, 7, 27 | syl2anc 693 |
. . . 4
UnifOn |
29 | | oveq2 6658 |
. . . . . . . . 9
|
30 | 29 | imaeq2d 5466 |
. . . . . . . 8
|
31 | 30 | cbvmptv 4750 |
. . . . . . 7
|
32 | 31 | rneqi 5352 |
. . . . . 6
|
33 | 32 | metustfbas 22362 |
. . . . 5
PsMet
|
34 | 15, 2, 33 | syl2anc 693 |
. . . 4
|
35 | | oveq2 6658 |
. . . . . . . . 9
|
36 | 35 | imaeq2d 5466 |
. . . . . . . 8
|
37 | 36 | cbvmptv 4750 |
. . . . . . 7
|
38 | 37 | rneqi 5352 |
. . . . . 6
|
39 | 38 | metustfbas 22362 |
. . . . 5
PsMet
|
40 | 22, 7, 39 | syl2anc 693 |
. . . 4
|
41 | 13, 14, 21, 28, 34, 40 | isucn2 22083 |
. . 3
Cnu
|
42 | 12, 41 | bitrd 268 |
. 2
Cnu
|
43 | | eqid 2622 |
. . . . . . . . . 10
|
44 | | oveq2 6658 |
. . . . . . . . . . . . 13
|
45 | 44 | imaeq2d 5466 |
. . . . . . . . . . . 12
|
46 | 45 | eqeq2d 2632 |
. . . . . . . . . . 11
|
47 | 46 | rspcev 3309 |
. . . . . . . . . 10
|
48 | 43, 47 | mpan2 707 |
. . . . . . . . 9
|
49 | 48 | adantl 482 |
. . . . . . . 8
|
50 | 38 | metustel 22355 |
. . . . . . . . . 10
PsMet
|
51 | 7, 50 | syl 17 |
. . . . . . . . 9
|
52 | 51 | adantr 481 |
. . . . . . . 8
|
53 | 49, 52 | mpbird 247 |
. . . . . . 7
|
54 | 26 | metustel 22355 |
. . . . . . . 8
PsMet
|
55 | 7, 54 | syl 17 |
. . . . . . 7
|
56 | | simpr 477 |
. . . . . . . . . . 11
|
57 | 56 | breqd 4664 |
. . . . . . . . . 10
|
58 | 57 | imbi2d 330 |
. . . . . . . . 9
|
59 | 58 | ralbidv 2986 |
. . . . . . . 8
|
60 | 59 | rexralbidv 3058 |
. . . . . . 7
|
61 | 53, 55, 60 | ralxfr2d 4882 |
. . . . . 6
|
62 | | eqid 2622 |
. . . . . . . . . . 11
|
63 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
64 | 63 | imaeq2d 5466 |
. . . . . . . . . . . . 13
|
65 | 64 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
66 | 65 | rspcev 3309 |
. . . . . . . . . . 11
|
67 | 62, 66 | mpan2 707 |
. . . . . . . . . 10
|
68 | 67 | adantl 482 |
. . . . . . . . 9
|
69 | 32 | metustel 22355 |
. . . . . . . . . . 11
PsMet
|
70 | 2, 69 | syl 17 |
. . . . . . . . . 10
|
71 | 70 | adantr 481 |
. . . . . . . . 9
|
72 | 68, 71 | mpbird 247 |
. . . . . . . 8
|
73 | 19 | metustel 22355 |
. . . . . . . . 9
PsMet
|
74 | 2, 73 | syl 17 |
. . . . . . . 8
|
75 | | simpr 477 |
. . . . . . . . . . 11
|
76 | 75 | breqd 4664 |
. . . . . . . . . 10
|
77 | 76 | imbi1d 331 |
. . . . . . . . 9
|
78 | 77 | 2ralbidv 2989 |
. . . . . . . 8
|
79 | 72, 74, 78 | rexxfr2d 4883 |
. . . . . . 7
|
80 | 79 | ralbidv 2986 |
. . . . . 6
|
81 | 61, 80 | bitrd 268 |
. . . . 5
|
82 | 81 | adantr 481 |
. . . 4
|
83 | 2 | ad4antr 768 |
. . . . . . . . 9
PsMet |
84 | | simplr 792 |
. . . . . . . . 9
|
85 | | simprr 796 |
. . . . . . . . 9
|
86 | | simprl 794 |
. . . . . . . . 9
|
87 | | elbl4 22368 |
. . . . . . . . . 10
PsMet
|
88 | | rpxr 11840 |
. . . . . . . . . . 11
|
89 | | elbl3ps 22196 |
. . . . . . . . . . 11
PsMet
|
90 | 88, 89 | sylanl2 683 |
. . . . . . . . . 10
PsMet
|
91 | 87, 90 | bitr3d 270 |
. . . . . . . . 9
PsMet
|
92 | 83, 84, 85, 86, 91 | syl22anc 1327 |
. . . . . . . 8
|
93 | 7 | ad4antr 768 |
. . . . . . . . 9
PsMet |
94 | | simpllr 799 |
. . . . . . . . 9
|
95 | | simp-4r 807 |
. . . . . . . . . 10
|
96 | 95, 85 | ffvelrnd 6360 |
. . . . . . . . 9
|
97 | 95, 86 | ffvelrnd 6360 |
. . . . . . . . 9
|
98 | | elbl4 22368 |
. . . . . . . . . 10
PsMet |
99 | | rpxr 11840 |
. . . . . . . . . . 11
|
100 | | elbl3ps 22196 |
. . . . . . . . . . 11
PsMet |
101 | 99, 100 | sylanl2 683 |
. . . . . . . . . 10
PsMet |
102 | 98, 101 | bitr3d 270 |
. . . . . . . . 9
PsMet |
103 | 93, 94, 96, 97, 102 | syl22anc 1327 |
. . . . . . . 8
|
104 | 92, 103 | imbi12d 334 |
. . . . . . 7
|
105 | 104 | 2ralbidva 2988 |
. . . . . 6
|
106 | 105 | rexbidva 3049 |
. . . . 5
|
107 | 106 | ralbidva 2985 |
. . . 4
|
108 | 82, 107 | bitrd 268 |
. . 3
|
109 | 108 | pm5.32da 673 |
. 2
|
110 | 42, 109 | bitrd 268 |
1
Cnu
|