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	⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) = 𝑂 )
	fuco11b.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	fuco11b.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
Assertion	fuco11bALT	⊢ ( 𝜑 → ( 𝐺 𝑂 𝐹 ) = ( 𝐺 ∘func 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		fuco11b.o	⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) = 𝑂 )
2		fuco11b.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
3		fuco11b.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
4		df-ov	⊢ ( 𝐺 𝑂 𝐹 ) = ( 𝑂 ‘ ⟨ 𝐺 , 𝐹 ⟩ )
5		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
6		1st2nd	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐷 Func 𝐸 ) ) → 𝐺 = ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ )
7	5 3 6	sylancr	⊢ ( 𝜑 → 𝐺 = ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ )
8		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
9		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 = ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
10	8 2 9	sylancr	⊢ ( 𝜑 → 𝐹 = ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
11	7 10	oveq12d	⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) = ( ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ ∘func ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ) )
12		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
13	8 2 12	sylancr	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
14	13	funcrcl2	⊢ ( 𝜑 → 𝐶 ∈ Cat )
15		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1st ‘ 𝐺 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐺 ) )
16	5 3 15	sylancr	⊢ ( 𝜑 → ( 1st ‘ 𝐺 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐺 ) )
17	16	funcrcl2	⊢ ( 𝜑 → 𝐷 ∈ Cat )
18	16	funcrcl3	⊢ ( 𝜑 → 𝐸 ∈ Cat )
19		eqidd	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) )
20	14 17 18 19	fucoelvv	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( V × V ) )
21		1st2nd2	⊢ ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( V × V ) → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) , ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟩ )
22	20 21	syl	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) , ( 2nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ⟩ )
23	7 10	opeq12d	⊢ ( 𝜑 → ⟨ 𝐺 , 𝐹 ⟩ = ⟨ ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ , ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ⟩ )
24	22 13 16 23	fuco11	⊢ ( 𝜑 → ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ‘ ⟨ 𝐺 , 𝐹 ⟩ ) = ( ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ ∘func ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ) )
25	1	fveq1d	⊢ ( 𝜑 → ( ( 1st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ) ‘ ⟨ 𝐺 , 𝐹 ⟩ ) = ( 𝑂 ‘ ⟨ 𝐺 , 𝐹 ⟩ ) )
26	11 24 25	3eqtr2rd	⊢ ( 𝜑 → ( 𝑂 ‘ ⟨ 𝐺 , 𝐹 ⟩ ) = ( 𝐺 ∘func 𝐹 ) )
27	4 26	eqtrid	⊢ ( 𝜑 → ( 𝐺 𝑂 𝐹 ) = ( 𝐺 ∘func 𝐹 ) )