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

Metamath Proof Explorer

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 ‘ 𝐶 ) = ∅ )