Metamath Proof Explorer

Theorem functermc2

Description: Functor to a terminal category. (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses functermc.d ⊢ φ → D ∈ Cat
functermc.e No typesetting found for |- ( ph -> E e. TermCat ) with typecode |-
functermc.b ⊢ B = Base D
functermc.c ⊢ C = Base E
functermc.h ⊢ H = Hom ⁡ D
functermc.j ⊢ J = Hom ⁡ E
functermc.f ⊢ F = B × C
functermc.g ⊢ G = x ∈ B , y ∈ B ⟼ x H y × F ⁡ x J F ⁡ y
Assertion functermc2 ⊢ φ → D Func E = F G

Proof

Step Hyp Ref Expression
1 functermc.d ⊢ φ → D ∈ Cat
2 functermc.e Could not format ( ph -> E e. TermCat ) : No typesetting found for |- ( ph -> E e. TermCat ) with typecode |-
3 functermc.b ⊢ B = Base D
4 functermc.c ⊢ C = Base E
5 functermc.h ⊢ H = Hom ⁡ D
6 functermc.j ⊢ J = Hom ⁡ E
7 functermc.f ⊢ F = B × C
8 functermc.g ⊢ G = x ∈ B , y ∈ B ⟼ x H y × F ⁡ x J F ⁡ y
9 relfunc ⊢ Rel ⁡ D Func E
10 3 fvexi ⊢ B ∈ V
11 4 fvexi ⊢ C ∈ V
12 10 11 xpex ⊢ B × C ∈ V
13 7 12 eqeltri ⊢ F ∈ V
14 10 10 mpoex ⊢ x ∈ B , y ∈ B ⟼ x H y × F ⁡ x J F ⁡ y ∈ V
15 8 14 eqeltri ⊢ G ∈ V
16 13 15 relsnop ⊢ Rel ⁡ F G
17 1 2 3 4 5 6 7 8 functermc ⊢ φ → z D Func E w ↔ z = F ∧ w = G
18 brsnop ⊢ F ∈ V ∧ G ∈ V → z F G w ↔ z = F ∧ w = G
19 13 15 18 mp2an ⊢ z F G w ↔ z = F ∧ w = G
20 17 19 bitr4di ⊢ φ → z D Func E w ↔ z F G w
21 9 16 20 eqbrrdiv ⊢ φ → D Func E = F G