Theorem natffn

Description: The natural transformation set operation is a well-defined function. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypothesis	natrcl.1	$$⊢N=C\mathrm{Nat}D$$
Assertion	natffn	$$⊢NFn\left(\left(C\mathrm{Func}D\right)\times \left(C\mathrm{Func}D\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		natrcl.1	$$⊢N=C\mathrm{Nat}D$$
2		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
3		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
4		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
5		eqid	$$⊢\mathrm{comp}\left(D\right)=\mathrm{comp}\left(D\right)$$
6	1 2 3 4 5	natfval	$$⊢N=\left(f\in \left(C\mathrm{Func}D\right),g\in \left(C\mathrm{Func}D\right)⟼⦋1^{st}\left(f\right)/r⦌⦋1^{st}\left(g\right)/s⦌\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall h\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(h\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(h\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\right)$$
7		ovex	$$⊢r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\in \mathrm{V}$$
8	7	rgenw	$$⊢\forall x\in {\mathrm{Base}}_{C}r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\in \mathrm{V}$$
9		ixpexg	$$⊢\forall x\in {\mathrm{Base}}_{C}r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\in \mathrm{V}\to \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)\in \mathrm{V}$$
10	8 9	ax-mp	$$⊢\underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)\in \mathrm{V}$$
11	10	rabex	$$⊢\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall h\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(h\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(h\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in \mathrm{V}$$
12	11	csbex	$$⊢⦋1^{st}\left(g\right)/s⦌\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall h\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(h\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(h\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in \mathrm{V}$$
13	12	csbex	$$⊢⦋1^{st}\left(f\right)/r⦌⦋1^{st}\left(g\right)/s⦌\left\{a\in \underset{x\in {\mathrm{Base}}_C}{⨉}\left(r\left(x\right)\mathrm{Hom}\left(D\right)s\left(x\right)\right)|\forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C\forall h\in \left(x\mathrm{Hom}\left(C\right)y\right)a\left(y\right)\left(⟨r\left(x\right),r\left(y\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)\left(x{2}^{nd}\left(f\right)y\right)\left(h\right)=\left(x{2}^{nd}\left(g\right)y\right)\left(h\right)\left(⟨r\left(x\right),s\left(x\right)⟩\mathrm{comp}\left(D\right)s\left(y\right)\right)a\left(x\right)\right\}\in \mathrm{V}$$
14	6 13	fnmpoi	$$⊢NFn\left(\left(C\mathrm{Func}D\right)\times \left(C\mathrm{Func}D\right)\right)$$