Metamath Proof Explorer

Theorem cofu1stfix

Description: Post-composition by an object-fixing functor preserves the entire object function, including its exact domain. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

		Ref	Expression
	Hypotheses	cofu1stfix.a	⊢ 𝐴 = ( Base ‘ 𝐸 )
		cofu1stfix.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
		cofu1stfix.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐸 Func 𝐸 ) )
		cofu1stfix.i	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) = ( I ↾ 𝐴 ) )
	Assertion	cofu1stfix	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐾 ∘_func 𝐹 ) ) = ( 1^st ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		cofu1stfix.a	⊢ 𝐴 = ( Base ‘ 𝐸 )
2		cofu1stfix.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
3		cofu1stfix.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐸 Func 𝐸 ) )
4		cofu1stfix.i	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) = ( I ↾ 𝐴 ) )
5		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
6	5 2 3	cofu1st	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐾 ∘_func 𝐹 ) ) = ( ( 1^st ‘ 𝐾 ) ∘ ( 1^st ‘ 𝐹 ) ) )
7	4	coeq1d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ∘ ( 1^st ‘ 𝐹 ) ) = ( ( I ↾ 𝐴 ) ∘ ( 1^st ‘ 𝐹 ) ) )
8	2	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
9	5 1 8	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐷 ) ⟶ 𝐴 )
10		fcoi2	⊢ ( ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐷 ) ⟶ 𝐴 → ( ( I ↾ 𝐴 ) ∘ ( 1^st ‘ 𝐹 ) ) = ( 1^st ‘ 𝐹 ) )
11	9 10	syl	⊢ ( 𝜑 → ( ( I ↾ 𝐴 ) ∘ ( 1^st ‘ 𝐹 ) ) = ( 1^st ‘ 𝐹 ) )
12	6 7 11	3eqtrd	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐾 ∘_func 𝐹 ) ) = ( 1^st ‘ 𝐹 ) )