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 ) = (/) <-> ( Homf ` C ) = (/) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
2 eqid 
 |-  ( Base ` C ) = ( Base ` C )
3 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
4 1 2 3 homffval 
 |-  ( Homf ` C ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( Hom ` C ) y ) )
5 0mpo0 
 |-  ( ( ( Base ` C ) = (/) \/ ( Base ` C ) = (/) ) -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( Hom ` C ) y ) ) = (/) )
6 5 orcs 
 |-  ( ( Base ` C ) = (/) -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x ( Hom ` C ) y ) ) = (/) )
7 4 6 eqtrid 
 |-  ( ( Base ` C ) = (/) -> ( Homf ` C ) = (/) )
8 1 2 homffn 
 |-  ( Homf ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) )
9 f0bi 
 |-  ( ( Homf ` C ) : (/) --> (/) <-> ( Homf ` C ) = (/) )
10 ffn 
 |-  ( ( Homf ` C ) : (/) --> (/) -> ( Homf ` C ) Fn (/) )
11 9 10 sylbir 
 |-  ( ( Homf ` C ) = (/) -> ( Homf ` C ) Fn (/) )
12 fndmu 
 |-  ( ( ( Homf ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) /\ ( Homf ` C ) Fn (/) ) -> ( ( Base ` C ) X. ( Base ` C ) ) = (/) )
13 8 11 12 sylancr 
 |-  ( ( Homf ` C ) = (/) -> ( ( Base ` C ) X. ( Base ` C ) ) = (/) )
14 xpeq0 
 |-  ( ( ( Base ` C ) X. ( Base ` C ) ) = (/) <-> ( ( Base ` C ) = (/) \/ ( Base ` C ) = (/) ) )
15 pm4.25 
 |-  ( ( Base ` C ) = (/) <-> ( ( Base ` C ) = (/) \/ ( Base ` C ) = (/) ) )
16 14 15 bitr4i 
 |-  ( ( ( Base ` C ) X. ( Base ` C ) ) = (/) <-> ( Base ` C ) = (/) )
17 13 16 sylib 
 |-  ( ( Homf ` C ) = (/) -> ( Base ` C ) = (/) )
18 7 17 impbii 
 |-  ( ( Base ` C ) = (/) <-> ( Homf ` C ) = (/) )