Step | Hyp | Ref
| Expression |
1 | | smflimsuplem5.a |
. . 3
|
2 | | smflimsuplem5.n |
. . . . . . . 8
|
3 | | smflimsuplem5.z |
. . . . . . . . . . . 12
|
4 | 3 | eleq2i 2693 |
. . . . . . . . . . 11
|
5 | 4 | biimpi 206 |
. . . . . . . . . 10
|
6 | | uzss 11708 |
. . . . . . . . . 10
|
7 | 5, 6 | syl 17 |
. . . . . . . . 9
|
8 | 7, 3 | syl6sseqr 3652 |
. . . . . . . 8
|
9 | 2, 8 | syl 17 |
. . . . . . 7
|
10 | 9 | sselda 3603 |
. . . . . 6
|
11 | | smflimsuplem5.e |
. . . . . . . . . 10
|
12 | | nfcv 2764 |
. . . . . . . . . . 11
|
13 | | nfrab1 3122 |
. . . . . . . . . . 11
|
14 | 12, 13 | nfmpt 4746 |
. . . . . . . . . 10
|
15 | 11, 14 | nfcxfr 2762 |
. . . . . . . . 9
|
16 | | nfcv 2764 |
. . . . . . . . 9
|
17 | 15, 16 | nffv 6198 |
. . . . . . . 8
|
18 | | fvex 6201 |
. . . . . . . 8
|
19 | 17, 18 | mptexf 39444 |
. . . . . . 7
|
20 | 19 | a1i 11 |
. . . . . 6
|
21 | | smflimsuplem5.h |
. . . . . . 7
|
22 | 21 | fvmpt2 6291 |
. . . . . 6
|
23 | 10, 20, 22 | syl2anc 693 |
. . . . 5
|
24 | 23 | fveq1d 6193 |
. . . 4
|
25 | | nfcv 2764 |
. . . . . 6
|
26 | | nfcv 2764 |
. . . . . 6
|
27 | | nfcv 2764 |
. . . . . 6
|
28 | | fveq2 6191 |
. . . . . . . . 9
|
29 | 28 | mpteq2dv 4745 |
. . . . . . . 8
|
30 | 29 | rneqd 5353 |
. . . . . . 7
|
31 | 30 | supeq1d 8352 |
. . . . . 6
|
32 | 17, 25, 26, 27, 31 | cbvmptf 4748 |
. . . . 5
|
33 | | simpl 473 |
. . . . . . . . 9
|
34 | 33 | fveq2d 6195 |
. . . . . . . 8
|
35 | 34 | mpteq2dva 4744 |
. . . . . . 7
|
36 | 35 | rneqd 5353 |
. . . . . 6
|
37 | 36 | supeq1d 8352 |
. . . . 5
|
38 | 37 | eleq1d 2686 |
. . . . . . . 8
|
39 | | uzss 11708 |
. . . . . . . . . . 11
|
40 | | iinss1 4533 |
. . . . . . . . . . 11
|
41 | 39, 40 | syl 17 |
. . . . . . . . . 10
|
42 | 41 | adantl 482 |
. . . . . . . . 9
|
43 | | smflimsuplem5.x |
. . . . . . . . . 10
|
44 | 43 | adantr 481 |
. . . . . . . . 9
|
45 | 42, 44 | sseldd 3604 |
. . . . . . . 8
|
46 | | smflimsuplem5.b |
. . . . . . . . . . 11
|
47 | | nfv 1843 |
. . . . . . . . . . 11
|
48 | 46, 47 | nfan 1828 |
. . . . . . . . . 10
|
49 | | eqid 2622 |
. . . . . . . . . 10
|
50 | | simpll 790 |
. . . . . . . . . . 11
|
51 | 39 | sselda 3603 |
. . . . . . . . . . . 12
|
52 | 51 | adantll 750 |
. . . . . . . . . . 11
|
53 | | smflimsuplem5.s |
. . . . . . . . . . . . . 14
SAlg |
54 | 53 | adantr 481 |
. . . . . . . . . . . . 13
SAlg |
55 | | simpl 473 |
. . . . . . . . . . . . . 14
|
56 | 9 | sselda 3603 |
. . . . . . . . . . . . . 14
|
57 | | smflimsuplem5.f |
. . . . . . . . . . . . . . 15
SMblFn |
58 | 57 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
SMblFn |
59 | 55, 56, 58 | syl2anc 693 |
. . . . . . . . . . . . 13
SMblFn |
60 | | eqid 2622 |
. . . . . . . . . . . . 13
|
61 | 54, 59, 60 | smff 40941 |
. . . . . . . . . . . 12
|
62 | | eliin 4525 |
. . . . . . . . . . . . . . . 16
|
63 | 43, 62 | syl 17 |
. . . . . . . . . . . . . . 15
|
64 | 43, 63 | mpbid 222 |
. . . . . . . . . . . . . 14
|
65 | 64 | adantr 481 |
. . . . . . . . . . . . 13
|
66 | | simpr 477 |
. . . . . . . . . . . . 13
|
67 | | rspa 2930 |
. . . . . . . . . . . . 13
|
68 | 65, 66, 67 | syl2anc 693 |
. . . . . . . . . . . 12
|
69 | 61, 68 | ffvelrnd 6360 |
. . . . . . . . . . 11
|
70 | 50, 52, 69 | syl2anc 693 |
. . . . . . . . . 10
|
71 | | eluzelz 11697 |
. . . . . . . . . . . . . 14
|
72 | 71 | adantl 482 |
. . . . . . . . . . . . 13
|
73 | | smflimsuplem5.m |
. . . . . . . . . . . . . 14
|
74 | 73 | adantr 481 |
. . . . . . . . . . . . 13
|
75 | | fvex 6201 |
. . . . . . . . . . . . . 14
|
76 | 75 | a1i 11 |
. . . . . . . . . . . . 13
|
77 | 48, 72, 74, 49, 3, 70, 76 | limsupequzmpt 39961 |
. . . . . . . . . . . 12
|
78 | | smflimsuplem5.r |
. . . . . . . . . . . . 13
|
79 | 78 | adantr 481 |
. . . . . . . . . . . 12
|
80 | 77, 79 | eqeltrd 2701 |
. . . . . . . . . . 11
|
81 | 80 | renepnfd 10090 |
. . . . . . . . . 10
|
82 | 48, 49, 70, 81 | limsupubuzmpt 39951 |
. . . . . . . . 9
|
83 | | uzid2 39630 |
. . . . . . . . . . . 12
|
84 | | ne0i 3921 |
. . . . . . . . . . . 12
|
85 | 83, 84 | syl 17 |
. . . . . . . . . . 11
|
86 | 85 | adantl 482 |
. . . . . . . . . 10
|
87 | 48, 86, 70 | supxrre3rnmpt 39656 |
. . . . . . . . 9
|
88 | 82, 87 | mpbird 247 |
. . . . . . . 8
|
89 | 38, 45, 88 | elrabd 3365 |
. . . . . . 7
|
90 | | simpl 473 |
. . . . . . . . . . . . 13
|
91 | 90 | fveq2d 6195 |
. . . . . . . . . . . 12
|
92 | 91 | mpteq2dva 4744 |
. . . . . . . . . . 11
|
93 | 92 | rneqd 5353 |
. . . . . . . . . 10
|
94 | 93 | supeq1d 8352 |
. . . . . . . . 9
|
95 | 94 | eleq1d 2686 |
. . . . . . . 8
|
96 | 95 | cbvrabv 3199 |
. . . . . . 7
|
97 | 89, 96 | syl6eleq 2711 |
. . . . . 6
|
98 | | eqid 2622 |
. . . . . . . 8
|
99 | | fvex 6201 |
. . . . . . . . . . . . 13
|
100 | 99 | dmex 7099 |
. . . . . . . . . . . 12
|
101 | 100 | rgenw 2924 |
. . . . . . . . . . 11
|
102 | 101 | a1i 11 |
. . . . . . . . . 10
|
103 | 85, 102 | iinexd 39318 |
. . . . . . . . 9
|
104 | 103 | adantl 482 |
. . . . . . . 8
|
105 | 98, 104 | rabexd 4814 |
. . . . . . 7
|
106 | 11 | fvmpt2 6291 |
. . . . . . 7
|
107 | 10, 105, 106 | syl2anc 693 |
. . . . . 6
|
108 | 97, 107 | eleqtrrd 2704 |
. . . . 5
|
109 | 88 | elexd 3214 |
. . . . 5
|
110 | 32, 37, 108, 109 | fvmptd3 39447 |
. . . 4
|
111 | 24, 110 | eqtrd 2656 |
. . 3
|
112 | 1, 111 | mpteq2da 4743 |
. 2
|
113 | 3 | eluzelz2 39627 |
. . . 4
|
114 | 2, 113 | syl 17 |
. . 3
|
115 | | eqid 2622 |
. . 3
|
116 | 75 | a1i 11 |
. . . . 5
|
117 | 75 | a1i 11 |
. . . . 5
|
118 | 46, 114, 73, 115, 3, 116, 117 | limsupequzmpt 39961 |
. . . 4
|
119 | 118, 78 | eqeltrd 2701 |
. . 3
|
120 | 46, 114, 115, 69, 119 | supcnvlimsupmpt 39973 |
. 2
|
121 | 112, 120 | eqbrtrd 4675 |
1
|