Metamath Proof Explorer

Theorem isnat2

Description: Property of being a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses natfval.1 
|- N = ( C Nat D )
natfval.b 
|- B = ( Base ` C )
natfval.h 
|- H = ( Hom ` C )
natfval.j 
|- J = ( Hom ` D )
natfval.o 
|- .x. = ( comp ` D )
isnat2.f 
|- ( ph -> F e. ( C Func D ) )
isnat2.g 
|- ( ph -> G e. ( C Func D ) )
Assertion isnat2 
|- ( ph -> ( A e. ( F N G ) <-> ( A e. X_ x e. B ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x H y ) ( ( A ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. .x. ( ( 1st ` G ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` h ) ) = ( ( ( x ( 2nd ` G ) y ) ` h ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` G ) ` y ) ) ( A ` x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 natfval.1 
 |-  N = ( C Nat D )
2 natfval.b 
 |-  B = ( Base ` C )
3 natfval.h 
 |-  H = ( Hom ` C )
4 natfval.j 
 |-  J = ( Hom ` D )
5 natfval.o 
 |-  .x. = ( comp ` D )
6 isnat2.f 
 |-  ( ph -> F e. ( C Func D ) )
7 isnat2.g 
 |-  ( ph -> G e. ( C Func D ) )
8 relfunc 
 |-  Rel ( C Func D )
9 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
10 8 6 9 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
11 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
12 8 7 11 sylancr 
 |-  ( ph -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
13 10 12 oveq12d 
 |-  ( ph -> ( F N G ) = ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
14 13 eleq2d 
 |-  ( ph -> ( A e. ( F N G ) <-> A e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) ) )
15 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
16 8 6 15 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
17 1st2ndbr 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
18 8 7 17 sylancr 
 |-  ( ph -> ( 1st ` G ) ( C Func D ) ( 2nd ` G ) )
19 1 2 3 4 5 16 18 isnat 
 |-  ( ph -> ( A e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) <-> ( A e. X_ x e. B ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x H y ) ( ( A ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. .x. ( ( 1st ` G ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` h ) ) = ( ( ( x ( 2nd ` G ) y ) ` h ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` G ) ` y ) ) ( A ` x ) ) ) ) )
20 14 19 bitrd 
 |-  ( ph -> ( A e. ( F N G ) <-> ( A e. X_ x e. B ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x H y ) ( ( A ` y ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` F ) ` y ) >. .x. ( ( 1st ` G ) ` y ) ) ( ( x ( 2nd ` F ) y ) ` h ) ) = ( ( ( x ( 2nd ` G ) y ) ` h ) ( <. ( ( 1st ` F ) ` x ) , ( ( 1st ` G ) ` x ) >. .x. ( ( 1st ` G ) ` y ) ) ( A ` x ) ) ) ) )