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

Metamath Proof Explorer

Theorem homfeq

Description: Condition for two categories with the same base to have the same hom-sets. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses homfeq.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
homfeq.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
homfeq.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
homfeq.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐷 ) )
Assertion homfeq ( 𝜑 → ( ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) = ( 𝑥 𝐽 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 homfeq.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
2 homfeq.j ⊢ 𝐽 = ( Hom ‘ 𝐷 )
3 homfeq.1 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
4 homfeq.2 ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐷 ) )
5 eqid ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
6 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 5 6 1 homffval ⊢ ( Homf ‘ 𝐶 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 𝐻 𝑦 ) )
8 eqidd ⊢ ( 𝜑 → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
9 3 3 8 mpoeq123dv ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 𝐻 𝑦 ) ) )
10 7 9 eqtr4id ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) )
11 eqid ⊢ ( Homf ‘ 𝐷 ) = ( Homf ‘ 𝐷 )
12 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
13 11 12 2 homffval ⊢ ( Homf ‘ 𝐷 ) = ( 𝑥 ∈ ( Base ‘ 𝐷 ) , 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 𝐽 𝑦 ) )
14 eqidd ⊢ ( 𝜑 → ( 𝑥 𝐽 𝑦 ) = ( 𝑥 𝐽 𝑦 ) )
15 4 4 14 mpoeq123dv ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐽 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐷 ) , 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 𝐽 𝑦 ) ) )
16 13 15 eqtr4id ⊢ ( 𝜑 → ( Homf ‘ 𝐷 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐽 𝑦 ) ) )
17 10 16 eqeq12d ⊢ ( 𝜑 → ( ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) ↔ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐽 𝑦 ) ) ) )
18 ovex ⊢ ( 𝑥 𝐻 𝑦 ) ∈ V
19 18 rgen2w ⊢ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ V
20 mpo2eqb ⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) ∈ V → ( ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐽 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) = ( 𝑥 𝐽 𝑦 ) ) )
21 19 20 ax-mp ⊢ ( ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐻 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 𝐽 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) = ( 𝑥 𝐽 𝑦 ) )
22 17 21 bitrdi ⊢ ( 𝜑 → ( ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) = ( 𝑥 𝐽 𝑦 ) ) )