Theorem fucoid2

Description: Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid . (Contributed by Zhi Wang, 30-Sep-2025)

	Ref	Expression
Hypotheses	fucoid.o	No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
	fucoid.t	$$⊢T=\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)$$
	fucoid.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(T\right)$$
	fucoid.q	$$⊢Q=C\mathrm{FuncCat}E$$
	fucoid.i	$$⊢I=\mathrm{Id}\left(Q\right)$$
	fucoid2.w	$$⊢\phi \to W=\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)$$
	fucoid2.u	$$⊢\phi \to U\in W$$
Assertion	fucoid2	$$⊢\phi \to \left(UPU\right)\left(\underset{\dot{}}{1}\left(U\right)\right)=I\left(O\left(U\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fucoid.o	Could not format ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode |-
2		fucoid.t	$$⊢T=\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)$$
3		fucoid.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(T\right)$$
4		fucoid.q	$$⊢Q=C\mathrm{FuncCat}E$$
5		fucoid.i	$$⊢I=\mathrm{Id}\left(Q\right)$$
6		fucoid2.w	$$⊢\phi \to W=\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)$$
7		fucoid2.u	$$⊢\phi \to U\in W$$
8		relfunc	$$⊢\mathrm{Rel}\left(D\mathrm{Func}E\right)$$
9		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
10	6 7 8 9	fuco2eld2	$$⊢\phi \to U=⟨⟨1^{st}\left(1^{st}\left(U\right)\right),2^{nd}\left(1^{st}\left(U\right)\right)⟩,⟨1^{st}\left(2^{nd}\left(U\right)\right),2^{nd}\left(2^{nd}\left(U\right)\right)⟩⟩$$
11	7 10 6	3eltr3d	$$⊢\phi \to ⟨⟨1^{st}\left(1^{st}\left(U\right)\right),2^{nd}\left(1^{st}\left(U\right)\right)⟩,⟨1^{st}\left(2^{nd}\left(U\right)\right),2^{nd}\left(2^{nd}\left(U\right)\right)⟩⟩\in \left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)$$
12		opelxp2	$$⊢⟨⟨1^{st}\left(1^{st}\left(U\right)\right),2^{nd}\left(1^{st}\left(U\right)\right)⟩,⟨1^{st}\left(2^{nd}\left(U\right)\right),2^{nd}\left(2^{nd}\left(U\right)\right)⟩⟩\in \left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)\to ⟨1^{st}\left(2^{nd}\left(U\right)\right),2^{nd}\left(2^{nd}\left(U\right)\right)⟩\in \left(C\mathrm{Func}D\right)$$
13	11 12	syl	$$⊢\phi \to ⟨1^{st}\left(2^{nd}\left(U\right)\right),2^{nd}\left(2^{nd}\left(U\right)\right)⟩\in \left(C\mathrm{Func}D\right)$$
14		df-br	$$⊢1^{st}\left(2^{nd}\left(U\right)\right)\left(C\mathrm{Func}D\right)2^{nd}\left(2^{nd}\left(U\right)\right)\leftrightarrow ⟨1^{st}\left(2^{nd}\left(U\right)\right),2^{nd}\left(2^{nd}\left(U\right)\right)⟩\in \left(C\mathrm{Func}D\right)$$
15	13 14	sylibr	$$⊢\phi \to 1^{st}\left(2^{nd}\left(U\right)\right)\left(C\mathrm{Func}D\right)2^{nd}\left(2^{nd}\left(U\right)\right)$$
16		opelxp1	$$⊢⟨⟨1^{st}\left(1^{st}\left(U\right)\right),2^{nd}\left(1^{st}\left(U\right)\right)⟩,⟨1^{st}\left(2^{nd}\left(U\right)\right),2^{nd}\left(2^{nd}\left(U\right)\right)⟩⟩\in \left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)\to ⟨1^{st}\left(1^{st}\left(U\right)\right),2^{nd}\left(1^{st}\left(U\right)\right)⟩\in \left(D\mathrm{Func}E\right)$$
17	11 16	syl	$$⊢\phi \to ⟨1^{st}\left(1^{st}\left(U\right)\right),2^{nd}\left(1^{st}\left(U\right)\right)⟩\in \left(D\mathrm{Func}E\right)$$
18		df-br	$$⊢1^{st}\left(1^{st}\left(U\right)\right)\left(D\mathrm{Func}E\right)2^{nd}\left(1^{st}\left(U\right)\right)\leftrightarrow ⟨1^{st}\left(1^{st}\left(U\right)\right),2^{nd}\left(1^{st}\left(U\right)\right)⟩\in \left(D\mathrm{Func}E\right)$$
19	17 18	sylibr	$$⊢\phi \to 1^{st}\left(1^{st}\left(U\right)\right)\left(D\mathrm{Func}E\right)2^{nd}\left(1^{st}\left(U\right)\right)$$
20	1 2 3 4 5 15 19 10	fucoid	$$⊢\phi \to \left(UPU\right)\left(\underset{\dot{}}{1}\left(U\right)\right)=I\left(O\left(U\right)\right)$$