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	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
	fucoid.t	|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
	fucoid.1	|- .1. = ( Id ` T )
	fucoid.q	|- Q = ( C FuncCat E )
	fucoid.i	|- I = ( Id ` Q )
	fucoid2.w	|- ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
	fucoid2.u	|- ( ph -> U e. W )
Assertion	fucoid2	|- ( ph -> ( ( U P U ) ` ( .1. ` U ) ) = ( I ` ( O ` U ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoid.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
2		fucoid.t	|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
3		fucoid.1	|- .1. = ( Id ` T )
4		fucoid.q	|- Q = ( C FuncCat E )
5		fucoid.i	|- I = ( Id ` Q )
6		fucoid2.w	|- ( ph -> W = ( ( D Func E ) X. ( C Func D ) ) )
7		fucoid2.u	|- ( ph -> U e. W )
8		relfunc	|- Rel ( D Func E )
9		relfunc	|- Rel ( C Func D )
10	6 7 8 9	fuco2eld2	|- ( ph -> U = <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. )
11	7 10 6	3eltr3d	|- ( ph -> <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. e. ( ( D Func E ) X. ( C Func D ) ) )
12		opelxp2	|- ( <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. e. ( ( D Func E ) X. ( C Func D ) ) -> <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. e. ( C Func D ) )
13	11 12	syl	|- ( ph -> <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. e. ( C Func D ) )
14		df-br	|- ( ( 1st ` ( 2nd ` U ) ) ( C Func D ) ( 2nd ` ( 2nd ` U ) ) <-> <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. e. ( C Func D ) )
15	13 14	sylibr	|- ( ph -> ( 1st ` ( 2nd ` U ) ) ( C Func D ) ( 2nd ` ( 2nd ` U ) ) )
16		opelxp1	|- ( <. <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. , <. ( 1st ` ( 2nd ` U ) ) , ( 2nd ` ( 2nd ` U ) ) >. >. e. ( ( D Func E ) X. ( C Func D ) ) -> <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. e. ( D Func E ) )
17	11 16	syl	|- ( ph -> <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. e. ( D Func E ) )
18		df-br	|- ( ( 1st ` ( 1st ` U ) ) ( D Func E ) ( 2nd ` ( 1st ` U ) ) <-> <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. e. ( D Func E ) )
19	17 18	sylibr	|- ( ph -> ( 1st ` ( 1st ` U ) ) ( D Func E ) ( 2nd ` ( 1st ` U ) ) )
20	1 2 3 4 5 15 19 10	fucoid	|- ( ph -> ( ( U P U ) ` ( .1. ` U ) ) = ( I ` ( O ` U ) ) )