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 ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝐻 𝑦 ) = ( 𝑥 𝐽 𝑦 ) ) )