Step | Hyp | Ref
| Expression |
1 | | mclsval.c |
. . 3
mCls |
2 | | mclsval.1 |
. . . 4
mFS |
3 | | elex 3212 |
. . . 4
mFS |
4 | | fveq2 6191 |
. . . . . . . 8
mDV mDV |
5 | | mclsval.d |
. . . . . . . 8
mDV |
6 | 4, 5 | syl6eqr 2674 |
. . . . . . 7
mDV |
7 | 6 | pweqd 4163 |
. . . . . 6
mDV |
8 | | fveq2 6191 |
. . . . . . . 8
mEx mEx |
9 | | mclsval.e |
. . . . . . . 8
mEx |
10 | 8, 9 | syl6eqr 2674 |
. . . . . . 7
mEx |
11 | 10 | pweqd 4163 |
. . . . . 6
mEx |
12 | | fveq2 6191 |
. . . . . . . . . . . . 13
mVH mVH |
13 | | mclsval.h |
. . . . . . . . . . . . 13
mVH |
14 | 12, 13 | syl6eqr 2674 |
. . . . . . . . . . . 12
mVH |
15 | 14 | rneqd 5353 |
. . . . . . . . . . 11
mVH |
16 | 15 | uneq2d 3767 |
. . . . . . . . . 10
mVH |
17 | 16 | sseq1d 3632 |
. . . . . . . . 9
mVH
|
18 | | fveq2 6191 |
. . . . . . . . . . . . . 14
mAx mAx |
19 | | mclsval.a |
. . . . . . . . . . . . . 14
mAx |
20 | 18, 19 | syl6eqr 2674 |
. . . . . . . . . . . . 13
mAx |
21 | 20 | eleq2d 2687 |
. . . . . . . . . . . 12
mAx
|
22 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
mSubst mSubst |
23 | | mclsval.s |
. . . . . . . . . . . . . . 15
mSubst |
24 | 22, 23 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
mSubst |
25 | 24 | rneqd 5353 |
. . . . . . . . . . . . 13
mSubst |
26 | 15 | uneq2d 3767 |
. . . . . . . . . . . . . . . . 17
mVH |
27 | 26 | imaeq2d 5466 |
. . . . . . . . . . . . . . . 16
mVH |
28 | 27 | sseq1d 3632 |
. . . . . . . . . . . . . . 15
mVH
|
29 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
mVars mVars |
30 | | mclsval.v |
. . . . . . . . . . . . . . . . . . . . 21
mVars |
31 | 29, 30 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . . 20
mVars |
32 | 14 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . 21
mVH |
33 | 32 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
mVH |
34 | 31, 33 | fveq12d 6197 |
. . . . . . . . . . . . . . . . . . 19
mVarsmVH |
35 | 14 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . 21
mVH |
36 | 35 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
mVH |
37 | 31, 36 | fveq12d 6197 |
. . . . . . . . . . . . . . . . . . 19
mVarsmVH |
38 | 34, 37 | xpeq12d 5140 |
. . . . . . . . . . . . . . . . . 18
mVarsmVH mVarsmVH |
39 | 38 | sseq1d 3632 |
. . . . . . . . . . . . . . . . 17
mVarsmVH mVarsmVH |
40 | 39 | imbi2d 330 |
. . . . . . . . . . . . . . . 16
mVarsmVH mVarsmVH
|
41 | 40 | 2albidv 1851 |
. . . . . . . . . . . . . . 15
mVarsmVH mVarsmVH
|
42 | 28, 41 | anbi12d 747 |
. . . . . . . . . . . . . 14
mVH
mVarsmVH mVarsmVH
|
43 | 42 | imbi1d 331 |
. . . . . . . . . . . . 13
mVH mVarsmVH mVarsmVH |
44 | 25, 43 | raleqbidv 3152 |
. . . . . . . . . . . 12
mSubst mVH
mVarsmVH mVarsmVH
|
45 | 21, 44 | imbi12d 334 |
. . . . . . . . . . 11
mAx
mSubst mVH
mVarsmVH mVarsmVH |
46 | 45 | albidv 1849 |
. . . . . . . . . 10
mAx
mSubst mVH mVarsmVH mVarsmVH
|
47 | 46 | 2albidv 1851 |
. . . . . . . . 9
mAx
mSubst mVH mVarsmVH mVarsmVH
|
48 | 17, 47 | anbi12d 747 |
. . . . . . . 8
mVH
mAx
mSubst mVH mVarsmVH mVarsmVH
|
49 | 48 | abbidv 2741 |
. . . . . . 7
mVH
mAx mSubst mVH mVarsmVH mVarsmVH
|
50 | 49 | inteqd 4480 |
. . . . . 6
mVH
mAx mSubst mVH mVarsmVH mVarsmVH
|
51 | 7, 11, 50 | mpt2eq123dv 6717 |
. . . . 5
mDV mEx mVH
mAx
mSubst mVH mVarsmVH mVarsmVH
|
52 | | df-mcls 31394 |
. . . . 5
mCls mDV mEx mVH
mAx
mSubst mVH mVarsmVH mVarsmVH
|
53 | | fvex 6201 |
. . . . . . . 8
mDV |
54 | 5, 53 | eqeltri 2697 |
. . . . . . 7
|
55 | 54 | pwex 4848 |
. . . . . 6
|
56 | | fvex 6201 |
. . . . . . . 8
mEx |
57 | 9, 56 | eqeltri 2697 |
. . . . . . 7
|
58 | 57 | pwex 4848 |
. . . . . 6
|
59 | 55, 58 | mpt2ex 7247 |
. . . . 5
|
60 | 51, 52, 59 | fvmpt 6282 |
. . . 4
mCls
|
61 | 2, 3, 60 | 3syl 18 |
. . 3
mCls |
62 | 1, 61 | syl5eq 2668 |
. 2
|
63 | | simprr 796 |
. . . . . . 7
|
64 | 63 | uneq1d 3766 |
. . . . . 6
|
65 | 64 | sseq1d 3632 |
. . . . 5
|
66 | | simprl 794 |
. . . . . . . . . . . . . 14
|
67 | 66 | sseq2d 3633 |
. . . . . . . . . . . . 13
|
68 | 67 | imbi2d 330 |
. . . . . . . . . . . 12
|
69 | 68 | 2albidv 1851 |
. . . . . . . . . . 11
|
70 | 69 | anbi2d 740 |
. . . . . . . . . 10
|
71 | 70 | imbi1d 331 |
. . . . . . . . 9
|
72 | 71 | ralbidv 2986 |
. . . . . . . 8
|
73 | 72 | imbi2d 330 |
. . . . . . 7
|
74 | 73 | albidv 1849 |
. . . . . 6
|
75 | 74 | 2albidv 1851 |
. . . . 5
|
76 | 65, 75 | anbi12d 747 |
. . . 4
|
77 | 76 | abbidv 2741 |
. . 3
|
78 | 77 | inteqd 4480 |
. 2
|
79 | | mclsval.2 |
. . 3
|
80 | 54 | elpw2 4828 |
. . 3
|
81 | 79, 80 | sylibr 224 |
. 2
|
82 | | mclsval.3 |
. . 3
|
83 | 57 | elpw2 4828 |
. . 3
|
84 | 82, 83 | sylibr 224 |
. 2
|
85 | 5, 9, 1, 2, 79, 82, 13, 19, 23, 30 | mclsssvlem 31459 |
. . 3
|
86 | 57 | ssex 4802 |
. . 3
|
87 | 85, 86 | syl 17 |
. 2
|
88 | 62, 78, 81, 84, 87 | ovmpt2d 6788 |
1
|