This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 𝐾 𝑌 ) = ( ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐺 ( ◡ 𝐹 ‘ 𝑌 ) ) “ ( ( ◡ 𝐹 ‘ 𝑋 ) 𝐻 ( ◡ 𝐹 ‘ 𝑌 ) ) ) )