Theorem 0funcg

Description: The functor from the empty category. (Contributed by Zhi Wang, 17-Oct-2025)

	Ref	Expression
Hypotheses	0funcg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	0funcg.b	⊢ ( 𝜑 → ∅ = ( Base ‘ 𝐶 ) )
	0funcg.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion	0funcg	⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) = { ⟨ ∅ , ∅ ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		0funcg.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
2		0funcg.b	⊢ ( 𝜑 → ∅ = ( Base ‘ 𝐶 ) )
3		0funcg.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
4		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
5		0ex	⊢ ∅ ∈ V
6	5 5	relsnop	⊢ Rel { ⟨ ∅ , ∅ ⟩ }
7	1 2 3	0funcg2	⊢ ( 𝜑 → ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ↔ ( 𝑓 = ∅ ∧ 𝑔 = ∅ ) ) )
8		brsnop	⊢ ( ( ∅ ∈ V ∧ ∅ ∈ V ) → ( 𝑓 { ⟨ ∅ , ∅ ⟩ } 𝑔 ↔ ( 𝑓 = ∅ ∧ 𝑔 = ∅ ) ) )
9	5 5 8	mp2an	⊢ ( 𝑓 { ⟨ ∅ , ∅ ⟩ } 𝑔 ↔ ( 𝑓 = ∅ ∧ 𝑔 = ∅ ) )
10	7 9	bitr4di	⊢ ( 𝜑 → ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ↔ 𝑓 { ⟨ ∅ , ∅ ⟩ } 𝑔 ) )
11	4 6 10	eqbrrdiv	⊢ ( 𝜑 → ( 𝐶 Func 𝐷 ) = { ⟨ ∅ , ∅ ⟩ } )