Metamath Proof Explorer

Theorem fuco22nat

Description: The composed natural transformation is a natural transformation. (Contributed by Zhi Wang, 2-Oct-2025)

Ref Expression
Hypotheses fuco22nat.o 
|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
fuco22nat.a 
|- ( ph -> A e. ( F ( C Nat D ) M ) )
fuco22nat.b 
|- ( ph -> B e. ( K ( D Nat E ) R ) )
fuco22nat.u 
|- ( ph -> U = <. K , F >. )
fuco22nat.v 
|- ( ph -> V = <. R , M >. )
Assertion fuco22nat 
|- ( ph -> ( B ( U P V ) A ) e. ( ( O ` U ) ( C Nat E ) ( O ` V ) ) )

Proof

Step Hyp Ref Expression
1 fuco22nat.o 
 |-  ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
2 fuco22nat.a 
 |-  ( ph -> A e. ( F ( C Nat D ) M ) )
3 fuco22nat.b 
 |-  ( ph -> B e. ( K ( D Nat E ) R ) )
4 fuco22nat.u 
 |-  ( ph -> U = <. K , F >. )
5 fuco22nat.v 
 |-  ( ph -> V = <. R , M >. )
6 eqid 
 |-  ( C Nat D ) = ( C Nat D )
7 6 2 nat1st2nd 
 |-  ( ph -> A e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( C Nat D ) <. ( 1st ` M ) , ( 2nd ` M ) >. ) )
8 eqid 
 |-  ( D Nat E ) = ( D Nat E )
9 8 3 nat1st2nd 
 |-  ( ph -> B e. ( <. ( 1st ` K ) , ( 2nd ` K ) >. ( D Nat E ) <. ( 1st ` R ) , ( 2nd ` R ) >. ) )
10 relfunc 
 |-  Rel ( D Func E )
11 8 natrcl 
 |-  ( B e. ( K ( D Nat E ) R ) -> ( K e. ( D Func E ) /\ R e. ( D Func E ) ) )
12 3 11 syl 
 |-  ( ph -> ( K e. ( D Func E ) /\ R e. ( D Func E ) ) )
13 12 simpld 
 |-  ( ph -> K e. ( D Func E ) )
14 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ K e. ( D Func E ) ) -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
15 10 13 14 sylancr 
 |-  ( ph -> K = <. ( 1st ` K ) , ( 2nd ` K ) >. )
16 relfunc 
 |-  Rel ( C Func D )
17 6 natrcl 
 |-  ( A e. ( F ( C Nat D ) M ) -> ( F e. ( C Func D ) /\ M e. ( C Func D ) ) )
18 2 17 syl 
 |-  ( ph -> ( F e. ( C Func D ) /\ M e. ( C Func D ) ) )
19 18 simpld 
 |-  ( ph -> F e. ( C Func D ) )
20 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
21 16 19 20 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
22 15 21 opeq12d 
 |-  ( ph -> <. K , F >. = <. <. ( 1st ` K ) , ( 2nd ` K ) >. , <. ( 1st ` F ) , ( 2nd ` F ) >. >. )
23 4 22 eqtrd 
 |-  ( ph -> U = <. <. ( 1st ` K ) , ( 2nd ` K ) >. , <. ( 1st ` F ) , ( 2nd ` F ) >. >. )
24 12 simprd 
 |-  ( ph -> R e. ( D Func E ) )
25 1st2nd 
 |-  ( ( Rel ( D Func E ) /\ R e. ( D Func E ) ) -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. )
26 10 24 25 sylancr 
 |-  ( ph -> R = <. ( 1st ` R ) , ( 2nd ` R ) >. )
27 18 simprd 
 |-  ( ph -> M e. ( C Func D ) )
28 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ M e. ( C Func D ) ) -> M = <. ( 1st ` M ) , ( 2nd ` M ) >. )
29 16 27 28 sylancr 
 |-  ( ph -> M = <. ( 1st ` M ) , ( 2nd ` M ) >. )
30 26 29 opeq12d 
 |-  ( ph -> <. R , M >. = <. <. ( 1st ` R ) , ( 2nd ` R ) >. , <. ( 1st ` M ) , ( 2nd ` M ) >. >. )
31 5 30 eqtrd 
 |-  ( ph -> V = <. <. ( 1st ` R ) , ( 2nd ` R ) >. , <. ( 1st ` M ) , ( 2nd ` M ) >. >. )
32 1 7 9 23 31 fuco22natlem 
 |-  ( ph -> ( B ( U P V ) A ) e. ( ( O ` U ) ( C Nat E ) ( O ` V ) ) )