# Metamath Proof Explorer

## Theorem nati

Description: Naturality property of a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses natrcl.1 ${⊢}{N}={C}\mathrm{Nat}{D}$
natixp.2 ${⊢}{\phi }\to {A}\in \left(⟨{F},{G}⟩{N}⟨{K},{L}⟩\right)$
natixp.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
nati.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
nati.o
nati.x ${⊢}{\phi }\to {X}\in {B}$
nati.y ${⊢}{\phi }\to {Y}\in {B}$
nati.r ${⊢}{\phi }\to {R}\in \left({X}{H}{Y}\right)$
Assertion nati

### Proof

Step Hyp Ref Expression
1 natrcl.1 ${⊢}{N}={C}\mathrm{Nat}{D}$
2 natixp.2 ${⊢}{\phi }\to {A}\in \left(⟨{F},{G}⟩{N}⟨{K},{L}⟩\right)$
3 natixp.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
4 nati.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
5 nati.o
6 nati.x ${⊢}{\phi }\to {X}\in {B}$
7 nati.y ${⊢}{\phi }\to {Y}\in {B}$
8 nati.r ${⊢}{\phi }\to {R}\in \left({X}{H}{Y}\right)$
9 eqid ${⊢}\mathrm{Hom}\left({D}\right)=\mathrm{Hom}\left({D}\right)$
10 1 natrcl ${⊢}{A}\in \left(⟨{F},{G}⟩{N}⟨{K},{L}⟩\right)\to \left(⟨{F},{G}⟩\in \left({C}\mathrm{Func}{D}\right)\wedge ⟨{K},{L}⟩\in \left({C}\mathrm{Func}{D}\right)\right)$
11 2 10 syl ${⊢}{\phi }\to \left(⟨{F},{G}⟩\in \left({C}\mathrm{Func}{D}\right)\wedge ⟨{K},{L}⟩\in \left({C}\mathrm{Func}{D}\right)\right)$
12 11 simpld ${⊢}{\phi }\to ⟨{F},{G}⟩\in \left({C}\mathrm{Func}{D}\right)$
13 df-br ${⊢}{F}\left({C}\mathrm{Func}{D}\right){G}↔⟨{F},{G}⟩\in \left({C}\mathrm{Func}{D}\right)$
14 12 13 sylibr ${⊢}{\phi }\to {F}\left({C}\mathrm{Func}{D}\right){G}$
15 11 simprd ${⊢}{\phi }\to ⟨{K},{L}⟩\in \left({C}\mathrm{Func}{D}\right)$
16 df-br ${⊢}{K}\left({C}\mathrm{Func}{D}\right){L}↔⟨{K},{L}⟩\in \left({C}\mathrm{Func}{D}\right)$
17 15 16 sylibr ${⊢}{\phi }\to {K}\left({C}\mathrm{Func}{D}\right){L}$
18 1 3 4 9 5 14 17 isnat
19 2 18 mpbid
20 19 simprd
21 7 adantr ${⊢}\left({\phi }\wedge {x}={X}\right)\to {Y}\in {B}$
22 8 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\to {R}\in \left({X}{H}{Y}\right)$
23 simplr ${⊢}\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\to {x}={X}$
24 simpr ${⊢}\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\to {y}={Y}$
25 23 24 oveq12d ${⊢}\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\to {x}{H}{y}={X}{H}{Y}$
26 22 25 eleqtrrd ${⊢}\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\to {R}\in \left({x}{H}{y}\right)$
27 simpllr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to {x}={X}$
28 27 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to {F}\left({x}\right)={F}\left({X}\right)$
29 simplr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to {y}={Y}$
30 29 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to {F}\left({y}\right)={F}\left({Y}\right)$
31 28 30 opeq12d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to ⟨{F}\left({x}\right),{F}\left({y}\right)⟩=⟨{F}\left({X}\right),{F}\left({Y}\right)⟩$
32 29 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to {K}\left({y}\right)={K}\left({Y}\right)$
33 31 32 oveq12d
34 29 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to {A}\left({y}\right)={A}\left({Y}\right)$
35 27 29 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to {x}{G}{y}={X}{G}{Y}$
36 simpr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to {f}={R}$
37 35 36 fveq12d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to \left({x}{G}{y}\right)\left({f}\right)=\left({X}{G}{Y}\right)\left({R}\right)$
38 33 34 37 oveq123d
39 27 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to {K}\left({x}\right)={K}\left({X}\right)$
40 28 39 opeq12d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to ⟨{F}\left({x}\right),{K}\left({x}\right)⟩=⟨{F}\left({X}\right),{K}\left({X}\right)⟩$
41 40 32 oveq12d
42 27 29 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to {x}{L}{y}={X}{L}{Y}$
43 42 36 fveq12d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to \left({x}{L}{y}\right)\left({f}\right)=\left({X}{L}{Y}\right)\left({R}\right)$
44 27 fveq2d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {f}={R}\right)\to {A}\left({x}\right)={A}\left({X}\right)$
45 41 43 44 oveq123d
46 38 45 eqeq12d
47 26 46 rspcdv
48 21 47 rspcimdv
49 6 48 rspcimdv
50 20 49 mpd