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 
|- ( ph -> X e. B )
functhinclem3.y 
|- ( ph -> Y e. B )
functhinclem3.m 
|- ( ph -> M e. ( X H Y ) )
functhinclem3.g 
|- ( ph -> G = ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) ) )
functhinclem3.1 
|- ( ph -> ( ( ( F ` X ) J ( F ` Y ) ) = (/) -> ( X H Y ) = (/) ) )
functhinclem3.2 
|- ( ph -> E* n n e. ( ( F ` X ) J ( F ` Y ) ) )
Assertion functhinclem3 
|- ( ph -> ( ( X G Y ) ` M ) e. ( ( F ` X ) J ( F ` Y ) ) )

Proof

Step Hyp Ref Expression
1 functhinclem3.x 
 |-  ( ph -> X e. B )
2 functhinclem3.y 
 |-  ( ph -> Y e. B )
3 functhinclem3.m 
 |-  ( ph -> M e. ( X H Y ) )
4 functhinclem3.g 
 |-  ( ph -> G = ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) ) )
5 functhinclem3.1 
 |-  ( ph -> ( ( ( F ` X ) J ( F ` Y ) ) = (/) -> ( X H Y ) = (/) ) )
6 functhinclem3.2 
 |-  ( ph -> E* n n e. ( ( F ` X ) J ( F ` Y ) ) )
7 simprl 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> x = X )
8 simprr 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> y = Y )
9 7 8 oveq12d 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( x H y ) = ( X H Y ) )
10 7 fveq2d 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( F ` x ) = ( F ` X ) )
11 8 fveq2d 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( F ` y ) = ( F ` Y ) )
12 10 11 oveq12d 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( F ` x ) J ( F ` y ) ) = ( ( F ` X ) J ( F ` Y ) ) )
13 9 12 xpeq12d 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) = ( ( X H Y ) X. ( ( F ` X ) J ( F ` Y ) ) ) )
14 ovex 
 |-  ( X H Y ) e. _V
15 ovex 
 |-  ( ( F ` X ) J ( F ` Y ) ) e. _V
16 14 15 xpex 
 |-  ( ( X H Y ) X. ( ( F ` X ) J ( F ` Y ) ) ) e. _V
17 16 a1i 
 |-  ( ph -> ( ( X H Y ) X. ( ( F ` X ) J ( F ` Y ) ) ) e. _V )
18 4 13 1 2 17 ovmpod 
 |-  ( ph -> ( X G Y ) = ( ( X H Y ) X. ( ( F ` X ) J ( F ` Y ) ) ) )
19 eqid 
 |-  ( ( X H Y ) X. ( ( F ` X ) J ( F ` Y ) ) ) = ( ( X H Y ) X. ( ( F ` X ) J ( F ` Y ) ) )
20 19 5 6 mofeu 
 |-  ( ph -> ( ( X G Y ) : ( X H Y ) --> ( ( F ` X ) J ( F ` Y ) ) <-> ( X G Y ) = ( ( X H Y ) X. ( ( F ` X ) J ( F ` Y ) ) ) ) )
21 18 20 mpbird 
 |-  ( ph -> ( X G Y ) : ( X H Y ) --> ( ( F ` X ) J ( F ` Y ) ) )
22 21 3 ffvelrnd 
 |-  ( ph -> ( ( X G Y ) ` M ) e. ( ( F ` X ) J ( F ` Y ) ) )