This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ¬ ( 𝑋 𝐻 𝑌 ) = ∅ )