Metamath Proof Explorer


Theorem natpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same natural transformations. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Hypotheses fucpropd.1 φ Hom 𝑓 A = Hom 𝑓 B
fucpropd.2 φ comp 𝑓 A = comp 𝑓 B
fucpropd.3 φ Hom 𝑓 C = Hom 𝑓 D
fucpropd.4 φ comp 𝑓 C = comp 𝑓 D
fucpropd.a φ A Cat
fucpropd.b φ B Cat
fucpropd.c φ C Cat
fucpropd.d φ D Cat
Assertion natpropd φ A Nat C = B Nat D

Proof

Step Hyp Ref Expression
1 fucpropd.1 φ Hom 𝑓 A = Hom 𝑓 B
2 fucpropd.2 φ comp 𝑓 A = comp 𝑓 B
3 fucpropd.3 φ Hom 𝑓 C = Hom 𝑓 D
4 fucpropd.4 φ comp 𝑓 C = comp 𝑓 D
5 fucpropd.a φ A Cat
6 fucpropd.b φ B Cat
7 fucpropd.c φ C Cat
8 fucpropd.d φ D Cat
9 1 2 3 4 5 6 7 8 funcpropd φ A Func C = B Func D
10 9 adantr φ f A Func C A Func C = B Func D
11 nfv r φ f A Func C g A Func C
12 nfcsb1v _ r 1 st f / r 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
13 12 a1i φ f A Func C g A Func C _ r 1 st f / r 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
14 fvexd φ f A Func C g A Func C 1 st f V
15 nfv s φ f A Func C g A Func C r = 1 st f
16 nfcsb1v _ s 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
17 16 a1i φ f A Func C g A Func C r = 1 st f _ s 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
18 fvexd φ f A Func C g A Func C r = 1 st f 1 st g V
19 eqid Base C = Base C
20 eqid Hom C = Hom C
21 eqid Hom D = Hom D
22 3 ad4antr φ f A Func C g A Func C r = 1 st f s = 1 st g x Base A Hom 𝑓 C = Hom 𝑓 D
23 eqid Base A = Base A
24 simplr φ f A Func C g A Func C r = 1 st f s = 1 st g r = 1 st f
25 relfunc Rel A Func C
26 simpllr φ f A Func C g A Func C r = 1 st f s = 1 st g f A Func C g A Func C
27 26 simpld φ f A Func C g A Func C r = 1 st f s = 1 st g f A Func C
28 1st2ndbr Rel A Func C f A Func C 1 st f A Func C 2 nd f
29 25 27 28 sylancr φ f A Func C g A Func C r = 1 st f s = 1 st g 1 st f A Func C 2 nd f
30 24 29 eqbrtrd φ f A Func C g A Func C r = 1 st f s = 1 st g r A Func C 2 nd f
31 23 19 30 funcf1 φ f A Func C g A Func C r = 1 st f s = 1 st g r : Base A Base C
32 31 ffvelrnda φ f A Func C g A Func C r = 1 st f s = 1 st g x Base A r x Base C
33 simpr φ f A Func C g A Func C r = 1 st f s = 1 st g s = 1 st g
34 26 simprd φ f A Func C g A Func C r = 1 st f s = 1 st g g A Func C
35 1st2ndbr Rel A Func C g A Func C 1 st g A Func C 2 nd g
36 25 34 35 sylancr φ f A Func C g A Func C r = 1 st f s = 1 st g 1 st g A Func C 2 nd g
37 33 36 eqbrtrd φ f A Func C g A Func C r = 1 st f s = 1 st g s A Func C 2 nd g
38 23 19 37 funcf1 φ f A Func C g A Func C r = 1 st f s = 1 st g s : Base A Base C
39 38 ffvelrnda φ f A Func C g A Func C r = 1 st f s = 1 st g x Base A s x Base C
40 19 20 21 22 32 39 homfeqval φ f A Func C g A Func C r = 1 st f s = 1 st g x Base A r x Hom C s x = r x Hom D s x
41 40 ixpeq2dva φ f A Func C g A Func C r = 1 st f s = 1 st g x Base A r x Hom C s x = x Base A r x Hom D s x
42 1 homfeqbas φ Base A = Base B
43 42 ad3antrrr φ f A Func C g A Func C r = 1 st f s = 1 st g Base A = Base B
44 43 ixpeq1d φ f A Func C g A Func C r = 1 st f s = 1 st g x Base A r x Hom D s x = x Base B r x Hom D s x
45 41 44 eqtrd φ f A Func C g A Func C r = 1 st f s = 1 st g x Base A r x Hom C s x = x Base B r x Hom D s x
46 fveq2 x = z r x = r z
47 fveq2 x = z s x = s z
48 46 47 oveq12d x = z r x Hom C s x = r z Hom C s z
49 48 cbvixpv x Base A r x Hom C s x = z Base A r z Hom C s z
50 49 eleq2i a x Base A r x Hom C s x a z Base A r z Hom C s z
51 43 adantr φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z Base A = Base B
52 51 adantr φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A Base A = Base B
53 eqid Hom A = Hom A
54 eqid Hom B = Hom B
55 1 ad6antr φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A Hom 𝑓 A = Hom 𝑓 B
56 simplr φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A x Base A
57 simpr φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A y Base A
58 23 53 54 55 56 57 homfeqval φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A x Hom A y = x Hom B y
59 eqid comp C = comp C
60 eqid comp D = comp D
61 3 ad7antr φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y Hom 𝑓 C = Hom 𝑓 D
62 4 ad7antr φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y comp 𝑓 C = comp 𝑓 D
63 32 ad5ant13 φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y r x Base C
64 31 ad2antrr φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A r : Base A Base C
65 64 ffvelrnda φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A r y Base C
66 65 adantr φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y r y Base C
67 38 ad2antrr φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A s : Base A Base C
68 67 ffvelrnda φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A s y Base C
69 68 adantr φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y s y Base C
70 30 ad3antrrr φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A r A Func C 2 nd f
71 23 53 20 70 56 57 funcf2 φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A x 2 nd f y : x Hom A y r x Hom C r y
72 71 ffvelrnda φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y x 2 nd f y h r x Hom C r y
73 fveq2 z = y r z = r y
74 fveq2 z = y s z = s y
75 73 74 oveq12d z = y r z Hom C s z = r y Hom C s y
76 75 fvixp a z Base A r z Hom C s z y Base A a y r y Hom C s y
77 76 ad5ant24 φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y a y r y Hom C s y
78 19 20 59 60 61 62 63 66 69 72 77 comfeqval φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y a y r x r y comp C s y x 2 nd f y h = a y r x r y comp D s y x 2 nd f y h
79 39 ad5ant13 φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y s x Base C
80 fveq2 z = x r z = r x
81 fveq2 z = x s z = s x
82 80 81 oveq12d z = x r z Hom C s z = r x Hom C s x
83 82 fvixp a z Base A r z Hom C s z x Base A a x r x Hom C s x
84 83 ad5ant23 φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y a x r x Hom C s x
85 37 ad3antrrr φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A s A Func C 2 nd g
86 23 53 20 85 56 57 funcf2 φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A x 2 nd g y : x Hom A y s x Hom C s y
87 86 ffvelrnda φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y x 2 nd g y h s x Hom C s y
88 19 20 59 60 61 62 63 79 69 84 87 comfeqval φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y x 2 nd g y h r x s x comp C s y a x = x 2 nd g y h r x s x comp D s y a x
89 78 88 eqeq12d φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y a y r x r y comp C s y x 2 nd f y h = x 2 nd g y h r x s x comp C s y a x a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
90 58 89 raleqbidva φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y a y r x r y comp C s y x 2 nd f y h = x 2 nd g y h r x s x comp C s y a x h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
91 52 90 raleqbidva φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y a y r x r y comp C s y x 2 nd f y h = x 2 nd g y h r x s x comp C s y a x y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
92 51 91 raleqbidva φ f A Func C g A Func C r = 1 st f s = 1 st g a z Base A r z Hom C s z x Base A y Base A h x Hom A y a y r x r y comp C s y x 2 nd f y h = x 2 nd g y h r x s x comp C s y a x x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
93 50 92 sylan2b φ f A Func C g A Func C r = 1 st f s = 1 st g a x Base A r x Hom C s x x Base A y Base A h x Hom A y a y r x r y comp C s y x 2 nd f y h = x 2 nd g y h r x s x comp C s y a x x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
94 45 93 rabeqbidva φ f A Func C g A Func C r = 1 st f s = 1 st g a x Base A r x Hom C s x | x Base A y Base A h x Hom A y a y r x r y comp C s y x 2 nd f y h = x 2 nd g y h r x s x comp C s y a x = a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
95 csbeq1a s = 1 st g a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x = 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
96 95 adantl φ f A Func C g A Func C r = 1 st f s = 1 st g a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x = 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
97 94 96 eqtrd φ f A Func C g A Func C r = 1 st f s = 1 st g a x Base A r x Hom C s x | x Base A y Base A h x Hom A y a y r x r y comp C s y x 2 nd f y h = x 2 nd g y h r x s x comp C s y a x = 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
98 15 17 18 97 csbiedf φ f A Func C g A Func C r = 1 st f 1 st g / s a x Base A r x Hom C s x | x Base A y Base A h x Hom A y a y r x r y comp C s y x 2 nd f y h = x 2 nd g y h r x s x comp C s y a x = 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
99 csbeq1a r = 1 st f 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x = 1 st f / r 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
100 99 adantl φ f A Func C g A Func C r = 1 st f 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x = 1 st f / r 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
101 98 100 eqtrd φ f A Func C g A Func C r = 1 st f 1 st g / s a x Base A r x Hom C s x | x Base A y Base A h x Hom A y a y r x r y comp C s y x 2 nd f y h = x 2 nd g y h r x s x comp C s y a x = 1 st f / r 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
102 11 13 14 101 csbiedf φ f A Func C g A Func C 1 st f / r 1 st g / s a x Base A r x Hom C s x | x Base A y Base A h x Hom A y a y r x r y comp C s y x 2 nd f y h = x 2 nd g y h r x s x comp C s y a x = 1 st f / r 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
103 9 10 102 mpoeq123dva φ f A Func C , g A Func C 1 st f / r 1 st g / s a x Base A r x Hom C s x | x Base A y Base A h x Hom A y a y r x r y comp C s y x 2 nd f y h = x 2 nd g y h r x s x comp C s y a x = f B Func D , g B Func D 1 st f / r 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
104 eqid A Nat C = A Nat C
105 104 23 53 20 59 natfval A Nat C = f A Func C , g A Func C 1 st f / r 1 st g / s a x Base A r x Hom C s x | x Base A y Base A h x Hom A y a y r x r y comp C s y x 2 nd f y h = x 2 nd g y h r x s x comp C s y a x
106 eqid B Nat D = B Nat D
107 eqid Base B = Base B
108 106 107 54 21 60 natfval B Nat D = f B Func D , g B Func D 1 st f / r 1 st g / s a x Base B r x Hom D s x | x Base B y Base B h x Hom B y a y r x r y comp D s y x 2 nd f y h = x 2 nd g y h r x s x comp D s y a x
109 103 105 108 3eqtr4g φ A Nat C = B Nat D