Metamath Proof Explorer

Theorem funcf2lem

Description: A utility theorem for proving equivalence of "is a functor". (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Assertion funcf2lem 
|- ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G e. _V /\ G Fn ( B X. B ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) )

Proof

Step Hyp Ref Expression
1 elixp2 
 |-  ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G e. _V /\ G Fn ( B X. B ) /\ A. z e. ( B X. B ) ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) )
2 fveq2 
 |-  ( z = <. x , y >. -> ( G ` z ) = ( G ` <. x , y >. ) )
3 df-ov 
 |-  ( x G y ) = ( G ` <. x , y >. )
4 2 3 eqtr4di 
 |-  ( z = <. x , y >. -> ( G ` z ) = ( x G y ) )
5 vex 
 |-  x e. _V
6 vex 
 |-  y e. _V
7 5 6 op1std 
 |-  ( z = <. x , y >. -> ( 1st ` z ) = x )
8 7 fveq2d 
 |-  ( z = <. x , y >. -> ( F ` ( 1st ` z ) ) = ( F ` x ) )
9 5 6 op2ndd 
 |-  ( z = <. x , y >. -> ( 2nd ` z ) = y )
10 9 fveq2d 
 |-  ( z = <. x , y >. -> ( F ` ( 2nd ` z ) ) = ( F ` y ) )
11 8 10 oveq12d 
 |-  ( z = <. x , y >. -> ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) = ( ( F ` x ) J ( F ` y ) ) )
12 fveq2 
 |-  ( z = <. x , y >. -> ( H ` z ) = ( H ` <. x , y >. ) )
13 df-ov 
 |-  ( x H y ) = ( H ` <. x , y >. )
14 12 13 eqtr4di 
 |-  ( z = <. x , y >. -> ( H ` z ) = ( x H y ) )
15 11 14 oveq12d 
 |-  ( z = <. x , y >. -> ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) = ( ( ( F ` x ) J ( F ` y ) ) ^m ( x H y ) ) )
16 4 15 eleq12d 
 |-  ( z = <. x , y >. -> ( ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( x G y ) e. ( ( ( F ` x ) J ( F ` y ) ) ^m ( x H y ) ) ) )
17 ovex 
 |-  ( ( F ` x ) J ( F ` y ) ) e. _V
18 ovex 
 |-  ( x H y ) e. _V
19 17 18 elmap 
 |-  ( ( x G y ) e. ( ( ( F ` x ) J ( F ` y ) ) ^m ( x H y ) ) <-> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) )
20 16 19 bitrdi 
 |-  ( z = <. x , y >. -> ( ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) )
21 20 ralxp 
 |-  ( A. z e. ( B X. B ) ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) )
22 21 3anbi3i 
 |-  ( ( G e. _V /\ G Fn ( B X. B ) /\ A. z e. ( B X. B ) ( G ` z ) e. ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) ) <-> ( G e. _V /\ G Fn ( B X. B ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) )
23 1 22 bitri 
 |-  ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) J ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G e. _V /\ G Fn ( B X. B ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) ) )