Step | Hyp | Ref
| Expression |
1 | | abid 2610 |
. . . . . . . 8
|
2 | | intss1 4492 |
. . . . . . . 8
|
3 | 1, 2 | sylbir 225 |
. . . . . . 7
|
4 | | mclsval.d |
. . . . . . . . 9
mDV |
5 | | mclsval.e |
. . . . . . . . 9
mEx |
6 | | mclsval.c |
. . . . . . . . 9
mCls |
7 | | mclsval.1 |
. . . . . . . . 9
mFS |
8 | | mclsval.2 |
. . . . . . . . 9
|
9 | | mclsval.3 |
. . . . . . . . 9
|
10 | | mclsax.h |
. . . . . . . . 9
mVH |
11 | | mclsax.a |
. . . . . . . . 9
mAx |
12 | | mclsax.l |
. . . . . . . . 9
mSubst |
13 | | mclsax.w |
. . . . . . . . 9
mVars |
14 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 | mclsval 31460 |
. . . . . . . 8
|
15 | 14 | sseq1d 3632 |
. . . . . . 7
|
16 | 3, 15 | syl5ibr 236 |
. . . . . 6
|
17 | | sstr2 3610 |
. . . . . . . . . . . . . . 15
|
18 | 17 | com12 32 |
. . . . . . . . . . . . . 14
|
19 | 18 | anim1d 588 |
. . . . . . . . . . . . 13
|
20 | 19 | imim1d 82 |
. . . . . . . . . . . 12
|
21 | 20 | ralimdv 2963 |
. . . . . . . . . . 11
|
22 | 21 | imim2d 57 |
. . . . . . . . . 10
|
23 | 22 | alimdv 1845 |
. . . . . . . . 9
|
24 | 23 | 2alimdv 1847 |
. . . . . . . 8
|
25 | 24 | com12 32 |
. . . . . . 7
|
26 | 25 | adantl 482 |
. . . . . 6
|
27 | 16, 26 | sylcom 30 |
. . . . 5
|
28 | | eqid 2622 |
. . . . . . . 8
mPreSt mPreSt |
29 | | eqid 2622 |
. . . . . . . 8
mStat mStat |
30 | 28, 29 | mstapst 31444 |
. . . . . . 7
mStat mPreSt |
31 | 11, 29 | maxsta 31451 |
. . . . . . . . 9
mFS mStat |
32 | 7, 31 | syl 17 |
. . . . . . . 8
mStat |
33 | | mclsax.4 |
. . . . . . . 8
|
34 | 32, 33 | sseldd 3604 |
. . . . . . 7
mStat |
35 | 30, 34 | sseldi 3601 |
. . . . . 6
mPreSt |
36 | 28 | mpstrcl 31438 |
. . . . . 6
mPreSt
|
37 | | simp1 1061 |
. . . . . . . . . 10
|
38 | | simp2 1062 |
. . . . . . . . . 10
|
39 | | simp3 1063 |
. . . . . . . . . 10
|
40 | 37, 38, 39 | oteq123d 4417 |
. . . . . . . . 9
|
41 | 40 | eleq1d 2686 |
. . . . . . . 8
|
42 | 38 | uneq1d 3766 |
. . . . . . . . . . . . 13
|
43 | 42 | imaeq2d 5466 |
. . . . . . . . . . . 12
|
44 | 43 | sseq1d 3632 |
. . . . . . . . . . 11
|
45 | 37 | breqd 4664 |
. . . . . . . . . . . . 13
|
46 | 45 | imbi1d 331 |
. . . . . . . . . . . 12
|
47 | 46 | 2albidv 1851 |
. . . . . . . . . . 11
|
48 | 44, 47 | anbi12d 747 |
. . . . . . . . . 10
|
49 | 39 | fveq2d 6195 |
. . . . . . . . . . 11
|
50 | 49 | eleq1d 2686 |
. . . . . . . . . 10
|
51 | 48, 50 | imbi12d 334 |
. . . . . . . . 9
|
52 | 51 | ralbidv 2986 |
. . . . . . . 8
|
53 | 41, 52 | imbi12d 334 |
. . . . . . 7
|
54 | 53 | spc3gv 3298 |
. . . . . 6
|
55 | 35, 36, 54 | 3syl 18 |
. . . . 5
|
56 | | elun 3753 |
. . . . . . . . . . 11
|
57 | | mclsax.6 |
. . . . . . . . . . . 12
|
58 | | mclsax.7 |
. . . . . . . . . . . . . . 15
|
59 | 58 | ralrimiva 2966 |
. . . . . . . . . . . . . 14
|
60 | | mclsax.v |
. . . . . . . . . . . . . . . . 17
mVR |
61 | 60, 5, 10 | mvhf 31455 |
. . . . . . . . . . . . . . . 16
mFS |
62 | 7, 61 | syl 17 |
. . . . . . . . . . . . . . 15
|
63 | | ffn 6045 |
. . . . . . . . . . . . . . 15
|
64 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
65 | 64 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
|
66 | 65 | ralrn 6362 |
. . . . . . . . . . . . . . 15
|
67 | 62, 63, 66 | 3syl 18 |
. . . . . . . . . . . . . 14
|
68 | 59, 67 | mpbird 247 |
. . . . . . . . . . . . 13
|
69 | 68 | r19.21bi 2932 |
. . . . . . . . . . . 12
|
70 | 57, 69 | jaodan 826 |
. . . . . . . . . . 11
|
71 | 56, 70 | sylan2b 492 |
. . . . . . . . . 10
|
72 | 71 | ralrimiva 2966 |
. . . . . . . . 9
|
73 | | mclsax.5 |
. . . . . . . . . . . 12
|
74 | 12, 5 | msubf 31429 |
. . . . . . . . . . . 12
|
75 | 73, 74 | syl 17 |
. . . . . . . . . . 11
|
76 | | ffun 6048 |
. . . . . . . . . . 11
|
77 | 75, 76 | syl 17 |
. . . . . . . . . 10
|
78 | 4, 5, 28 | elmpst 31433 |
. . . . . . . . . . . . . . 15
mPreSt
|
79 | 35, 78 | sylib 208 |
. . . . . . . . . . . . . 14
|
80 | 79 | simp2d 1074 |
. . . . . . . . . . . . 13
|
81 | 80 | simpld 475 |
. . . . . . . . . . . 12
|
82 | | fdm 6051 |
. . . . . . . . . . . . 13
|
83 | 75, 82 | syl 17 |
. . . . . . . . . . . 12
|
84 | 81, 83 | sseqtr4d 3642 |
. . . . . . . . . . 11
|
85 | | frn 6053 |
. . . . . . . . . . . . 13
|
86 | 62, 85 | syl 17 |
. . . . . . . . . . . 12
|
87 | 86, 83 | sseqtr4d 3642 |
. . . . . . . . . . 11
|
88 | 84, 87 | unssd 3789 |
. . . . . . . . . 10
|
89 | | funimass4 6247 |
. . . . . . . . . 10
|
90 | 77, 88, 89 | syl2anc 693 |
. . . . . . . . 9
|
91 | 72, 90 | mpbird 247 |
. . . . . . . 8
|
92 | | mclsax.8 |
. . . . . . . . . . . . . 14
|
93 | 92 | 3exp2 1285 |
. . . . . . . . . . . . 13
|
94 | 93 | imp4b 613 |
. . . . . . . . . . . 12
|
95 | 94 | ralrimivv 2970 |
. . . . . . . . . . 11
|
96 | | dfss3 3592 |
. . . . . . . . . . . 12
|
97 | | eleq1 2689 |
. . . . . . . . . . . . . 14
|
98 | | df-br 4654 |
. . . . . . . . . . . . . 14
|
99 | 97, 98 | syl6bbr 278 |
. . . . . . . . . . . . 13
|
100 | 99 | ralxp 5263 |
. . . . . . . . . . . 12
|
101 | 96, 100 | bitri 264 |
. . . . . . . . . . 11
|
102 | 95, 101 | sylibr 224 |
. . . . . . . . . 10
|
103 | 102 | ex 450 |
. . . . . . . . 9
|
104 | 103 | alrimivv 1856 |
. . . . . . . 8
|
105 | 91, 104 | jca 554 |
. . . . . . 7
|
106 | | imaeq1 5461 |
. . . . . . . . . . . 12
|
107 | 106 | sseq1d 3632 |
. . . . . . . . . . 11
|
108 | | fveq1 6190 |
. . . . . . . . . . . . . . . 16
|
109 | 108 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
110 | | fveq1 6190 |
. . . . . . . . . . . . . . . 16
|
111 | 110 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
112 | 109, 111 | xpeq12d 5140 |
. . . . . . . . . . . . . 14
|
113 | 112 | sseq1d 3632 |
. . . . . . . . . . . . 13
|
114 | 113 | imbi2d 330 |
. . . . . . . . . . . 12
|
115 | 114 | 2albidv 1851 |
. . . . . . . . . . 11
|
116 | 107, 115 | anbi12d 747 |
. . . . . . . . . 10
|
117 | | fveq1 6190 |
. . . . . . . . . . 11
|
118 | 117 | eleq1d 2686 |
. . . . . . . . . 10
|
119 | 116, 118 | imbi12d 334 |
. . . . . . . . 9
|
120 | 119 | rspcv 3305 |
. . . . . . . 8
|
121 | 73, 120 | syl 17 |
. . . . . . 7
|
122 | 105, 121 | mpid 44 |
. . . . . 6
|
123 | 33, 122 | embantd 59 |
. . . . 5
|
124 | 27, 55, 123 | 3syld 60 |
. . . 4
|
125 | 124 | alrimiv 1855 |
. . 3
|
126 | | fvex 6201 |
. . . 4
|
127 | 126 | elintab 4487 |
. . 3
|
128 | 125, 127 | sylibr 224 |
. 2
|
129 | 128, 14 | eleqtrrd 2704 |
1
|