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 ⊢ S = F A
imaf1hom.1 ⊢ φ → F : B ⟶ 1-1 C
imaf1hom.x ⊢ φ → X ∈ S
imaf1hom.y ⊢ φ → Y ∈ S
imaf1hom.f ⊢ φ → F ∈ V
imaf1hom.k ⊢ K = x ∈ S , y ∈ S ⟼ ⋃ p ∈ F -1 x × F -1 y G ⁡ p H ⁡ p
Assertion imaf1hom ⊢ φ → X K Y = F -1 ⁡ X G F -1 ⁡ Y F -1 ⁡ X H F -1 ⁡ Y

Proof

Step Hyp Ref Expression
1 imaf1hom.s ⊢ S = F A
2 imaf1hom.1 ⊢ φ → F : B ⟶ 1-1 C
3 imaf1hom.x ⊢ φ → X ∈ S
4 imaf1hom.y ⊢ φ → Y ∈ S
5 imaf1hom.f ⊢ φ → F ∈ V
6 imaf1hom.k ⊢ K = x ∈ S , y ∈ S ⟼ ⋃ p ∈ F -1 x × F -1 y G ⁡ p H ⁡ p
7 5 5 3 4 6 imasubclem3 ⊢ φ → X K Y = ⋃ p ∈ F -1 X × F -1 Y G ⁡ p H ⁡ p
8 1 2 3 imaf1homlem ⊢ φ → F -1 ⁡ X = F -1 X ∧ F ⁡ F -1 ⁡ X = X ∧ F -1 ⁡ X ∈ B
9 8 simp1d ⊢ φ → F -1 ⁡ X = F -1 X
10 1 2 4 imaf1homlem ⊢ φ → F -1 ⁡ Y = F -1 Y ∧ F ⁡ F -1 ⁡ Y = Y ∧ F -1 ⁡ Y ∈ B
11 10 simp1d ⊢ φ → F -1 ⁡ Y = F -1 Y
12 9 11 xpeq12d ⊢ φ → F -1 ⁡ X × F -1 ⁡ Y = F -1 X × F -1 Y
13 fvex ⊢ F -1 ⁡ X ∈ V
14 fvex ⊢ F -1 ⁡ Y ∈ V
15 13 14 xpsn ⊢ F -1 ⁡ X × F -1 ⁡ Y = F -1 ⁡ X F -1 ⁡ Y
16 12 15 eqtr3di ⊢ φ → F -1 X × F -1 Y = F -1 ⁡ X F -1 ⁡ Y
17 16 iuneq1d ⊢ φ → ⋃ p ∈ F -1 X × F -1 Y G ⁡ p H ⁡ p = ⋃ p ∈ F -1 ⁡ X F -1 ⁡ Y G ⁡ p H ⁡ p
18 7 17 eqtrd ⊢ φ → X K Y = ⋃ p ∈ F -1 ⁡ X F -1 ⁡ Y G ⁡ p H ⁡ p
19 opex ⊢ F -1 ⁡ X F -1 ⁡ Y ∈ V
20 fveq2 ⊢ p = F -1 ⁡ X F -1 ⁡ Y → G ⁡ p = G ⁡ F -1 ⁡ X F -1 ⁡ Y
21 df-ov ⊢ F -1 ⁡ X G F -1 ⁡ Y = G ⁡ F -1 ⁡ X F -1 ⁡ Y
22 20 21 eqtr4di ⊢ p = F -1 ⁡ X F -1 ⁡ Y → G ⁡ p = F -1 ⁡ X G F -1 ⁡ Y
23 fveq2 ⊢ p = F -1 ⁡ X F -1 ⁡ Y → H ⁡ p = H ⁡ F -1 ⁡ X F -1 ⁡ Y
24 df-ov ⊢ F -1 ⁡ X H F -1 ⁡ Y = H ⁡ F -1 ⁡ X F -1 ⁡ Y
25 23 24 eqtr4di ⊢ p = F -1 ⁡ X F -1 ⁡ Y → H ⁡ p = F -1 ⁡ X H F -1 ⁡ Y
26 22 25 imaeq12d ⊢ p = F -1 ⁡ X F -1 ⁡ Y → G ⁡ p H ⁡ p = F -1 ⁡ X G F -1 ⁡ Y F -1 ⁡ X H F -1 ⁡ Y
27 19 26 iunxsn ⊢ ⋃ p ∈ F -1 ⁡ X F -1 ⁡ Y G ⁡ p H ⁡ p = F -1 ⁡ X G F -1 ⁡ Y F -1 ⁡ X H F -1 ⁡ Y
28 18 27 eqtrdi ⊢ φ → X K Y = F -1 ⁡ X G F -1 ⁡ Y F -1 ⁡ X H F -1 ⁡ Y