Metamath Proof Explorer

Theorem isnatd

Description: Property of being a natural transformation; deduction form. (Contributed by Zhi Wang, 29-Sep-2025)

Ref Expression
Hypotheses isnatd.1 
|- N = ( C Nat D )
isnatd.b 
|- B = ( Base ` C )
isnatd.h 
|- H = ( Hom ` C )
isnatd.j 
|- J = ( Hom ` D )
isnatd.o 
|- .x. = ( comp ` D )
isnatd.f 
|- ( ph -> F ( C Func D ) G )
isnatd.g 
|- ( ph -> K ( C Func D ) L )
isnatd.a 
|- ( ph -> A Fn B )
isnatd.2 
|- ( ( ph /\ x e. B ) -> ( A ` x ) e. ( ( F ` x ) J ( K ` x ) ) )
isnatd.3 
|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ h e. ( x H y ) ) -> ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) )
Assertion isnatd 
|- ( ph -> A e. ( <. F , G >. N <. K , L >. ) )

Proof

Step Hyp Ref Expression
1 isnatd.1 
 |-  N = ( C Nat D )
2 isnatd.b 
 |-  B = ( Base ` C )
3 isnatd.h 
 |-  H = ( Hom ` C )
4 isnatd.j 
 |-  J = ( Hom ` D )
5 isnatd.o 
 |-  .x. = ( comp ` D )
6 isnatd.f 
 |-  ( ph -> F ( C Func D ) G )
7 isnatd.g 
 |-  ( ph -> K ( C Func D ) L )
8 isnatd.a 
 |-  ( ph -> A Fn B )
9 isnatd.2 
 |-  ( ( ph /\ x e. B ) -> ( A ` x ) e. ( ( F ` x ) J ( K ` x ) ) )
10 isnatd.3 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ h e. ( x H y ) ) -> ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) )
11 dffn5 
 |-  ( A Fn B <-> A = ( x e. B |-> ( A ` x ) ) )
12 8 11 sylib 
 |-  ( ph -> A = ( x e. B |-> ( A ` x ) ) )
13 2 fvexi 
 |-  B e. _V
14 13 mptex 
 |-  ( x e. B |-> ( A ` x ) ) e. _V
15 12 14 eqeltrdi 
 |-  ( ph -> A e. _V )
16 9 ralrimiva 
 |-  ( ph -> A. x e. B ( A ` x ) e. ( ( F ` x ) J ( K ` x ) ) )
17 elixp2 
 |-  ( A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) <-> ( A e. _V /\ A Fn B /\ A. x e. B ( A ` x ) e. ( ( F ` x ) J ( K ` x ) ) ) )
18 15 8 16 17 syl3anbrc 
 |-  ( ph -> A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) )
19 10 ralrimiva 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> A. h e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) )
20 19 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B A. h e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) )
21 1 2 3 4 5 6 7 isnat 
 |-  ( ph -> ( A e. ( <. F , G >. N <. K , L >. ) <-> ( A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x H y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. .x. ( K ` y ) ) ( ( x G y ) ` h ) ) = ( ( ( x L y ) ` h ) ( <. ( F ` x ) , ( K ` x ) >. .x. ( K ` y ) ) ( A ` x ) ) ) ) )
22 18 20 21 mpbir2and 
 |-  ( ph -> A e. ( <. F , G >. N <. K , L >. ) )