Metamath Proof Explorer

Theorem natideq

Description: A natural transformation is an identity exactly when all its components are identities. This also covers an empty object set. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypotheses natideq.q 
|- Q = ( C FuncCat D )
natideq.n 
|- N = ( C Nat D )
natideq.b 
|- B = ( Base ` C )
natideq.i 
|- I = ( Id ` Q )
natideq.j 
|- J = ( Id ` D )
natideq.a 
|- ( ph -> A e. ( F N F ) )
Assertion natideq 
|- ( ph -> ( A = ( I ` F ) <-> A. x e. B ( A ` x ) = ( J ` ( ( 1st ` F ) ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 natideq.q 
 |-  Q = ( C FuncCat D )
2 natideq.n 
 |-  N = ( C Nat D )
3 natideq.b 
 |-  B = ( Base ` C )
4 natideq.i 
 |-  I = ( Id ` Q )
5 natideq.j 
 |-  J = ( Id ` D )
6 natideq.a 
 |-  ( ph -> A e. ( F N F ) )
7 2 natrcl 
 |-  ( A e. ( F N F ) -> ( F e. ( C Func D ) /\ F e. ( C Func D ) ) )
8 6 7 syl 
 |-  ( ph -> ( F e. ( C Func D ) /\ F e. ( C Func D ) ) )
9 8 simpld 
 |-  ( ph -> F e. ( C Func D ) )
10 1 4 5 9 fucid 
 |-  ( ph -> ( I ` F ) = ( J o. ( 1st ` F ) ) )
11 1 2 5 9 fucidcl 
 |-  ( ph -> ( J o. ( 1st ` F ) ) e. ( F N F ) )
12 10 11 eqeltrd 
 |-  ( ph -> ( I ` F ) e. ( F N F ) )
13 2 3 6 12 nateq 
 |-  ( ph -> ( A = ( I ` F ) <-> A. x e. B ( A ` x ) = ( ( I ` F ) ` x ) ) )
14 10 adantr 
 |-  ( ( ph /\ x e. B ) -> ( I ` F ) = ( J o. ( 1st ` F ) ) )
15 14 fveq1d 
 |-  ( ( ph /\ x e. B ) -> ( ( I ` F ) ` x ) = ( ( J o. ( 1st ` F ) ) ` x ) )
16 eqid 
 |-  ( Base ` D ) = ( Base ` D )
17 9 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
18 3 16 17 funcf1 
 |-  ( ph -> ( 1st ` F ) : B --> ( Base ` D ) )
19 18 adantr 
 |-  ( ( ph /\ x e. B ) -> ( 1st ` F ) : B --> ( Base ` D ) )
20 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
21 19 20 fvco3d 
 |-  ( ( ph /\ x e. B ) -> ( ( J o. ( 1st ` F ) ) ` x ) = ( J ` ( ( 1st ` F ) ` x ) ) )
22 15 21 eqtrd 
 |-  ( ( ph /\ x e. B ) -> ( ( I ` F ) ` x ) = ( J ` ( ( 1st ` F ) ` x ) ) )
23 22 eqeq2d 
 |-  ( ( ph /\ x e. B ) -> ( ( A ` x ) = ( ( I ` F ) ` x ) <-> ( A ` x ) = ( J ` ( ( 1st ` F ) ` x ) ) ) )
24 23 ralbidva 
 |-  ( ph -> ( A. x e. B ( A ` x ) = ( ( I ` F ) ` x ) <-> A. x e. B ( A ` x ) = ( J ` ( ( 1st ` F ) ` x ) ) ) )
25 13 24 bitrd 
 |-  ( ph -> ( A = ( I ` F ) <-> A. x e. B ( A ` x ) = ( J ` ( ( 1st ` F ) ` x ) ) ) )