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

Metamath Proof Explorer

Theorem fulltermc

Description: A functor to a terminal category is full iff all hom-sets of the source category are non-empty. (Contributed by Zhi Wang, 17-Oct-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 |-
fulltermc.f ⊢ φ → F C Func D G
Assertion fulltermc ⊢ φ → F C Full D G ↔ ∀ x ∈ B ∀ y ∈ B ¬ 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 fulltermc.f ⊢ φ → F C Func D G
5 eqid ⊢ Hom ⁡ D = Hom ⁡ D
6 3 termcthind ⊢ φ → D ∈ ThinCat
7 1 5 2 6 4 fullthinc ⊢ φ → F C Full D G ↔ ∀ x ∈ B ∀ y ∈ B x H y = ∅ → F ⁡ x Hom ⁡ D F ⁡ y = ∅
8 3 adantr Could not format ( ( ph /\ ( x e. B /\ y e. B ) ) -> D e. TermCat ) : No typesetting found for |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> D e. TermCat ) with typecode |-
9 eqid ⊢ Base D = Base D
10 1 9 4 funcf1 ⊢ φ → F : B ⟶ Base D
11 10 ffvelcdmda ⊢ φ ∧ x ∈ B → F ⁡ x ∈ Base D
12 11 adantrr ⊢ φ ∧ x ∈ B ∧ y ∈ B → F ⁡ x ∈ Base D
13 10 ffvelcdmda ⊢ φ ∧ y ∈ B → F ⁡ y ∈ Base D
14 13 adantrl ⊢ φ ∧ x ∈ B ∧ y ∈ B → F ⁡ y ∈ Base D
15 8 9 12 14 5 termchomn0 ⊢ φ ∧ x ∈ B ∧ y ∈ B → ¬ F ⁡ x Hom ⁡ D F ⁡ y = ∅
16 biimt ⊢ ¬ F ⁡ x Hom ⁡ D F ⁡ y = ∅ → ¬ x H y = ∅ ↔ ¬ F ⁡ x Hom ⁡ D F ⁡ y = ∅ → ¬ x H y = ∅
17 15 16 syl ⊢ φ ∧ x ∈ B ∧ y ∈ B → ¬ x H y = ∅ ↔ ¬ F ⁡ x Hom ⁡ D F ⁡ y = ∅ → ¬ x H y = ∅
18 con34b ⊢ x H y = ∅ → F ⁡ x Hom ⁡ D F ⁡ y = ∅ ↔ ¬ F ⁡ x Hom ⁡ D F ⁡ y = ∅ → ¬ x H y = ∅
19 17 18 bitr4di ⊢ φ ∧ x ∈ B ∧ y ∈ B → ¬ x H y = ∅ ↔ x H y = ∅ → F ⁡ x Hom ⁡ D F ⁡ y = ∅
20 19 2ralbidva ⊢ φ → ∀ x ∈ B ∀ y ∈ B ¬ x H y = ∅ ↔ ∀ x ∈ B ∀ y ∈ B x H y = ∅ → F ⁡ x Hom ⁡ D F ⁡ y = ∅
21 7 20 bitr4d ⊢ φ → F C Full D G ↔ ∀ x ∈ B ∀ y ∈ B ¬ x H y = ∅