Theorem homf0

Description: The base is empty iff the functionalized Hom-set operation is empty. (Contributed by Zhi Wang, 23-Oct-2025)

	Ref	Expression
Assertion	homf0	⊢ ( ( Base ‘ 𝐶 ) = ∅ ↔ ( Homf ‘ 𝐶 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
2		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
3		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
4	1 2 3	homffval	⊢ ( Homf ‘ 𝐶 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
5		0mpo0	⊢ ( ( ( Base ‘ 𝐶 ) = ∅ ∨ ( Base ‘ 𝐶 ) = ∅ ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) = ∅ )
6	5	orcs	⊢ ( ( Base ‘ 𝐶 ) = ∅ → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) = ∅ )
7	4 6	eqtrid	⊢ ( ( Base ‘ 𝐶 ) = ∅ → ( Homf ‘ 𝐶 ) = ∅ )
8	1 2	homffn	⊢ ( Homf ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
9		f0bi	⊢ ( ( Homf ‘ 𝐶 ) : ∅ ⟶ ∅ ↔ ( Homf ‘ 𝐶 ) = ∅ )
10		ffn	⊢ ( ( Homf ‘ 𝐶 ) : ∅ ⟶ ∅ → ( Homf ‘ 𝐶 ) Fn ∅ )
11	9 10	sylbir	⊢ ( ( Homf ‘ 𝐶 ) = ∅ → ( Homf ‘ 𝐶 ) Fn ∅ )
12		fndmu	⊢ ( ( ( Homf ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ ( Homf ‘ 𝐶 ) Fn ∅ ) → ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) = ∅ )
13	8 11 12	sylancr	⊢ ( ( Homf ‘ 𝐶 ) = ∅ → ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) = ∅ )
14		xpeq0	⊢ ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) = ∅ ↔ ( ( Base ‘ 𝐶 ) = ∅ ∨ ( Base ‘ 𝐶 ) = ∅ ) )
15		pm4.25	⊢ ( ( Base ‘ 𝐶 ) = ∅ ↔ ( ( Base ‘ 𝐶 ) = ∅ ∨ ( Base ‘ 𝐶 ) = ∅ ) )
16	14 15	bitr4i	⊢ ( ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) = ∅ ↔ ( Base ‘ 𝐶 ) = ∅ )
17	13 16	sylib	⊢ ( ( Homf ‘ 𝐶 ) = ∅ → ( Base ‘ 𝐶 ) = ∅ )
18	7 17	impbii	⊢ ( ( Base ‘ 𝐶 ) = ∅ ↔ ( Homf ‘ 𝐶 ) = ∅ )