Metamath Proof Explorer

Theorem fucofulem2

Description: Lemma for proving functor theorems. Maybe consider eufnfv to prove the uniqueness of a functor. (Contributed by Zhi Wang, 25-Sep-2025)

Ref Expression
Hypotheses fucofulem2.b 
|- B = ( ( D Func E ) X. ( C Func D ) )
fucofulem2.h 
|- H = ( Hom ` ( ( D FuncCat E ) Xc. ( C FuncCat D ) ) )
Assertion fucofulem2 
|- ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) ( C Nat E ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G = ( u e. B , v e. B |-> ( u G v ) ) /\ A. m e. B A. n e. B ( ( m G n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m G n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m G n ) q ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fucofulem2.b 
 |-  B = ( ( D Func E ) X. ( C Func D ) )
2 fucofulem2.h 
 |-  H = ( Hom ` ( ( D FuncCat E ) Xc. ( C FuncCat D ) ) )
3 eqid 
 |-  ( ( D FuncCat E ) Xc. ( C FuncCat D ) ) = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
4 3 xpcfucbas 
 |-  ( ( D Func E ) X. ( C Func D ) ) = ( Base ` ( ( D FuncCat E ) Xc. ( C FuncCat D ) ) )
5 1 4 eqtri 
 |-  B = ( Base ` ( ( D FuncCat E ) Xc. ( C FuncCat D ) ) )
6 5 funcf2lem2 
 |-  ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) ( C Nat E ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G Fn ( B X. B ) /\ A. m e. B A. n e. B ( m G n ) : ( m H n ) --> ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) )
7 fnov 
 |-  ( G Fn ( B X. B ) <-> G = ( u e. B , v e. B |-> ( u G v ) ) )
8 ffnfv 
 |-  ( ( m G n ) : ( m H n ) --> ( ( F ` m ) ( C Nat E ) ( F ` n ) ) <-> ( ( m G n ) Fn ( m H n ) /\ A. r e. ( m H n ) ( ( m G n ) ` r ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) )
9 simpl 
 |-  ( ( m e. B /\ n e. B ) -> m e. B )
10 simpr 
 |-  ( ( m e. B /\ n e. B ) -> n e. B )
11 3 5 2 9 10 xpcfuchom 
 |-  ( ( m e. B /\ n e. B ) -> ( m H n ) = ( ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) X. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ) )
12 11 fneq2d 
 |-  ( ( m e. B /\ n e. B ) -> ( ( m G n ) Fn ( m H n ) <-> ( m G n ) Fn ( ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) X. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ) ) )
13 fnov 
 |-  ( ( m G n ) Fn ( ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) X. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ) <-> ( m G n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m G n ) a ) ) )
14 12 13 bitrdi 
 |-  ( ( m e. B /\ n e. B ) -> ( ( m G n ) Fn ( m H n ) <-> ( m G n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m G n ) a ) ) ) )
15 11 raleqdv 
 |-  ( ( m e. B /\ n e. B ) -> ( A. r e. ( m H n ) ( ( m G n ) ` r ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) <-> A. r e. ( ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) X. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ) ( ( m G n ) ` r ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) )
16 fveq2 
 |-  ( r = <. p , q >. -> ( ( m G n ) ` r ) = ( ( m G n ) ` <. p , q >. ) )
17 df-ov 
 |-  ( p ( m G n ) q ) = ( ( m G n ) ` <. p , q >. )
18 16 17 eqtr4di 
 |-  ( r = <. p , q >. -> ( ( m G n ) ` r ) = ( p ( m G n ) q ) )
19 18 eleq1d 
 |-  ( r = <. p , q >. -> ( ( ( m G n ) ` r ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) <-> ( p ( m G n ) q ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) )
20 19 ralxp 
 |-  ( A. r e. ( ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) X. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ) ( ( m G n ) ` r ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) <-> A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m G n ) q ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) )
21 15 20 bitrdi 
 |-  ( ( m e. B /\ n e. B ) -> ( A. r e. ( m H n ) ( ( m G n ) ` r ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) <-> A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m G n ) q ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) )
22 14 21 anbi12d 
 |-  ( ( m e. B /\ n e. B ) -> ( ( ( m G n ) Fn ( m H n ) /\ A. r e. ( m H n ) ( ( m G n ) ` r ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) <-> ( ( m G n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m G n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m G n ) q ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) ) )
23 8 22 bitrid 
 |-  ( ( m e. B /\ n e. B ) -> ( ( m G n ) : ( m H n ) --> ( ( F ` m ) ( C Nat E ) ( F ` n ) ) <-> ( ( m G n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m G n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m G n ) q ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) ) )
24 23 adantl 
 |-  ( ( T. /\ ( m e. B /\ n e. B ) ) -> ( ( m G n ) : ( m H n ) --> ( ( F ` m ) ( C Nat E ) ( F ` n ) ) <-> ( ( m G n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m G n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m G n ) q ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) ) )
25 24 2ralbidva 
 |-  ( T. -> ( A. m e. B A. n e. B ( m G n ) : ( m H n ) --> ( ( F ` m ) ( C Nat E ) ( F ` n ) ) <-> A. m e. B A. n e. B ( ( m G n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m G n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m G n ) q ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) ) )
26 25 mptru 
 |-  ( A. m e. B A. n e. B ( m G n ) : ( m H n ) --> ( ( F ` m ) ( C Nat E ) ( F ` n ) ) <-> A. m e. B A. n e. B ( ( m G n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m G n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m G n ) q ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) )
27 7 26 anbi12i 
 |-  ( ( G Fn ( B X. B ) /\ A. m e. B A. n e. B ( m G n ) : ( m H n ) --> ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) <-> ( G = ( u e. B , v e. B |-> ( u G v ) ) /\ A. m e. B A. n e. B ( ( m G n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m G n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m G n ) q ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) ) )
28 6 27 bitri 
 |-  ( G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) ( C Nat E ) ( F ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( G = ( u e. B , v e. B |-> ( u G v ) ) /\ A. m e. B A. n e. B ( ( m G n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m G n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m G n ) q ) e. ( ( F ` m ) ( C Nat E ) ( F ` n ) ) ) ) )