Description: Lemma for functhinc . The mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | functhinclem3.x | |
|
functhinclem3.y | |
||
functhinclem3.m | |
||
functhinclem3.g | |
||
functhinclem3.1 | |
||
functhinclem3.2 | |
||
Assertion | functhinclem3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | functhinclem3.x | |
|
2 | functhinclem3.y | |
|
3 | functhinclem3.m | |
|
4 | functhinclem3.g | |
|
5 | functhinclem3.1 | |
|
6 | functhinclem3.2 | |
|
7 | simprl | |
|
8 | simprr | |
|
9 | 7 8 | oveq12d | |
10 | 7 | fveq2d | |
11 | 8 | fveq2d | |
12 | 10 11 | oveq12d | |
13 | 9 12 | xpeq12d | |
14 | ovex | |
|
15 | ovex | |
|
16 | 14 15 | xpex | |
17 | 16 | a1i | |
18 | 4 13 1 2 17 | ovmpod | |
19 | eqid | |
|
20 | 19 5 6 | mofeu | |
21 | 18 20 | mpbird | |
22 | 21 3 | ffvelcdmd | |