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 ⊢ B = Base C
fulltermc.h ⊢ H = Hom ⁡ C
fulltermc.d No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
fulltermc2.f ⊢ φ → F C Full D G
fulltermc2.x ⊢ φ → X ∈ B
fulltermc2.y ⊢ φ → Y ∈ B
Assertion fulltermc2 ⊢ φ → ¬ X H Y = ∅

Proof

Step Hyp Ref Expression
1 fulltermc.b ⊢ B = Base C
2 fulltermc.h ⊢ H = Hom ⁡ C
3 fulltermc.d Could not format ( ph -> D e. TermCat ) : No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
4 fulltermc2.f ⊢ φ → F C Full D G
5 fulltermc2.x ⊢ φ → X ∈ B
6 fulltermc2.y ⊢ φ → Y ∈ B
7 oveq1 ⊢ x = X → x H y = X H y
8 7 eqeq1d ⊢ x = X → x H y = ∅ ↔ X H y = ∅
9 8 notbid ⊢ x = X → ¬ x H y = ∅ ↔ ¬ X H y = ∅
10 oveq2 ⊢ y = Y → X H y = X H Y
11 10 eqeq1d ⊢ y = Y → X H y = ∅ ↔ X H Y = ∅
12 11 notbid ⊢ y = Y → ¬ X H y = ∅ ↔ ¬ X H Y = ∅
13 fullfunc ⊢ C Full D ⊆ C Func D
14 13 ssbri ⊢ F C Full D G → F C Func D G
15 4 14 syl ⊢ φ → F C Func D G
16 1 2 3 15 fulltermc ⊢ φ → F C Full D G ↔ ∀ x ∈ B ∀ y ∈ B ¬ x H y = ∅
17 4 16 mpbid ⊢ φ → ∀ x ∈ B ∀ y ∈ B ¬ x H y = ∅
18 9 12 17 5 6 rspc2dv ⊢ φ → ¬ X H Y = ∅