Metamath Proof Explorer

Theorem elhoma

Description: Value of the disjointified hom-set function. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses homarcl.h ⊢ H = Hom a ⁡ C
homafval.b ⊢ B = Base C
homafval.c ⊢ φ → C ∈ Cat
homaval.j ⊢ J = Hom ⁡ C
homaval.x ⊢ φ → X ∈ B
homaval.y ⊢ φ → Y ∈ B
Assertion elhoma ⊢ φ → Z X H Y F ↔ Z = X Y ∧ F ∈ X J Y

Proof

Step Hyp Ref Expression
1 homarcl.h ⊢ H = Hom a ⁡ C
2 homafval.b ⊢ B = Base C
3 homafval.c ⊢ φ → C ∈ Cat
4 homaval.j ⊢ J = Hom ⁡ C
5 homaval.x ⊢ φ → X ∈ B
6 homaval.y ⊢ φ → Y ∈ B
7 1 2 3 4 5 6 homaval ⊢ φ → X H Y = X Y × X J Y
8 7 breqd ⊢ φ → Z X H Y F ↔ Z X Y × X J Y F
9 brxp ⊢ Z X Y × X J Y F ↔ Z ∈ X Y ∧ F ∈ X J Y
10 opex ⊢ X Y ∈ V
11 10 elsn2 ⊢ Z ∈ X Y ↔ Z = X Y
12 11 anbi1i ⊢ Z ∈ X Y ∧ F ∈ X J Y ↔ Z = X Y ∧ F ∈ X J Y
13 9 12 bitri ⊢ Z X Y × X J Y F ↔ Z = X Y ∧ F ∈ X J Y
14 8 13 bitrdi ⊢ φ → Z X H Y F ↔ Z = X Y ∧ F ∈ X J Y