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 C = ∅ ↔ Hom 𝑓 ⁡ C = ∅

Proof

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