Theorem 0funcg

Description: The functor from the empty category. Corollary of Definition 3.47 of Adamek p. 40, Definition 7.1 of Adamek p. 101, Example 3.3(4.c) of Adamek p. 24, and Example 7.2(3) of Adamek p. 101. (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 𝐷 ) = { ⟨ ∅ , ∅ ⟩ } )