Theorem imaf1hom

Description: The hom-set of an image of a functor injective on objects. (Contributed by Zhi Wang, 7-Nov-2025)

	Ref	Expression
Hypotheses	imaf1hom.s	⊢ 𝑆 = ( 𝐹 “ 𝐴 )
	imaf1hom.1	⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ 𝐶 )
	imaf1hom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	imaf1hom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
	imaf1hom.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	imaf1hom.k	⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
Assertion	imaf1hom	⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) “ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		imaf1hom.s	⊢ 𝑆 = ( 𝐹 “ 𝐴 )
2		imaf1hom.1	⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ 𝐶 )
3		imaf1hom.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
4		imaf1hom.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
5		imaf1hom.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
6		imaf1hom.k	⊢ 𝐾 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑥 } ) × ( ◡ 𝐹 “ { 𝑦 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
7	5 5 3 4 6	imasubclem3	⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐹 “ { 𝑌 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
8	1 2 3	imaf1homlem	⊢ ( 𝜑 → ( { ( ◡ 𝐹 ‘ 𝑋 ) } = ( ◡ 𝐹 “ { 𝑋 } ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑋 ) ) = 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) )
9	8	simp1d	⊢ ( 𝜑 → { ( ◡ 𝐹 ‘ 𝑋 ) } = ( ◡ 𝐹 “ { 𝑋 } ) )
10	1 2 4	imaf1homlem	⊢ ( 𝜑 → ( { ( ◡ 𝐹 ‘ 𝑌 ) } = ( ◡ 𝐹 “ { 𝑌 } ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) = 𝑌 ∧ ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝐵 ) )
11	10	simp1d	⊢ ( 𝜑 → { ( ◡ 𝐹 ‘ 𝑌 ) } = ( ◡ 𝐹 “ { 𝑌 } ) )
12	9 11	xpeq12d	⊢ ( 𝜑 → ( { ( ◡ 𝐹 ‘ 𝑋 ) } × { ( ◡ 𝐹 ‘ 𝑌 ) } ) = ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐹 “ { 𝑌 } ) ) )
13		fvex	⊢ ( ◡ 𝐹 ‘ 𝑋 ) ∈ V
14		fvex	⊢ ( ◡ 𝐹 ‘ 𝑌 ) ∈ V
15	13 14	xpsn	⊢ ( { ( ◡ 𝐹 ‘ 𝑋 ) } × { ( ◡ 𝐹 ‘ 𝑌 ) } ) = { ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ }
16	12 15	eqtr3di	⊢ ( 𝜑 → ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐹 “ { 𝑌 } ) ) = { ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ } )
17	16	iuneq1d	⊢ ( 𝜑 → ∪ 𝑝 ∈ ( ( ◡ 𝐹 “ { 𝑋 } ) × ( ◡ 𝐹 “ { 𝑌 } ) ) ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) = ∪ 𝑝 ∈ { ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ } ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
18	7 17	eqtrd	⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ∪ 𝑝 ∈ { ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ } ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) )
19		opex	⊢ ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ ∈ V
20		fveq2	⊢ ( 𝑝 = ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ → ( 𝐺 ‘ 𝑝 ) = ( 𝐺 ‘ ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ ) )
21		df-ov	⊢ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) = ( 𝐺 ‘ ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ )
22	20 21	eqtr4di	⊢ ( 𝑝 = ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ → ( 𝐺 ‘ 𝑝 ) = ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) )
23		fveq2	⊢ ( 𝑝 = ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ → ( 𝐻 ‘ 𝑝 ) = ( 𝐻 ‘ ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ ) )
24		df-ov	⊢ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) = ( 𝐻 ‘ ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ )
25	23 24	eqtr4di	⊢ ( 𝑝 = ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ → ( 𝐻 ‘ 𝑝 ) = ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) )
26	22 25	imaeq12d	⊢ ( 𝑝 = ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ → ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) = ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) “ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) )
27	19 26	iunxsn	⊢ ∪ 𝑝 ∈ { ⟨ ( ◡ 𝐹 ‘ 𝑋 ) , ( ◡ 𝐹 ‘ 𝑌 ) ⟩ } ( ( 𝐺 ‘ 𝑝 ) “ ( 𝐻 ‘ 𝑝 ) ) = ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) “ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) )
28	18 27	eqtrdi	⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) “ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) )