Metamath Proof Explorer

Theorem homaf

Description: Functionality 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
Assertion homaf ⊢ φ → H : B × B ⟶ 𝒫 B × B × V

Proof

Step Hyp Ref Expression
1 homarcl.h ⊢ H = Hom a ⁡ C
2 homafval.b ⊢ B = Base C
3 homafval.c ⊢ φ → C ∈ Cat
4 eqid ⊢ Hom ⁡ C = Hom ⁡ C
5 1 2 3 4 homafval ⊢ φ → H = x ∈ B × B ⟼ x × Hom ⁡ C ⁡ x
6 snssi ⊢ x ∈ B × B → x ⊆ B × B
7 6 adantl ⊢ φ ∧ x ∈ B × B → x ⊆ B × B
8 ssv ⊢ Hom ⁡ C ⁡ x ⊆ V
9 xpss12 ⊢ x ⊆ B × B ∧ Hom ⁡ C ⁡ x ⊆ V → x × Hom ⁡ C ⁡ x ⊆ B × B × V
10 7 8 9 sylancl ⊢ φ ∧ x ∈ B × B → x × Hom ⁡ C ⁡ x ⊆ B × B × V
11 snex ⊢ x ∈ V
12 fvex ⊢ Hom ⁡ C ⁡ x ∈ V
13 11 12 xpex ⊢ x × Hom ⁡ C ⁡ x ∈ V
14 13 elpw ⊢ x × Hom ⁡ C ⁡ x ∈ 𝒫 B × B × V ↔ x × Hom ⁡ C ⁡ x ⊆ B × B × V
15 10 14 sylibr ⊢ φ ∧ x ∈ B × B → x × Hom ⁡ C ⁡ x ∈ 𝒫 B × B × V
16 5 15 fmpt3d ⊢ φ → H : B × B ⟶ 𝒫 B × B × V