Step | Hyp | Ref
| Expression |
1 | | msubff1.v |
. . . 4
mVR |
2 | | msubff1.r |
. . . 4
mREx |
3 | | msubff1.s |
. . . 4
mSubst |
4 | | msubff1.e |
. . . 4
mEx |
5 | 1, 2, 3, 4 | msubff 31427 |
. . 3
mFS
|
6 | | mapsspm 7891 |
. . . 4
|
7 | 6 | a1i 11 |
. . 3
mFS |
8 | 5, 7 | fssresd 6071 |
. 2
mFS
|
9 | | eqid 2622 |
. . . . . . . . . . . . 13
mRSubst mRSubst |
10 | 1, 2, 9 | mrsubff 31409 |
. . . . . . . . . . . 12
mFS mRSubst |
11 | 10 | ad2antrr 762 |
. . . . . . . . . . 11
mFS mRSubst |
12 | | simplrl 800 |
. . . . . . . . . . . 12
mFS |
13 | 6, 12 | sseldi 3601 |
. . . . . . . . . . 11
mFS
|
14 | 11, 13 | ffvelrnd 6360 |
. . . . . . . . . 10
mFS mRSubst |
15 | | elmapi 7879 |
. . . . . . . . . 10
mRSubst mRSubst |
16 | | ffn 6045 |
. . . . . . . . . 10
mRSubst mRSubst |
17 | 14, 15, 16 | 3syl 18 |
. . . . . . . . 9
mFS mRSubst |
18 | | simplrr 801 |
. . . . . . . . . . . 12
mFS |
19 | 6, 18 | sseldi 3601 |
. . . . . . . . . . 11
mFS
|
20 | 11, 19 | ffvelrnd 6360 |
. . . . . . . . . 10
mFS mRSubst |
21 | | elmapi 7879 |
. . . . . . . . . 10
mRSubst mRSubst |
22 | | ffn 6045 |
. . . . . . . . . 10
mRSubst mRSubst |
23 | 20, 21, 22 | 3syl 18 |
. . . . . . . . 9
mFS mRSubst |
24 | | simplrr 801 |
. . . . . . . . . . . . 13
mFS
|
25 | 24 | fveq1d 6193 |
. . . . . . . . . . . 12
mFS
mType mType |
26 | 12 | adantr 481 |
. . . . . . . . . . . . . 14
mFS
|
27 | | elmapi 7879 |
. . . . . . . . . . . . . 14
|
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . 13
mFS
|
29 | | ssid 3624 |
. . . . . . . . . . . . . 14
|
30 | 29 | a1i 11 |
. . . . . . . . . . . . 13
mFS
|
31 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
mTC mTC |
32 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
mType mType |
33 | 1, 31, 32 | mtyf2 31448 |
. . . . . . . . . . . . . . . . 17
mFS mTypemTC |
34 | 33 | ad3antrrr 766 |
. . . . . . . . . . . . . . . 16
mFS
mTypemTC |
35 | | simplrl 800 |
. . . . . . . . . . . . . . . 16
mFS
|
36 | 34, 35 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
mFS
mType mTC |
37 | | opelxpi 5148 |
. . . . . . . . . . . . . . 15
mType mTC
mType mTC |
38 | 36, 37 | sylancom 701 |
. . . . . . . . . . . . . 14
mFS
mType mTC |
39 | 31, 4, 2 | mexval 31399 |
. . . . . . . . . . . . . 14
mTC |
40 | 38, 39 | syl6eleqr 2712 |
. . . . . . . . . . . . 13
mFS
mType |
41 | 1, 2, 3, 4, 9 | msubval 31422 |
. . . . . . . . . . . . 13
mType mType
mType mRSubstmType |
42 | 28, 30, 40, 41 | syl3anc 1326 |
. . . . . . . . . . . 12
mFS
mType mType mRSubstmType |
43 | 18 | adantr 481 |
. . . . . . . . . . . . . 14
mFS
|
44 | | elmapi 7879 |
. . . . . . . . . . . . . 14
|
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . 13
mFS
|
46 | 1, 2, 3, 4, 9 | msubval 31422 |
. . . . . . . . . . . . 13
mType mType
mType mRSubstmType |
47 | 45, 30, 40, 46 | syl3anc 1326 |
. . . . . . . . . . . 12
mFS
mType mType mRSubstmType |
48 | 25, 42, 47 | 3eqtr3d 2664 |
. . . . . . . . . . 11
mFS
mType mRSubstmType mType mRSubstmType |
49 | | fvex 6201 |
. . . . . . . . . . . . 13
mType |
50 | | fvex 6201 |
. . . . . . . . . . . . 13
mRSubstmType |
51 | 49, 50 | opth 4945 |
. . . . . . . . . . . 12
mType mRSubstmType mType mRSubstmType
mType mType
mRSubstmType mRSubstmType |
52 | 51 | simprbi 480 |
. . . . . . . . . . 11
mType mRSubstmType mType mRSubstmType mRSubstmType mRSubstmType |
53 | 48, 52 | syl 17 |
. . . . . . . . . 10
mFS
mRSubstmType mRSubstmType |
54 | | fvex 6201 |
. . . . . . . . . . . 12
mType |
55 | | vex 3203 |
. . . . . . . . . . . 12
|
56 | 54, 55 | op2nd 7177 |
. . . . . . . . . . 11
mType |
57 | 56 | fveq2i 6194 |
. . . . . . . . . 10
mRSubstmType mRSubst |
58 | 56 | fveq2i 6194 |
. . . . . . . . . 10
mRSubstmType mRSubst |
59 | 53, 57, 58 | 3eqtr3g 2679 |
. . . . . . . . 9
mFS
mRSubst mRSubst |
60 | 17, 23, 59 | eqfnfvd 6314 |
. . . . . . . 8
mFS mRSubst mRSubst |
61 | 1, 2, 9 | mrsubff1 31411 |
. . . . . . . . . . 11
mFS mRSubst |
62 | | f1fveq 6519 |
. . . . . . . . . . 11
mRSubst
mRSubst mRSubst |
63 | 61, 62 | sylan 488 |
. . . . . . . . . 10
mFS
mRSubst mRSubst |
64 | | fvres 6207 |
. . . . . . . . . . . 12
mRSubst mRSubst |
65 | | fvres 6207 |
. . . . . . . . . . . 12
mRSubst mRSubst |
66 | 64, 65 | eqeqan12d 2638 |
. . . . . . . . . . 11
mRSubst mRSubst
mRSubst mRSubst |
67 | 66 | adantl 482 |
. . . . . . . . . 10
mFS
mRSubst mRSubst mRSubst mRSubst |
68 | 63, 67 | bitr3d 270 |
. . . . . . . . 9
mFS
mRSubst mRSubst |
69 | 68 | adantr 481 |
. . . . . . . 8
mFS mRSubst mRSubst |
70 | 60, 69 | mpbird 247 |
. . . . . . 7
mFS |
71 | 70 | fveq1d 6193 |
. . . . . 6
mFS |
72 | 71 | expr 643 |
. . . . 5
mFS |
73 | 72 | ralrimdva 2969 |
. . . 4
mFS
|
74 | | fvres 6207 |
. . . . . 6
|
75 | | fvres 6207 |
. . . . . 6
|
76 | 74, 75 | eqeqan12d 2638 |
. . . . 5
|
77 | 76 | adantl 482 |
. . . 4
mFS
|
78 | | ffn 6045 |
. . . . . . 7
|
79 | | ffn 6045 |
. . . . . . 7
|
80 | | eqfnfv 6311 |
. . . . . . 7
|
81 | 78, 79, 80 | syl2an 494 |
. . . . . 6
|
82 | 27, 44, 81 | syl2an 494 |
. . . . 5
|
83 | 82 | adantl 482 |
. . . 4
mFS
|
84 | 73, 77, 83 | 3imtr4d 283 |
. . 3
mFS
|
85 | 84 | ralrimivva 2971 |
. 2
mFS
|
86 | | dff13 6512 |
. 2
|
87 | 8, 85, 86 | sylanbrc 698 |
1
mFS
|