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

Metamath Proof Explorer

Theorem functermc

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 functermc ⊢ φ → K D Func E L ↔ K = F ∧ L = 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 simpr ⊢ φ ∧ K D Func E L → K D Func E L
10 3 4 9 funcf1 ⊢ φ ∧ K D Func E L → K : B ⟶ C
11 2 4 termcbas ⊢ φ → ∃ z C = z
12 feq3 ⊢ C = z → K : B ⟶ C ↔ K : B ⟶ z
13 vex ⊢ z ∈ V
14 13 fconst2 ⊢ K : B ⟶ z ↔ K = B × z
15 xpeq2 ⊢ C = z → B × C = B × z
16 7 15 eqtrid ⊢ C = z → F = B × z
17 16 eqeq2d ⊢ C = z → K = F ↔ K = B × z
18 14 17 bitr4id ⊢ C = z → K : B ⟶ z ↔ K = F
19 12 18 bitrd ⊢ C = z → K : B ⟶ C ↔ K = F
20 19 exlimiv ⊢ ∃ z C = z → K : B ⟶ C ↔ K = F
21 11 20 syl ⊢ φ → K : B ⟶ C ↔ K = F
22 21 biimpa ⊢ φ ∧ K : B ⟶ C → K = F
23 10 22 syldan ⊢ φ ∧ K D Func E L → K = F
24 2 termcthind ⊢ φ → E ∈ ThinCat
25 13 fconst ⊢ B × z : B ⟶ z
26 16 feq1d ⊢ C = z → F : B ⟶ C ↔ B × z : B ⟶ C
27 feq3 ⊢ C = z → B × z : B ⟶ C ↔ B × z : B ⟶ z
28 26 27 bitrd ⊢ C = z → F : B ⟶ C ↔ B × z : B ⟶ z
29 25 28 mpbiri ⊢ C = z → F : B ⟶ C
30 29 exlimiv ⊢ ∃ z C = z → F : B ⟶ C
31 11 30 syl ⊢ φ → F : B ⟶ C
32 2 adantr Could not format ( ( ph /\ ( z e. B /\ w e. B ) ) -> E e. TermCat ) : No typesetting found for |- ( ( ph /\ ( z e. B /\ w e. B ) ) -> E e. TermCat ) with typecode |-
33 31 ffvelcdmda ⊢ φ ∧ z ∈ B → F ⁡ z ∈ C
34 33 adantrr ⊢ φ ∧ z ∈ B ∧ w ∈ B → F ⁡ z ∈ C
35 31 ffvelcdmda ⊢ φ ∧ w ∈ B → F ⁡ w ∈ C
36 35 adantrl ⊢ φ ∧ z ∈ B ∧ w ∈ B → F ⁡ w ∈ C
37 32 4 34 36 6 termchomn0 ⊢ φ ∧ z ∈ B ∧ w ∈ B → ¬ F ⁡ z J F ⁡ w = ∅
38 37 pm2.21d ⊢ φ ∧ z ∈ B ∧ w ∈ B → F ⁡ z J F ⁡ w = ∅ → z H w = ∅
39 38 ralrimivva ⊢ φ → ∀ z ∈ B ∀ w ∈ B F ⁡ z J F ⁡ w = ∅ → z H w = ∅
40 3 4 5 6 1 24 31 8 39 functhinc ⊢ φ → F D Func E L ↔ L = G
41 23 40 functermclem ⊢ φ → K D Func E L ↔ K = F ∧ L = G