Metamath Proof Explorer


Theorem functhinclem3

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 φXB
functhinclem3.y φYB
functhinclem3.m φMXHY
functhinclem3.g φG=xB,yBxHy×FxJFy
functhinclem3.1 φFXJFY=XHY=
functhinclem3.2 φ*nnFXJFY
Assertion functhinclem3 φXGYMFXJFY

Proof

Step Hyp Ref Expression
1 functhinclem3.x φXB
2 functhinclem3.y φYB
3 functhinclem3.m φMXHY
4 functhinclem3.g φG=xB,yBxHy×FxJFy
5 functhinclem3.1 φFXJFY=XHY=
6 functhinclem3.2 φ*nnFXJFY
7 simprl φx=Xy=Yx=X
8 simprr φx=Xy=Yy=Y
9 7 8 oveq12d φx=Xy=YxHy=XHY
10 7 fveq2d φx=Xy=YFx=FX
11 8 fveq2d φx=Xy=YFy=FY
12 10 11 oveq12d φx=Xy=YFxJFy=FXJFY
13 9 12 xpeq12d φx=Xy=YxHy×FxJFy=XHY×FXJFY
14 ovex XHYV
15 ovex FXJFYV
16 14 15 xpex XHY×FXJFYV
17 16 a1i φXHY×FXJFYV
18 4 13 1 2 17 ovmpod φXGY=XHY×FXJFY
19 eqid XHY×FXJFY=XHY×FXJFY
20 19 5 6 mofeu φXGY:XHYFXJFYXGY=XHY×FXJFY
21 18 20 mpbird φXGY:XHYFXJFY
22 21 3 ffvelcdmd φXGYMFXJFY