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 ⊢ 𝐵 = ( Base ‘ 𝐶 )
fulltermc.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
fulltermc.d ⊢ ( 𝜑 → 𝐷 ∈ TermCat )
fulltermc.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
Assertion fulltermc ( 𝜑 → ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 fulltermc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 fulltermc.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 fulltermc.d ⊢ ( 𝜑 → 𝐷 ∈ TermCat )
4 fulltermc.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
5 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
6 3 termcthind ⊢ ( 𝜑 → 𝐷 ∈ ThinCat )
7 1 5 2 6 4 fullthinc ⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) )
8 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐷 ∈ TermCat )
9 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
10 1 9 4 funcf1 ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
11 10 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
12 11 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
13 10 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
14 13 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
15 8 9 12 14 5 termchomn0 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ¬ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) = ∅ )
16 biimt ⊢ ( ¬ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) = ∅ → ( ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ¬ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) = ∅ → ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) ) )
17 15 16 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ¬ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) = ∅ → ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) ) )
18 con34b ⊢ ( ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ↔ ( ¬ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) = ∅ → ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) )
19 17 18 bitr4di ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) )
20 19 2ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) )
21 7 20 bitr4d ⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Full 𝐷 ) 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ ( 𝑥 𝐻 𝑦 ) = ∅ ) )