Theorem cofuswapf1

Description: The object part of a bifunctor pre-composed with a swap functor. (Contributed by Zhi Wang, 9-Oct-2025)

	Ref	Expression
Hypotheses	cofuswapf1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	cofuswapf1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	cofuswapf1.f	$$⊢\phi \to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
	cofuswapf1.g	No typesetting found for |- ( ph -> G = ( F o.func ( C swapF D ) ) ) with typecode |-
	cofuswapf1.a	$$⊢A={\mathrm{Base}}_C$$
	cofuswapf1.b	$$⊢B={\mathrm{Base}}_D$$
	cofuswapf1.x	$$⊢\phi \to X\in A$$
	cofuswapf1.y	$$⊢\phi \to Y\in B$$
Assertion	cofuswapf1	$$⊢\phi \to X{1}^{st}\left(G\right)Y=Y{1}^{st}\left(F\right)X$$

Proof

Step	Hyp	Ref	Expression
1		cofuswapf1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
2		cofuswapf1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
3		cofuswapf1.f	$$⊢\phi \to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
4		cofuswapf1.g	Could not format ( ph -> G = ( F o.func ( C swapF D ) ) ) : No typesetting found for |- ( ph -> G = ( F o.func ( C swapF D ) ) ) with typecode |-
5		cofuswapf1.a	$$⊢A={\mathrm{Base}}_C$$
6		cofuswapf1.b	$$⊢B={\mathrm{Base}}_D$$
7		cofuswapf1.x	$$⊢\phi \to X\in A$$
8		cofuswapf1.y	$$⊢\phi \to Y\in B$$
9		df-ov	$$⊢X{1}^{st}\left(G\right)Y=1^{st}\left(G\right)\left(⟨X,Y⟩\right)$$
10	4	fveq2d	Could not format ( ph -> ( 1st ` G ) = ( 1st ` ( F o.func ( C swapF D ) ) ) ) : No typesetting found for |- ( ph -> ( 1st ` G ) = ( 1st ` ( F o.func ( C swapF D ) ) ) ) with typecode |-
11	10	fveq1d	Could not format ( ph -> ( ( 1st ` G ) ` <. X , Y >. ) = ( ( 1st ` ( F o.func ( C swapF D ) ) ) ` <. X , Y >. ) ) : No typesetting found for |- ( ph -> ( ( 1st ` G ) ` <. X , Y >. ) = ( ( 1st ` ( F o.func ( C swapF D ) ) ) ` <. X , Y >. ) ) with typecode |-
12	9 11	eqtrid	Could not format ( ph -> ( X ( 1st ` G ) Y ) = ( ( 1st ` ( F o.func ( C swapF D ) ) ) ` <. X , Y >. ) ) : No typesetting found for |- ( ph -> ( X ( 1st ` G ) Y ) = ( ( 1st ` ( F o.func ( C swapF D ) ) ) ` <. X , Y >. ) ) with typecode |-
13		eqid	$$⊢C{\times }_{c}D=C{\times }_{c}D$$
14	13 5 6	xpcbas	$$⊢A\times B={\mathrm{Base}}_{\left(C{\times }_{c}D\right)}$$
15		eqid	$$⊢D{\times }_{c}C=D{\times }_{c}C$$
16	1 2 13 15	swapffunca	Could not format ( ph -> ( C swapF D ) e. ( ( C Xc. D ) Func ( D Xc. C ) ) ) : No typesetting found for |- ( ph -> ( C swapF D ) e. ( ( C Xc. D ) Func ( D Xc. C ) ) ) with typecode |-
17	7 8	opelxpd	$$⊢\phi \to ⟨X,Y⟩\in \left(A\times B\right)$$
18	14 16 3 17	cofu1	Could not format ( ph -> ( ( 1st ` ( F o.func ( C swapF D ) ) ) ` <. X , Y >. ) = ( ( 1st ` F ) ` ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ) ) : No typesetting found for |- ( ph -> ( ( 1st ` ( F o.func ( C swapF D ) ) ) ` <. X , Y >. ) = ( ( 1st ` F ) ` ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ) ) with typecode |-
19		df-ov	Could not format ( X ( 1st ` ( C swapF D ) ) Y ) = ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) : No typesetting found for |- ( X ( 1st ` ( C swapF D ) ) Y ) = ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) with typecode |-
20	1 2	swapfelvv	Could not format ( ph -> ( C swapF D ) e. ( _V X. _V ) ) : No typesetting found for |- ( ph -> ( C swapF D ) e. ( _V X. _V ) ) with typecode |-
21		1st2nd2	Could not format ( ( C swapF D ) e. ( _V X. _V ) -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. ) : No typesetting found for |- ( ( C swapF D ) e. ( _V X. _V ) -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. ) with typecode |-
22	20 21	syl	Could not format ( ph -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. ) : No typesetting found for |- ( ph -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. ) with typecode |-
23	7 5	eleqtrdi	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
24	8 6	eleqtrdi	$$⊢\phi \to Y\in {\mathrm{Base}}_D$$
25	22 23 24	swapf1	Could not format ( ph -> ( X ( 1st ` ( C swapF D ) ) Y ) = <. Y , X >. ) : No typesetting found for |- ( ph -> ( X ( 1st ` ( C swapF D ) ) Y ) = <. Y , X >. ) with typecode |-
26	19 25	eqtr3id	Could not format ( ph -> ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) = <. Y , X >. ) : No typesetting found for |- ( ph -> ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) = <. Y , X >. ) with typecode |-
27	26	fveq2d	Could not format ( ph -> ( ( 1st ` F ) ` ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ) = ( ( 1st ` F ) ` <. Y , X >. ) ) : No typesetting found for |- ( ph -> ( ( 1st ` F ) ` ( ( 1st ` ( C swapF D ) ) ` <. X , Y >. ) ) = ( ( 1st ` F ) ` <. Y , X >. ) ) with typecode |-
28	12 18 27	3eqtrd	$$⊢\phi \to X{1}^{st}\left(G\right)Y=1^{st}\left(F\right)\left(⟨Y,X⟩\right)$$
29		df-ov	$$⊢Y{1}^{st}\left(F\right)X=1^{st}\left(F\right)\left(⟨Y,X⟩\right)$$
30	28 29	eqtr4di	$$⊢\phi \to X{1}^{st}\left(G\right)Y=Y{1}^{st}\left(F\right)X$$