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

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 ⊢ 𝐻 = ( Homa ‘ 𝐶 )
homafval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
homafval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
Assertion homaf ( 𝜑 → 𝐻 : ( 𝐵 × 𝐵 ) ⟶ 𝒫 ( ( 𝐵 × 𝐵 ) × V ) )

Proof

Step Hyp Ref Expression
1 homarcl.h ⊢ 𝐻 = ( Homa ‘ 𝐶 )
2 homafval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 homafval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
5 1 2 3 4 homafval ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) ↦ ( { 𝑥 } × ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) ) )
6 snssi ⊢ ( 𝑥 ∈ ( 𝐵 × 𝐵 ) → { 𝑥 } ⊆ ( 𝐵 × 𝐵 ) )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 × 𝐵 ) ) → { 𝑥 } ⊆ ( 𝐵 × 𝐵 ) )
8 ssv ⊢ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ⊆ V
9 xpss12 ⊢ ( ( { 𝑥 } ⊆ ( 𝐵 × 𝐵 ) ∧ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ⊆ V ) → ( { 𝑥 } × ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) ⊆ ( ( 𝐵 × 𝐵 ) × V ) )
10 7 8 9 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 × 𝐵 ) ) → ( { 𝑥 } × ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) ⊆ ( ( 𝐵 × 𝐵 ) × V ) )
11 vsnex ⊢ { 𝑥 } ∈ V
12 fvex ⊢ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ∈ V
13 11 12 xpex ⊢ ( { 𝑥 } × ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) ∈ V
14 13 elpw ⊢ ( ( { 𝑥 } × ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) ∈ 𝒫 ( ( 𝐵 × 𝐵 ) × V ) ↔ ( { 𝑥 } × ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) ⊆ ( ( 𝐵 × 𝐵 ) × V ) )
15 10 14 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 × 𝐵 ) ) → ( { 𝑥 } × ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ) ∈ 𝒫 ( ( 𝐵 × 𝐵 ) × V ) )
16 5 15 fmpt3d ⊢ ( 𝜑 → 𝐻 : ( 𝐵 × 𝐵 ) ⟶ 𝒫 ( ( 𝐵 × 𝐵 ) × V ) )