Step | Hyp | Ref
| Expression |
1 | | mrsubccat.s |
. . . 4
mRSubst |
2 | | mrsubccat.r |
. . . 4
mREx |
3 | 1, 2 | mrsubf 31414 |
. . 3
|
4 | | mrsubcn.v |
. . . . 5
mVR |
5 | | mrsubcn.c |
. . . . 5
mCN |
6 | 1, 2, 4, 5 | mrsubcn 31416 |
. . . 4
|
7 | 6 | ralrimiva 2966 |
. . 3
|
8 | 1, 2 | mrsubccat 31415 |
. . . . 5
++ ++ |
9 | 8 | 3expb 1266 |
. . . 4
++ ++
|
10 | 9 | ralrimivva 2971 |
. . 3
++ ++
|
11 | 3, 7, 10 | 3jca 1242 |
. 2
++ ++ |
12 | 5, 4, 2 | mrexval 31398 |
. . . . . . 7
Word |
13 | 12 | adantr 481 |
. . . . . 6
++ ++
Word
|
14 | | s1eq 13380 |
. . . . . . . . . . . . 13
|
15 | 14 | fveq2d 6195 |
. . . . . . . . . . . 12
|
16 | | eqid 2622 |
. . . . . . . . . . . 12
|
17 | | fvex 6201 |
. . . . . . . . . . . 12
|
18 | 15, 16, 17 | fvmpt 6282 |
. . . . . . . . . . 11
|
19 | 18 | adantl 482 |
. . . . . . . . . 10
++ ++
|
20 | | difun2 4048 |
. . . . . . . . . . . . . . 15
|
21 | 20 | eleq2i 2693 |
. . . . . . . . . . . . . 14
|
22 | | eldif 3584 |
. . . . . . . . . . . . . 14
|
23 | 21, 22 | bitr3i 266 |
. . . . . . . . . . . . 13
|
24 | | simpr2 1068 |
. . . . . . . . . . . . . 14
++ ++
|
25 | | s1eq 13380 |
. . . . . . . . . . . . . . . . 17
|
26 | 25 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
27 | 26, 25 | eqeq12d 2637 |
. . . . . . . . . . . . . . 15
|
28 | 27 | rspccva 3308 |
. . . . . . . . . . . . . 14
|
29 | 24, 28 | sylan 488 |
. . . . . . . . . . . . 13
++ ++
|
30 | 23, 29 | sylan2br 493 |
. . . . . . . . . . . 12
++ ++
|
31 | 30 | anassrs 680 |
. . . . . . . . . . 11
++ ++
|
32 | 31 | eqcomd 2628 |
. . . . . . . . . 10
++ ++
|
33 | 19, 32 | ifeqda 4121 |
. . . . . . . . 9
++ ++
|
34 | 33 | mpteq2dva 4744 |
. . . . . . . 8
++ ++
|
35 | 34 | coeq1d 5283 |
. . . . . . 7
++ ++
|
36 | 35 | oveq2d 6666 |
. . . . . 6
++ ++
freeMnd g freeMnd
g |
37 | 13, 36 | mpteq12dv 4733 |
. . . . 5
++ ++
freeMnd g Word freeMnd
g |
38 | | elun2 3781 |
. . . . . . . 8
|
39 | | simpr1 1067 |
. . . . . . . . . 10
++ ++
|
40 | 39 | adantr 481 |
. . . . . . . . 9
++ ++
|
41 | | simpr 477 |
. . . . . . . . . . 11
++ ++
|
42 | 41 | s1cld 13383 |
. . . . . . . . . 10
++ ++
Word
|
43 | 12 | ad2antrr 762 |
. . . . . . . . . 10
++ ++
Word
|
44 | 42, 43 | eleqtrrd 2704 |
. . . . . . . . 9
++ ++
|
45 | 40, 44 | ffvelrnd 6360 |
. . . . . . . 8
++ ++
|
46 | 38, 45 | sylan2 491 |
. . . . . . 7
++ ++
|
47 | 15 | cbvmptv 4750 |
. . . . . . 7
|
48 | 46, 47 | fmptd 6385 |
. . . . . 6
++ ++
|
49 | | ssid 3624 |
. . . . . 6
|
50 | | eqid 2622 |
. . . . . . 7
freeMnd
freeMnd
|
51 | 5, 4, 2, 1, 50 | mrsubfval 31405 |
. . . . . 6
freeMnd
g |
52 | 48, 49, 51 | sylancl 694 |
. . . . 5
++ ++
freeMnd g |
53 | | fvex 6201 |
. . . . . . . . . 10
mCN |
54 | 5, 53 | eqeltri 2697 |
. . . . . . . . 9
|
55 | | fvex 6201 |
. . . . . . . . . 10
mVR |
56 | 4, 55 | eqeltri 2697 |
. . . . . . . . 9
|
57 | 54, 56 | unex 6956 |
. . . . . . . 8
|
58 | 50 | frmdmnd 17396 |
. . . . . . . 8
freeMnd |
59 | 57, 58 | ax-mp 5 |
. . . . . . 7
freeMnd
|
60 | 59 | a1i 11 |
. . . . . 6
++ ++
freeMnd
|
61 | 57 | a1i 11 |
. . . . . 6
++ ++
|
62 | 45, 43 | eleqtrd 2703 |
. . . . . . 7
++ ++
Word
|
63 | | eqid 2622 |
. . . . . . 7
|
64 | 62, 63 | fmptd 6385 |
. . . . . 6
++ ++
Word |
65 | 13, 13 | feq23d 6040 |
. . . . . . . 8
++ ++
Word
Word |
66 | 39, 65 | mpbid 222 |
. . . . . . 7
++ ++
Word
Word |
67 | | simpr3 1069 |
. . . . . . . 8
++ ++
++ ++ |
68 | | simprl 794 |
. . . . . . . . . . . . . . 15
|
69 | 12 | adantr 481 |
. . . . . . . . . . . . . . . 16
Word
|
70 | 69 | adantr 481 |
. . . . . . . . . . . . . . 15
Word |
71 | 68, 70 | eleqtrd 2703 |
. . . . . . . . . . . . . 14
Word |
72 | | simprr 796 |
. . . . . . . . . . . . . . 15
|
73 | 72, 70 | eleqtrd 2703 |
. . . . . . . . . . . . . 14
Word
|
74 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
freeMnd freeMnd |
75 | 50, 74 | frmdbas 17389 |
. . . . . . . . . . . . . . . . 17
freeMnd
Word
|
76 | 57, 75 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
freeMnd Word |
77 | 76 | eqcomi 2631 |
. . . . . . . . . . . . . . 15
Word freeMnd |
78 | | eqid 2622 |
. . . . . . . . . . . . . . 15
freeMnd freeMnd |
79 | 50, 77, 78 | frmdadd 17392 |
. . . . . . . . . . . . . 14
Word
Word freeMnd ++ |
80 | 71, 73, 79 | syl2anc 693 |
. . . . . . . . . . . . 13
freeMnd ++ |
81 | 80 | fveq2d 6195 |
. . . . . . . . . . . 12
freeMnd ++ |
82 | | ffvelrn 6357 |
. . . . . . . . . . . . . . 15
|
83 | 82 | ad2ant2lr 784 |
. . . . . . . . . . . . . 14
|
84 | 83, 70 | eleqtrd 2703 |
. . . . . . . . . . . . 13
Word
|
85 | | ffvelrn 6357 |
. . . . . . . . . . . . . . 15
|
86 | 85 | ad2ant2l 782 |
. . . . . . . . . . . . . 14
|
87 | 86, 70 | eleqtrd 2703 |
. . . . . . . . . . . . 13
Word
|
88 | 50, 77, 78 | frmdadd 17392 |
. . . . . . . . . . . . 13
Word
Word freeMnd ++ |
89 | 84, 87, 88 | syl2anc 693 |
. . . . . . . . . . . 12
freeMnd ++ |
90 | 81, 89 | eqeq12d 2637 |
. . . . . . . . . . 11
freeMnd freeMnd
++ ++ |
91 | 90 | 2ralbidva 2988 |
. . . . . . . . . 10
freeMnd freeMnd
++ ++ |
92 | 69 | raleqdv 3144 |
. . . . . . . . . . 11
freeMnd freeMnd
Word freeMnd freeMnd |
93 | 69, 92 | raleqbidv 3152 |
. . . . . . . . . 10
freeMnd freeMnd
Word Word freeMnd freeMnd |
94 | 91, 93 | bitr3d 270 |
. . . . . . . . 9
++ ++
Word Word freeMnd freeMnd |
95 | 94 | 3ad2antr1 1226 |
. . . . . . . 8
++ ++
++ ++
Word Word freeMnd freeMnd |
96 | 67, 95 | mpbid 222 |
. . . . . . 7
++ ++
Word Word freeMnd freeMnd |
97 | | wrd0 13330 |
. . . . . . . . . . . 12
Word
|
98 | | ffvelrn 6357 |
. . . . . . . . . . . 12
Word Word Word
Word |
99 | 66, 97, 98 | sylancl 694 |
. . . . . . . . . . 11
++ ++
Word
|
100 | | lencl 13324 |
. . . . . . . . . . 11
Word
|
101 | 99, 100 | syl 17 |
. . . . . . . . . 10
++ ++
|
102 | 101 | nn0cnd 11353 |
. . . . . . . . 9
++ ++
|
103 | | 0cnd 10033 |
. . . . . . . . 9
++ ++
|
104 | 102 | addid1d 10236 |
. . . . . . . . . 10
++ ++
|
105 | 97, 13 | syl5eleqr 2708 |
. . . . . . . . . . . 12
++ ++
|
106 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
++ ++ |
107 | 106 | fveq2d 6195 |
. . . . . . . . . . . . . 14
++ ++ |
108 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
109 | 108 | oveq1d 6665 |
. . . . . . . . . . . . . 14
++ ++ |
110 | 107, 109 | eqeq12d 2637 |
. . . . . . . . . . . . 13
++ ++
++ ++ |
111 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
++ ++ |
112 | | ccatlid 13369 |
. . . . . . . . . . . . . . . . 17
Word
++ |
113 | 97, 112 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
++
|
114 | 111, 113 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
++ |
115 | 114 | fveq2d 6195 |
. . . . . . . . . . . . . 14
++ |
116 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
117 | 116 | oveq2d 6666 |
. . . . . . . . . . . . . 14
++ ++ |
118 | 115, 117 | eqeq12d 2637 |
. . . . . . . . . . . . 13
++ ++ ++ |
119 | 110, 118 | rspc2va 3323 |
. . . . . . . . . . . 12
++
++ ++ |
120 | 105, 105,
67, 119 | syl21anc 1325 |
. . . . . . . . . . 11
++ ++
++ |
121 | 120 | fveq2d 6195 |
. . . . . . . . . 10
++ ++
++ |
122 | | ccatlen 13360 |
. . . . . . . . . . 11
Word
Word
++ |
123 | 99, 99, 122 | syl2anc 693 |
. . . . . . . . . 10
++ ++
++ |
124 | 104, 121,
123 | 3eqtrrd 2661 |
. . . . . . . . 9
++ ++
|
125 | 102, 102,
103, 124 | addcanad 10241 |
. . . . . . . 8
++ ++
|
126 | | fvex 6201 |
. . . . . . . . 9
|
127 | | hasheq0 13154 |
. . . . . . . . 9
|
128 | 126, 127 | ax-mp 5 |
. . . . . . . 8
|
129 | 125, 128 | sylib 208 |
. . . . . . 7
++ ++
|
130 | 59, 59 | pm3.2i 471 |
. . . . . . . 8
freeMnd freeMnd |
131 | 50 | frmd0 17397 |
. . . . . . . . 9
freeMnd
|
132 | 77, 77, 78, 78, 131, 131 | ismhm 17337 |
. . . . . . . 8
freeMnd
MndHom freeMnd freeMnd
freeMnd Word Word
Word Word freeMnd freeMnd |
133 | 130, 132 | mpbiran 953 |
. . . . . . 7
freeMnd
MndHom freeMnd Word
Word
Word Word freeMnd freeMnd |
134 | 66, 96, 129, 133 | syl3anbrc 1246 |
. . . . . 6
++ ++
freeMnd MndHom freeMnd |
135 | | eqid 2622 |
. . . . . . . . . 10
varFMnd
varFMnd
|
136 | 135 | vrmdf 17395 |
. . . . . . . . 9
varFMnd
Word |
137 | 57, 136 | ax-mp 5 |
. . . . . . . 8
varFMnd
Word |
138 | | fcompt 6400 |
. . . . . . . 8
Word Word varFMnd Word
varFMnd varFMnd |
139 | 66, 137, 138 | sylancl 694 |
. . . . . . 7
++ ++
varFMnd varFMnd |
140 | 135 | vrmdval 17394 |
. . . . . . . . . 10
varFMnd |
141 | 61, 140 | sylan 488 |
. . . . . . . . 9
++ ++
varFMnd
|
142 | 141 | fveq2d 6195 |
. . . . . . . 8
++ ++
varFMnd |
143 | 142 | mpteq2dva 4744 |
. . . . . . 7
++ ++
varFMnd |
144 | 139, 143 | eqtrd 2656 |
. . . . . 6
++ ++
varFMnd |
145 | 50, 77, 135 | frmdup3lem 17403 |
. . . . . 6
freeMnd
Word freeMnd
MndHom freeMnd varFMnd
Word freeMnd
g |
146 | 60, 61, 64, 134, 144, 145 | syl32anc 1334 |
. . . . 5
++ ++
Word
freeMnd
g |
147 | 37, 52, 146 | 3eqtr4rd 2667 |
. . . 4
++ ++
|
148 | 4, 2, 1 | mrsubff 31409 |
. . . . . . 7
|
149 | | ffn 6045 |
. . . . . . 7
|
150 | 148, 149 | syl 17 |
. . . . . 6
|
151 | 150 | adantr 481 |
. . . . 5
++ ++
|
152 | | fvex 6201 |
. . . . . . . 8
mREx |
153 | 2, 152 | eqeltri 2697 |
. . . . . . 7
|
154 | | elpm2r 7875 |
. . . . . . 7
|
155 | 153, 56, 154 | mpanl12 718 |
. . . . . 6
|
156 | 48, 49, 155 | sylancl 694 |
. . . . 5
++ ++
|
157 | | fnfvelrn 6356 |
. . . . 5
|
158 | 151, 156,
157 | syl2anc 693 |
. . . 4
++ ++
|
159 | 147, 158 | eqeltrd 2701 |
. . 3
++ ++
|
160 | 159 | ex 450 |
. 2
++ ++
|
161 | 11, 160 | impbid2 216 |
1
++ ++
|