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)

	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		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
14	1 13	isfull	⊢ ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝐺 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) ) )
15	4 14	sylib	⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ran ( 𝑥 𝐺 𝑦 ) = ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) ) )
16	15	simpld	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
17	1 2 3 16	fulltermc	⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) )
18	4 17	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ ( 𝑥 𝐻 𝑦 ) = ∅ )
19	9 12 18 5 6	rspc2dv	⊢ ( 𝜑 → ¬ ( 𝑋 𝐻 𝑌 ) = ∅ )