Theorem 0func

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

	Ref	Expression
Hypothesis	0func.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
Assertion	0func	⊢ ( 𝜑 → ( ∅ Func 𝐶 ) = { ⟨ ∅ , ∅ ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		0func.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		relfunc	⊢ Rel ( ∅ Func 𝐶 )
3		0ex	⊢ ∅ ∈ V
4	3 3	relsnop	⊢ Rel { ⟨ ∅ , ∅ ⟩ }
5		base0	⊢ ∅ = ( Base ‘ ∅ )
6		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7		eqid	⊢ ( Hom ‘ ∅ ) = ( Hom ‘ ∅ )
8		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9		eqid	⊢ ( Id ‘ ∅ ) = ( Id ‘ ∅ )
10		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
11		eqid	⊢ ( comp ‘ ∅ ) = ( comp ‘ ∅ )
12		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
13		0cat	⊢ ∅ ∈ Cat
14	13	a1i	⊢ ( 𝜑 → ∅ ∈ Cat )
15	5 6 7 8 9 10 11 12 14 1	isfunc	⊢ ( 𝜑 → ( 𝑓 ( ∅ Func 𝐶 ) 𝑔 ↔ ( 𝑓 : ∅ ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ∅ × ∅ ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ ∅ ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ∅ ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ ∅ ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ ∅ ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ ∅ ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ∅ ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
16		f0bi	⊢ ( 𝑓 : ∅ ⟶ ( Base ‘ 𝐶 ) ↔ 𝑓 = ∅ )
17		ral0	⊢ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 𝑔 𝑦 ) : ( 𝑥 ( Hom ‘ ∅ ) 𝑦 ) ⟶ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) )
18	5	funcf2lem2	⊢ ( 𝑔 ∈ X 𝑧 ∈ ( ∅ × ∅ ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ ∅ ) ‘ 𝑧 ) ) ↔ ( 𝑔 Fn ( ∅ × ∅ ) ∧ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 𝑔 𝑦 ) : ( 𝑥 ( Hom ‘ ∅ ) 𝑦 ) ⟶ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) ) )
19	17 18	mpbiran2	⊢ ( 𝑔 ∈ X 𝑧 ∈ ( ∅ × ∅ ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ ∅ ) ‘ 𝑧 ) ) ↔ 𝑔 Fn ( ∅ × ∅ ) )
20		0xp	⊢ ( ∅ × ∅ ) = ∅
21	20	fneq2i	⊢ ( 𝑔 Fn ( ∅ × ∅ ) ↔ 𝑔 Fn ∅ )
22		fn0	⊢ ( 𝑔 Fn ∅ ↔ 𝑔 = ∅ )
23	19 21 22	3bitri	⊢ ( 𝑔 ∈ X 𝑧 ∈ ( ∅ × ∅ ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ ∅ ) ‘ 𝑧 ) ) ↔ 𝑔 = ∅ )
24		ral0	⊢ ∀ 𝑥 ∈ ∅ ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ ∅ ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ ∅ ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ ∅ ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ∅ ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) )
25	15 16 23 24	0funclem	⊢ ( 𝜑 → ( 𝑓 ( ∅ Func 𝐶 ) 𝑔 ↔ ( 𝑓 = ∅ ∧ 𝑔 = ∅ ) ) )
26		brsnop	⊢ ( ( ∅ ∈ V ∧ ∅ ∈ V ) → ( 𝑓 { ⟨ ∅ , ∅ ⟩ } 𝑔 ↔ ( 𝑓 = ∅ ∧ 𝑔 = ∅ ) ) )
27	3 3 26	mp2an	⊢ ( 𝑓 { ⟨ ∅ , ∅ ⟩ } 𝑔 ↔ ( 𝑓 = ∅ ∧ 𝑔 = ∅ ) )
28	25 27	bitr4di	⊢ ( 𝜑 → ( 𝑓 ( ∅ Func 𝐶 ) 𝑔 ↔ 𝑓 { ⟨ ∅ , ∅ ⟩ } 𝑔 ) )
29	2 4 28	eqbrrdiv	⊢ ( 𝜑 → ( ∅ Func 𝐶 ) = { ⟨ ∅ , ∅ ⟩ } )