Metamath Proof Explorer

Theorem homffval

Description: Value of the functionalized Hom-set operation. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

Ref Expression
Hypotheses homffval.f ⊢ F = Hom 𝑓 ⁡ C
homffval.b ⊢ B = Base C
homffval.h ⊢ H = Hom ⁡ C
Assertion homffval ⊢ F = x ∈ B , y ∈ B ⟼ x H y

Proof

Step Hyp Ref Expression
1 homffval.f ⊢ F = Hom 𝑓 ⁡ C
2 homffval.b ⊢ B = Base C
3 homffval.h ⊢ H = Hom ⁡ C
4 fveq2 ⊢ c = C → Base c = Base C
5 4 2 eqtr4di ⊢ c = C → Base c = B
6 fveq2 ⊢ c = C → Hom ⁡ c = Hom ⁡ C
7 6 3 eqtr4di ⊢ c = C → Hom ⁡ c = H
8 7 oveqd ⊢ c = C → x Hom ⁡ c y = x H y
9 5 5 8 mpoeq123dv ⊢ c = C → x ∈ Base c , y ∈ Base c ⟼ x Hom ⁡ c y = x ∈ B , y ∈ B ⟼ x H y
10 df-homf ⊢ Hom 𝑓 = c ∈ V ⟼ x ∈ Base c , y ∈ Base c ⟼ x Hom ⁡ c y
11 2 fvexi ⊢ B ∈ V
12 11 11 mpoex ⊢ x ∈ B , y ∈ B ⟼ x H y ∈ V
13 9 10 12 fvmpt ⊢ C ∈ V → Hom 𝑓 ⁡ C = x ∈ B , y ∈ B ⟼ x H y
14 fvprc ⊢ ¬ C ∈ V → Hom 𝑓 ⁡ C = ∅
15 fvprc ⊢ ¬ C ∈ V → Base C = ∅
16 2 15 syl5eq ⊢ ¬ C ∈ V → B = ∅
17 16 olcd ⊢ ¬ C ∈ V → B = ∅ ∨ B = ∅
18 0mpo0 ⊢ B = ∅ ∨ B = ∅ → x ∈ B , y ∈ B ⟼ x H y = ∅
19 17 18 syl ⊢ ¬ C ∈ V → x ∈ B , y ∈ B ⟼ x H y = ∅
20 14 19 eqtr4d ⊢ ¬ C ∈ V → Hom 𝑓 ⁡ C = x ∈ B , y ∈ B ⟼ x H y
21 13 20 pm2.61i ⊢ Hom 𝑓 ⁡ C = x ∈ B , y ∈ B ⟼ x H y
22 1 21 eqtri ⊢ F = x ∈ B , y ∈ B ⟼ x H y