Step | Hyp | Ref
| Expression |
1 | | mclsppslem.10 |
. . . 4
|
2 | | mclspps.l |
. . . . 5
mSubst |
3 | | mclspps.e |
. . . . 5
mEx |
4 | 2, 3 | msubf 31429 |
. . . 4
|
5 | 1, 4 | syl 17 |
. . 3
|
6 | | mclspps.1 |
. . . . . . . 8
mFS |
7 | | eqid 2622 |
. . . . . . . . 9
mAx mAx |
8 | | eqid 2622 |
. . . . . . . . 9
mStat mStat |
9 | 7, 8 | maxsta 31451 |
. . . . . . . 8
mFS mAx
mStat |
10 | 6, 9 | syl 17 |
. . . . . . 7
mAx mStat |
11 | | eqid 2622 |
. . . . . . . 8
mPreSt mPreSt |
12 | 11, 8 | mstapst 31444 |
. . . . . . 7
mStat mPreSt |
13 | 10, 12 | syl6ss 3615 |
. . . . . 6
mAx mPreSt |
14 | | mclsppslem.9 |
. . . . . 6
mAx |
15 | 13, 14 | sseldd 3604 |
. . . . 5
mPreSt |
16 | | mclspps.d |
. . . . . 6
mDV |
17 | 16, 3, 11 | elmpst 31433 |
. . . . 5
mPreSt
|
18 | 15, 17 | sylib 208 |
. . . 4
|
19 | 18 | simp3d 1075 |
. . 3
|
20 | 5, 19 | ffvelrnd 6360 |
. 2
|
21 | | fvco3 6275 |
. . . 4
|
22 | 5, 19, 21 | syl2anc 693 |
. . 3
|
23 | | mclspps.c |
. . . 4
mCls |
24 | | mclspps.2 |
. . . 4
|
25 | | mclspps.3 |
. . . 4
|
26 | | mclspps.v |
. . . 4
mVR |
27 | | mclspps.h |
. . . 4
mVH |
28 | | mclspps.w |
. . . 4
mVars |
29 | | mclspps.5 |
. . . . 5
|
30 | 2 | msubco 31428 |
. . . . 5
|
31 | 29, 1, 30 | syl2anc 693 |
. . . 4
|
32 | 2, 3 | msubf 31429 |
. . . . . . . . 9
|
33 | 29, 32 | syl 17 |
. . . . . . . 8
|
34 | | fco 6058 |
. . . . . . . 8
|
35 | 33, 5, 34 | syl2anc 693 |
. . . . . . 7
|
36 | | ffn 6045 |
. . . . . . 7
|
37 | 35, 36 | syl 17 |
. . . . . 6
|
38 | 37 | adantr 481 |
. . . . 5
|
39 | | mclsppslem.11 |
. . . . . . . . 9
|
40 | | ffun 6048 |
. . . . . . . . . . 11
|
41 | 5, 40 | syl 17 |
. . . . . . . . . 10
|
42 | 17 | simp2bi 1077 |
. . . . . . . . . . . . . 14
mPreSt
|
43 | 15, 42 | syl 17 |
. . . . . . . . . . . . 13
|
44 | 43 | simpld 475 |
. . . . . . . . . . . 12
|
45 | 26, 3, 27 | mvhf 31455 |
. . . . . . . . . . . . 13
mFS |
46 | | frn 6053 |
. . . . . . . . . . . . 13
|
47 | 6, 45, 46 | 3syl 18 |
. . . . . . . . . . . 12
|
48 | 44, 47 | unssd 3789 |
. . . . . . . . . . 11
|
49 | | fdm 6051 |
. . . . . . . . . . . 12
|
50 | 5, 49 | syl 17 |
. . . . . . . . . . 11
|
51 | 48, 50 | sseqtr4d 3642 |
. . . . . . . . . 10
|
52 | | funimass3 6333 |
. . . . . . . . . 10
|
53 | 41, 51, 52 | syl2anc 693 |
. . . . . . . . 9
|
54 | 39, 53 | mpbid 222 |
. . . . . . . 8
|
55 | | cnvco 5308 |
. . . . . . . . . 10
|
56 | 55 | imaeq1i 5463 |
. . . . . . . . 9
|
57 | | imaco 5640 |
. . . . . . . . 9
|
58 | 56, 57 | eqtri 2644 |
. . . . . . . 8
|
59 | 54, 58 | syl6sseqr 3652 |
. . . . . . 7
|
60 | 59 | unssad 3790 |
. . . . . 6
|
61 | 60 | sselda 3603 |
. . . . 5
|
62 | | elpreima 6337 |
. . . . . 6
|
63 | 62 | simplbda 654 |
. . . . 5
|
64 | 38, 61, 63 | syl2anc 693 |
. . . 4
|
65 | 37 | adantr 481 |
. . . . 5
|
66 | 59 | unssbd 3791 |
. . . . . . 7
|
67 | 66 | adantr 481 |
. . . . . 6
|
68 | | ffn 6045 |
. . . . . . . 8
|
69 | 6, 45, 68 | 3syl 18 |
. . . . . . 7
|
70 | | fnfvelrn 6356 |
. . . . . . 7
|
71 | 69, 70 | sylan 488 |
. . . . . 6
|
72 | 67, 71 | sseldd 3604 |
. . . . 5
|
73 | | elpreima 6337 |
. . . . . 6
|
74 | 73 | simplbda 654 |
. . . . 5
|
75 | 65, 72, 74 | syl2anc 693 |
. . . 4
|
76 | 5 | adantr 481 |
. . . . . . . . . . . . 13
|
77 | 6, 45 | syl 17 |
. . . . . . . . . . . . . . 15
|
78 | 77 | adantr 481 |
. . . . . . . . . . . . . 14
|
79 | 18 | simp1d 1073 |
. . . . . . . . . . . . . . . . . . . 20
|
80 | 79 | simpld 475 |
. . . . . . . . . . . . . . . . . . 19
|
81 | 26, 16 | mdvval 31401 |
. . . . . . . . . . . . . . . . . . . 20
|
82 | | difss 3737 |
. . . . . . . . . . . . . . . . . . . 20
|
83 | 81, 82 | eqsstri 3635 |
. . . . . . . . . . . . . . . . . . 19
|
84 | 80, 83 | syl6ss 3615 |
. . . . . . . . . . . . . . . . . 18
|
85 | 84 | ssbrd 4696 |
. . . . . . . . . . . . . . . . 17
|
86 | 85 | imp 445 |
. . . . . . . . . . . . . . . 16
|
87 | | brxp 5147 |
. . . . . . . . . . . . . . . 16
|
88 | 86, 87 | sylib 208 |
. . . . . . . . . . . . . . 15
|
89 | 88 | simpld 475 |
. . . . . . . . . . . . . 14
|
90 | 78, 89 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
|
91 | | fvco3 6275 |
. . . . . . . . . . . . 13
|
92 | 76, 90, 91 | syl2anc 693 |
. . . . . . . . . . . 12
|
93 | 92 | fveq2d 6195 |
. . . . . . . . . . 11
|
94 | 6 | adantr 481 |
. . . . . . . . . . . 12
mFS |
95 | 29 | adantr 481 |
. . . . . . . . . . . 12
|
96 | 76, 90 | ffvelrnd 6360 |
. . . . . . . . . . . 12
|
97 | 2, 3, 28, 27 | msubvrs 31457 |
. . . . . . . . . . . 12
mFS |
98 | 94, 95, 96, 97 | syl3anc 1326 |
. . . . . . . . . . 11
|
99 | 93, 98 | eqtrd 2656 |
. . . . . . . . . 10
|
100 | 99 | eleq2d 2687 |
. . . . . . . . 9
|
101 | | eliun 4524 |
. . . . . . . . 9
|
102 | 100, 101 | syl6bb 276 |
. . . . . . . 8
|
103 | 88 | simprd 479 |
. . . . . . . . . . . . . 14
|
104 | 78, 103 | ffvelrnd 6360 |
. . . . . . . . . . . . 13
|
105 | | fvco3 6275 |
. . . . . . . . . . . . 13
|
106 | 76, 104, 105 | syl2anc 693 |
. . . . . . . . . . . 12
|
107 | 106 | fveq2d 6195 |
. . . . . . . . . . 11
|
108 | 76, 104 | ffvelrnd 6360 |
. . . . . . . . . . . 12
|
109 | 2, 3, 28, 27 | msubvrs 31457 |
. . . . . . . . . . . 12
mFS |
110 | 94, 95, 108, 109 | syl3anc 1326 |
. . . . . . . . . . 11
|
111 | 107, 110 | eqtrd 2656 |
. . . . . . . . . 10
|
112 | 111 | eleq2d 2687 |
. . . . . . . . 9
|
113 | | eliun 4524 |
. . . . . . . . 9
|
114 | 112, 113 | syl6bb 276 |
. . . . . . . 8
|
115 | 102, 114 | anbi12d 747 |
. . . . . . 7
|
116 | | reeanv 3107 |
. . . . . . . 8
|
117 | | simpll 790 |
. . . . . . . . . 10
|
118 | | brxp 5147 |
. . . . . . . . . . . 12
|
119 | | mclsppslem.12 |
. . . . . . . . . . . . . . 15
|
120 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
121 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
122 | | breq12 4658 |
. . . . . . . . . . . . . . . . . 18
|
123 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
124 | 123 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
|
125 | 124 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
|
126 | 125 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
127 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
128 | 127 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
|
129 | 128 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
|
130 | 129 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
131 | 126, 130 | xpeq12d 5140 |
. . . . . . . . . . . . . . . . . . 19
|
132 | 131 | sseq1d 3632 |
. . . . . . . . . . . . . . . . . 18
|
133 | 122, 132 | imbi12d 334 |
. . . . . . . . . . . . . . . . 17
|
134 | 133 | spc2gv 3296 |
. . . . . . . . . . . . . . . 16
|
135 | 120, 121,
134 | mp2an 708 |
. . . . . . . . . . . . . . 15
|
136 | 119, 135 | syl 17 |
. . . . . . . . . . . . . 14
|
137 | 136 | imp 445 |
. . . . . . . . . . . . 13
|
138 | 137 | ssbrd 4696 |
. . . . . . . . . . . 12
|
139 | 118, 138 | syl5bir 233 |
. . . . . . . . . . 11
|
140 | 139 | imp 445 |
. . . . . . . . . 10
|
141 | | vex 3203 |
. . . . . . . . . . . . 13
|
142 | | vex 3203 |
. . . . . . . . . . . . 13
|
143 | | breq12 4658 |
. . . . . . . . . . . . . . . 16
|
144 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . 20
|
145 | 144 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
|
146 | 145 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
147 | 146 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
148 | 147 | eleq2d 2687 |
. . . . . . . . . . . . . . . 16
|
149 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
150 | 149 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
|
151 | 150 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
152 | 151 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
153 | 152 | eleq2d 2687 |
. . . . . . . . . . . . . . . 16
|
154 | 143, 148,
153 | 3anbi123d 1399 |
. . . . . . . . . . . . . . 15
|
155 | 154 | anbi2d 740 |
. . . . . . . . . . . . . 14
|
156 | 155 | imbi1d 331 |
. . . . . . . . . . . . 13
|
157 | | mclspps.8 |
. . . . . . . . . . . . 13
|
158 | 141, 142,
156, 157 | vtocl2 3261 |
. . . . . . . . . . . 12
|
159 | 158 | 3exp2 1285 |
. . . . . . . . . . 11
|
160 | 159 | imp4b 613 |
. . . . . . . . . 10
|
161 | 117, 140,
160 | syl2anc 693 |
. . . . . . . . 9
|
162 | 161 | rexlimdvva 3038 |
. . . . . . . 8
|
163 | 116, 162 | syl5bir 233 |
. . . . . . 7
|
164 | 115, 163 | sylbid 230 |
. . . . . 6
|
165 | 164 | exp4b 632 |
. . . . 5
|
166 | 165 | 3imp2 1282 |
. . . 4
|
167 | 16, 3, 23, 6, 24, 25, 7, 2, 26, 27, 28, 14, 31, 64, 75, 166 | mclsax 31466 |
. . 3
|
168 | 22, 167 | eqeltrrd 2702 |
. 2
|
169 | | ffn 6045 |
. . . 4
|
170 | 33, 169 | syl 17 |
. . 3
|
171 | | elpreima 6337 |
. . 3
|
172 | 170, 171 | syl 17 |
. 2
|
173 | 20, 168, 172 | mpbir2and 957 |
1
|