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 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
5 4 fucbas 
 |-  ( D Func E ) = ( Base ` ( D FuncCat E ) )
6 eqid 
 |-  ( C FuncCat D ) = ( C FuncCat D )
7 6 fucbas 
 |-  ( C Func D ) = ( Base ` ( C FuncCat D ) )
8 3 5 7 xpcbas 
 |-  ( ( D Func E ) X. ( C Func D ) ) = ( Base ` ( ( D FuncCat E ) Xc. ( C FuncCat D ) ) )
9 1 8 eqtri 
 |-  B = ( Base ` ( ( D FuncCat E ) Xc. ( C FuncCat D ) ) )
10 9 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 ) ) ) )
11 fnov 
 |-  ( G Fn ( B X. B ) <-> G = ( u e. B , v e. B |-> ( u G v ) ) )
12 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 ) ) ) )
13 eqid 
 |-  ( D Nat E ) = ( D Nat E )
14 4 13 fuchom 
 |-  ( D Nat E ) = ( Hom ` ( D FuncCat E ) )
15 eqid 
 |-  ( C Nat D ) = ( C Nat D )
16 6 15 fuchom 
 |-  ( C Nat D ) = ( Hom ` ( C FuncCat D ) )
17 simpl 
 |-  ( ( m e. B /\ n e. B ) -> m e. B )
18 simpr 
 |-  ( ( m e. B /\ n e. B ) -> n e. B )
19 3 9 14 16 2 17 18 xpchom 
 |-  ( ( m e. B /\ n e. B ) -> ( m H n ) = ( ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) X. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ) )
20 19 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 ) ) ) ) )
21 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 ) ) )
22 20 21 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 ) ) ) )
23 19 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 ) ) ) )
24 fveq2 
 |-  ( r = <. p , q >. -> ( ( m G n ) ` r ) = ( ( m G n ) ` <. p , q >. ) )
25 df-ov 
 |-  ( p ( m G n ) q ) = ( ( m G n ) ` <. p , q >. )
26 24 25 eqtr4di 
 |-  ( r = <. p , q >. -> ( ( m G n ) ` r ) = ( p ( m G n ) q ) )
27 26 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 ) ) ) )
28 27 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 ) ) )
29 23 28 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 ) ) ) )
30 22 29 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 ) ) ) ) )
31 12 30 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 ) ) ) ) )
32 31 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 ) ) ) ) )
33 32 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 ) ) ) ) )
34 33 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 ) ) ) )
35 11 34 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 ) ) ) ) )
36 10 35 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 ) ) ) ) )