Theorem fulltermc2

Description: Given a full functor to a terminal category, the source category must not have empty hom-sets. (Contributed by Zhi Wang, 17-Oct-2025) (Proof shortened by Zhi Wang, 6-Nov-2025)

	Ref	Expression
Hypotheses	fulltermc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	fulltermc.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	fulltermc.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
	fulltermc2.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
	fulltermc2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	fulltermc2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	fulltermc2	⊢ ( 𝜑 → ¬ ( 𝑋 𝐻 𝑌 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		fulltermc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		fulltermc.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		fulltermc.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
4		fulltermc2.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 )
5		fulltermc2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		fulltermc2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑦 ) )
8	7	eqeq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( 𝑋 𝐻 𝑦 ) = ∅ ) )
9	8	notbid	⊢ ( 𝑥 = 𝑋 → ( ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ¬ ( 𝑋 𝐻 𝑦 ) = ∅ ) )
10		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
11	10	eqeq1d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 𝐻 𝑦 ) = ∅ ↔ ( 𝑋 𝐻 𝑌 ) = ∅ ) )
12	11	notbid	⊢ ( 𝑦 = 𝑌 → ( ¬ ( 𝑋 𝐻 𝑦 ) = ∅ ↔ ¬ ( 𝑋 𝐻 𝑌 ) = ∅ ) )
13		fullfunc	⊢ ( 𝐶 Full 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
14	13	ssbri	⊢ ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
15	4 14	syl	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
16	1 2 3 15	fulltermc	⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) )
17	4 16	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ ( 𝑥 𝐻 𝑦 ) = ∅ )
18	9 12 17 5 6	rspc2dv	⊢ ( 𝜑 → ¬ ( 𝑋 𝐻 𝑌 ) = ∅ )