Step | Hyp | Ref
| Expression |
1 | | msubvrs.e |
. . . . . 6
mEx |
2 | | eqid 2622 |
. . . . . 6
mRSubst mRSubst |
3 | | msubvrs.s |
. . . . . 6
mSubst |
4 | 1, 2, 3 | elmsubrn 31425 |
. . . . 5
mRSubst |
5 | 4 | eleq2i 2693 |
. . . 4
mRSubst |
6 | | eqid 2622 |
. . . . 5
mRSubst mRSubst |
7 | | fvex 6201 |
. . . . . . 7
mEx |
8 | 1, 7 | eqeltri 2697 |
. . . . . 6
|
9 | 8 | mptex 6486 |
. . . . 5
|
10 | 6, 9 | elrnmpti 5376 |
. . . 4
mRSubst mRSubst |
11 | 5, 10 | bitri 264 |
. . 3
mRSubst |
12 | | simp2 1062 |
. . . . . . . . 9
mFS mRSubst
mRSubst |
13 | | simp3 1063 |
. . . . . . . . . . 11
mFS mRSubst
|
14 | | eqid 2622 |
. . . . . . . . . . . 12
mTC mTC |
15 | | eqid 2622 |
. . . . . . . . . . . 12
mREx mREx |
16 | 14, 1, 15 | mexval 31399 |
. . . . . . . . . . 11
mTC mREx |
17 | 13, 16 | syl6eleq 2711 |
. . . . . . . . . 10
mFS mRSubst
mTC mREx |
18 | | xp2nd 7199 |
. . . . . . . . . 10
mTC mREx mREx |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
mFS mRSubst
mREx |
20 | | eqid 2622 |
. . . . . . . . . 10
mVR mVR |
21 | 2, 20, 15 | mrsubvrs 31419 |
. . . . . . . . 9
mRSubst mREx
mVR
mVR mVR |
22 | 12, 19, 21 | syl2anc 693 |
. . . . . . . 8
mFS mRSubst
mVR
mVR mVR |
23 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
24 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
25 | 24 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
26 | 23, 25 | opeq12d 4410 |
. . . . . . . . . . . 12
|
27 | | eqid 2622 |
. . . . . . . . . . . 12
|
28 | | opex 4932 |
. . . . . . . . . . . 12
|
29 | 26, 27, 28 | fvmpt3i 6287 |
. . . . . . . . . . 11
|
30 | 13, 29 | syl 17 |
. . . . . . . . . 10
mFS mRSubst
|
31 | 30 | fveq2d 6195 |
. . . . . . . . 9
mFS mRSubst
|
32 | | xp1st 7198 |
. . . . . . . . . . . . 13
mTC mREx mTC |
33 | 17, 32 | syl 17 |
. . . . . . . . . . . 12
mFS mRSubst
mTC |
34 | 2, 15 | mrsubf 31414 |
. . . . . . . . . . . . . 14
mRSubst
mRExmREx |
35 | 12, 34 | syl 17 |
. . . . . . . . . . . . 13
mFS mRSubst
mRExmREx |
36 | 18, 16 | eleq2s 2719 |
. . . . . . . . . . . . . 14
mREx |
37 | 13, 36 | syl 17 |
. . . . . . . . . . . . 13
mFS mRSubst
mREx |
38 | 35, 37 | ffvelrnd 6360 |
. . . . . . . . . . . 12
mFS mRSubst
mREx |
39 | | opelxpi 5148 |
. . . . . . . . . . . 12
mTC mREx
mTC mREx |
40 | 33, 38, 39 | syl2anc 693 |
. . . . . . . . . . 11
mFS mRSubst
mTC mREx |
41 | 40, 16 | syl6eleqr 2712 |
. . . . . . . . . 10
mFS mRSubst
|
42 | | msubvrs.v |
. . . . . . . . . . 11
mVars |
43 | 20, 1, 42 | mvrsval 31402 |
. . . . . . . . . 10
mVR |
44 | 41, 43 | syl 17 |
. . . . . . . . 9
mFS mRSubst
mVR |
45 | | fvex 6201 |
. . . . . . . . . . . . 13
|
46 | | fvex 6201 |
. . . . . . . . . . . . 13
|
47 | 45, 46 | op2nd 7177 |
. . . . . . . . . . . 12
|
48 | 47 | a1i 11 |
. . . . . . . . . . 11
mFS mRSubst
|
49 | 48 | rneqd 5353 |
. . . . . . . . . 10
mFS mRSubst
|
50 | 49 | ineq1d 3813 |
. . . . . . . . 9
mFS mRSubst
mVR mVR |
51 | 31, 44, 50 | 3eqtrd 2660 |
. . . . . . . 8
mFS mRSubst
mVR |
52 | 20, 1, 42 | mvrsval 31402 |
. . . . . . . . . . 11
mVR |
53 | 13, 52 | syl 17 |
. . . . . . . . . 10
mFS mRSubst
mVR |
54 | 53 | iuneq1d 4545 |
. . . . . . . . 9
mFS mRSubst
mVR |
55 | | msubvrs.h |
. . . . . . . . . . . . . . . . 17
mVH |
56 | 20, 1, 55 | mvhf 31455 |
. . . . . . . . . . . . . . . 16
mFS mVR |
57 | 56 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
mFS mRSubst
mVR |
58 | | inss2 3834 |
. . . . . . . . . . . . . . . 16
mVR mVR |
59 | 58 | sseli 3599 |
. . . . . . . . . . . . . . 15
mVR
mVR |
60 | | ffvelrn 6357 |
. . . . . . . . . . . . . . 15
mVR
mVR |
61 | 57, 59, 60 | syl2an 494 |
. . . . . . . . . . . . . 14
mFS
mRSubst
mVR |
62 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
63 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
64 | 63 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
65 | 62, 64 | opeq12d 4410 |
. . . . . . . . . . . . . . 15
|
66 | 65, 27, 28 | fvmpt3i 6287 |
. . . . . . . . . . . . . 14
|
67 | 61, 66 | syl 17 |
. . . . . . . . . . . . 13
mFS
mRSubst
mVR |
68 | 59 | adantl 482 |
. . . . . . . . . . . . . . . 16
mFS
mRSubst
mVR mVR |
69 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
mType mType |
70 | 20, 69, 55 | mvhval 31431 |
. . . . . . . . . . . . . . . 16
mVR
mType |
71 | 68, 70 | syl 17 |
. . . . . . . . . . . . . . 15
mFS
mRSubst
mVR mType |
72 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
mType |
73 | | s1cli 13384 |
. . . . . . . . . . . . . . . . 17
Word
|
74 | 73 | elexi 3213 |
. . . . . . . . . . . . . . . 16
|
75 | 72, 74 | op1std 7178 |
. . . . . . . . . . . . . . 15
mType
mType |
76 | 71, 75 | syl 17 |
. . . . . . . . . . . . . 14
mFS
mRSubst
mVR mType |
77 | 72, 74 | op2ndd 7179 |
. . . . . . . . . . . . . . . 16
mType
|
78 | 71, 77 | syl 17 |
. . . . . . . . . . . . . . 15
mFS
mRSubst
mVR |
79 | 78 | fveq2d 6195 |
. . . . . . . . . . . . . 14
mFS
mRSubst
mVR |
80 | 76, 79 | opeq12d 4410 |
. . . . . . . . . . . . 13
mFS
mRSubst
mVR mType |
81 | 67, 80 | eqtrd 2656 |
. . . . . . . . . . . 12
mFS
mRSubst
mVR mType |
82 | 81 | fveq2d 6195 |
. . . . . . . . . . 11
mFS
mRSubst
mVR mType |
83 | | simpl1 1064 |
. . . . . . . . . . . . . . . 16
mFS
mRSubst
mVR mFS |
84 | 20, 14, 69 | mtyf2 31448 |
. . . . . . . . . . . . . . . 16
mFS mTypemVRmTC |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . 15
mFS
mRSubst
mVR mTypemVRmTC |
86 | 85, 68 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
mFS
mRSubst
mVR mType mTC |
87 | 35 | adantr 481 |
. . . . . . . . . . . . . . 15
mFS
mRSubst
mVR mRExmREx |
88 | | elun2 3781 |
. . . . . . . . . . . . . . . . . 18
mVR
mCN mVR |
89 | 68, 88 | syl 17 |
. . . . . . . . . . . . . . . . 17
mFS
mRSubst
mVR mCN mVR |
90 | 89 | s1cld 13383 |
. . . . . . . . . . . . . . . 16
mFS
mRSubst
mVR Word
mCN mVR |
91 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
mCN mCN |
92 | 91, 20, 15 | mrexval 31398 |
. . . . . . . . . . . . . . . . 17
mFS mREx Word
mCN mVR |
93 | 83, 92 | syl 17 |
. . . . . . . . . . . . . . . 16
mFS
mRSubst
mVR mREx Word
mCN mVR |
94 | 90, 93 | eleqtrrd 2704 |
. . . . . . . . . . . . . . 15
mFS
mRSubst
mVR mREx |
95 | 87, 94 | ffvelrnd 6360 |
. . . . . . . . . . . . . 14
mFS
mRSubst
mVR
mREx |
96 | | opelxpi 5148 |
. . . . . . . . . . . . . 14
mType mTC mREx
mType mTC mREx |
97 | 86, 95, 96 | syl2anc 693 |
. . . . . . . . . . . . 13
mFS
mRSubst
mVR mType mTC mREx |
98 | 97, 16 | syl6eleqr 2712 |
. . . . . . . . . . . 12
mFS
mRSubst
mVR mType |
99 | 20, 1, 42 | mvrsval 31402 |
. . . . . . . . . . . 12
mType mType mType mVR |
100 | 98, 99 | syl 17 |
. . . . . . . . . . 11
mFS
mRSubst
mVR mType mType mVR |
101 | | fvex 6201 |
. . . . . . . . . . . . . . 15
|
102 | 72, 101 | op2nd 7177 |
. . . . . . . . . . . . . 14
mType |
103 | 102 | a1i 11 |
. . . . . . . . . . . . 13
mFS
mRSubst
mVR mType |
104 | 103 | rneqd 5353 |
. . . . . . . . . . . 12
mFS
mRSubst
mVR
mType |
105 | 104 | ineq1d 3813 |
. . . . . . . . . . 11
mFS
mRSubst
mVR mType mVR mVR |
106 | 82, 100, 105 | 3eqtrd 2660 |
. . . . . . . . . 10
mFS
mRSubst
mVR mVR |
107 | 106 | iuneq2dv 4542 |
. . . . . . . . 9
mFS mRSubst
mVR
mVR mVR |
108 | 54, 107 | eqtrd 2656 |
. . . . . . . 8
mFS mRSubst
mVR mVR |
109 | 22, 51, 108 | 3eqtr4d 2666 |
. . . . . . 7
mFS mRSubst
|
110 | | fveq1 6190 |
. . . . . . . . 9
|
111 | 110 | fveq2d 6195 |
. . . . . . . 8
|
112 | | fveq1 6190 |
. . . . . . . . . 10
|
113 | 112 | fveq2d 6195 |
. . . . . . . . 9
|
114 | 113 | iuneq2d 4547 |
. . . . . . . 8
|
115 | 111, 114 | eqeq12d 2637 |
. . . . . . 7
|
116 | 109, 115 | syl5ibrcom 237 |
. . . . . 6
mFS mRSubst
|
117 | 116 | 3expia 1267 |
. . . . 5
mFS mRSubst
|
118 | 117 | com23 86 |
. . . 4
mFS mRSubst
|
119 | 118 | rexlimdva 3031 |
. . 3
mFS mRSubst |
120 | 11, 119 | syl5bi 232 |
. 2
mFS
|
121 | 120 | 3imp 1256 |
1
mFS |