Metamath Proof Explorer

Theorem isnat3

Description: A natural transformation is an exact component function with typed values satisfying naturality. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypotheses isnat3.n 
|- N = ( C Nat D )
isnat3.b 
|- B = ( Base ` C )
isnat3.h 
|- H = ( Hom ` C )
isnat3.j 
|- J = ( Hom ` D )
isnat3.o 
|- .x. = ( comp ` D )
isnat3.f 
|- ( ph -> F e. ( C Func D ) )
isnat3.g 
|- ( ph -> G e. ( C Func D ) )
Assertion isnat3 
|- ( ph -> ( A e. ( F N G ) <-> ( A = ( x e. B |-> ( A ` x ) ) /\ A. x e. B ( A ` x ) e. ( ( ( 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 isnat3.n 
 |-  N = ( C Nat D )
2 isnat3.b 
 |-  B = ( Base ` C )
3 isnat3.h 
 |-  H = ( Hom ` C )
4 isnat3.j 
 |-  J = ( Hom ` D )
5 isnat3.o 
 |-  .x. = ( comp ` D )
6 isnat3.f 
 |-  ( ph -> F e. ( C Func D ) )
7 isnat3.g 
 |-  ( ph -> G e. ( C Func D ) )
8 1 2 3 4 5 6 7 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 ) ) ) ) )
9 anass 
 |-  ( ( ( A = ( x e. B |-> ( A ` x ) ) /\ A. x e. B ( A ` x ) e. ( ( ( 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 ) ) ) <-> ( A = ( x e. B |-> ( A ` x ) ) /\ ( A. x e. B ( A ` x ) e. ( ( ( 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 ) ) ) ) )
10 2 fvexi 
 |-  B e. _V
11 10 elixpmpt 
 |-  ( A e. X_ x e. B ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) <-> ( A = ( x e. B |-> ( A ` x ) ) /\ A. x e. B ( A ` x ) e. ( ( ( 1st ` F ) ` x ) J ( ( 1st ` G ) ` x ) ) ) )
12 11 anbi1i 
 |-  ( ( 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 ) ) ) <-> ( ( A = ( x e. B |-> ( A ` x ) ) /\ A. x e. B ( A ` x ) e. ( ( ( 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 ) ) ) )
13 3anass 
 |-  ( ( A = ( x e. B |-> ( A ` x ) ) /\ A. x e. B ( A ` x ) e. ( ( ( 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 ) ) ) <-> ( A = ( x e. B |-> ( A ` x ) ) /\ ( A. x e. B ( A ` x ) e. ( ( ( 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 ) ) ) ) )
14 9 12 13 3bitr4i 
 |-  ( ( 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 ) ) ) <-> ( A = ( x e. B |-> ( A ` x ) ) /\ A. x e. B ( A ` x ) e. ( ( ( 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 ) ) ) )
15 8 14 bitrdi 
 |-  ( ph -> ( A e. ( F N G ) <-> ( A = ( x e. B |-> ( A ` x ) ) /\ A. x e. B ( A ` x ) e. ( ( ( 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 ) ) ) ) )