Metamath Proof Explorer

Theorem nat1st2nd

Description: Rewrite the natural transformation predicate with separated functor parts. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses natrcl.1 
|- N = ( C Nat D )
nat1st2nd.2 
|- ( ph -> A e. ( F N G ) )
Assertion nat1st2nd 
|- ( ph -> A e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )

Proof

Step Hyp Ref Expression
1 natrcl.1 
 |-  N = ( C Nat D )
2 nat1st2nd.2 
 |-  ( ph -> A e. ( F N G ) )
3 relfunc 
 |-  Rel ( C Func D )
4 1 natrcl 
 |-  ( A e. ( F N G ) -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
5 2 4 syl 
 |-  ( ph -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
6 5 simpld 
 |-  ( ph -> F e. ( C Func D ) )
7 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
8 3 6 7 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
9 5 simprd 
 |-  ( ph -> G e. ( C Func D ) )
10 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ G e. ( C Func D ) ) -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
11 3 9 10 sylancr 
 |-  ( ph -> G = <. ( 1st ` G ) , ( 2nd ` G ) >. )
12 8 11 oveq12d 
 |-  ( ph -> ( F N G ) = ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
13 2 12 eleqtrd 
 |-  ( ph -> A e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )