Theorem fuco11bALT

Description: Alternate proof of fuco11b . (Contributed by Zhi Wang, 11-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	fuco11b.o	No typesetting found for |- ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = O ) with typecode |-
	fuco11b.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	fuco11b.g	$$⊢\phi \to G\in \left(D\mathrm{Func}E\right)$$
Assertion	fuco11bALT	$$⊢\phi \to GOF=G{\circ }_{\mathrm{func}}F$$

Proof

Step	Hyp	Ref	Expression
1		fuco11b.o	Could not format ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = O ) : No typesetting found for |- ( ph -> ( 1st ` ( <. C , D >. o.F E ) ) = O ) with typecode |-
2		fuco11b.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
3		fuco11b.g	$$⊢\phi \to G\in \left(D\mathrm{Func}E\right)$$
4		df-ov	$$⊢GOF=O\left(⟨G,F⟩\right)$$
5		relfunc	$$⊢\mathrm{Rel}\left(D\mathrm{Func}E\right)$$
6		1st2nd	$$⊢\left(\mathrm{Rel}\left(D\mathrm{Func}E\right)\wedge G\in \left(D\mathrm{Func}E\right)\right)\to G=⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩$$
7	5 3 6	sylancr	$$⊢\phi \to G=⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩$$
8		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
9		1st2nd	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
10	8 2 9	sylancr	$$⊢\phi \to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
11	7 10	oveq12d	$$⊢\phi \to G{\circ }_{\mathrm{func}}F=⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩{\circ }_{\mathrm{func}}⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
12		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
13	8 2 12	sylancr	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
14	13	funcrcl2	$$⊢\phi \to C\in \mathrm{Cat}$$
15		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(D\mathrm{Func}E\right)\wedge G\in \left(D\mathrm{Func}E\right)\right)\to 1^{st}\left(G\right)\left(D\mathrm{Func}E\right)2^{nd}\left(G\right)$$
16	5 3 15	sylancr	$$⊢\phi \to 1^{st}\left(G\right)\left(D\mathrm{Func}E\right)2^{nd}\left(G\right)$$
17	16	funcrcl2	$$⊢\phi \to D\in \mathrm{Cat}$$
18	16	funcrcl3	$$⊢\phi \to E\in \mathrm{Cat}$$
19		eqidd	Could not format ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = ( <. C , D >. o.F E ) ) with typecode |-
20	14 17 18 19	fucoelvv	Could not format ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) e. ( _V X. _V ) ) with typecode |-
21		1st2nd2	Could not format ( ( <. C , D >. o.F E ) e. ( _V X. _V ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) : No typesetting found for |- ( ( <. C , D >. o.F E ) e. ( _V X. _V ) -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) with typecode |-
22	20 21	syl	Could not format ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) : No typesetting found for |- ( ph -> ( <. C , D >. o.F E ) = <. ( 1st ` ( <. C , D >. o.F E ) ) , ( 2nd ` ( <. C , D >. o.F E ) ) >. ) with typecode |-
23	7 10	opeq12d	$$⊢\phi \to ⟨G,F⟩=⟨⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩,⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩⟩$$
24	22 13 16 23	fuco11	Could not format ( ph -> ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. G , F >. ) = ( <. ( 1st ` G ) , ( 2nd ` G ) >. o.func <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) : No typesetting found for |- ( ph -> ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. G , F >. ) = ( <. ( 1st ` G ) , ( 2nd ` G ) >. o.func <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) with typecode |-
25	1	fveq1d	Could not format ( ph -> ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. G , F >. ) = ( O ` <. G , F >. ) ) : No typesetting found for |- ( ph -> ( ( 1st ` ( <. C , D >. o.F E ) ) ` <. G , F >. ) = ( O ` <. G , F >. ) ) with typecode |-
26	11 24 25	3eqtr2rd	$$⊢\phi \to O\left(⟨G,F⟩\right)=G{\circ }_{\mathrm{func}}F$$
27	4 26	eqtrid	$$⊢\phi \to GOF=G{\circ }_{\mathrm{func}}F$$