Metamath Proof Explorer

Theorem functhinc

Description: A functor to a thin category is determined entirely by the object part. The hypothesis "functhinc.1" is related to a monotone function if preorders induced by the categories are considered ( catprs2 ). (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Hypotheses functhinc.b ⊢B=BaseD
functhinc.c ⊢C=BaseE
functhinc.h ⊢H=Hom⁡D
functhinc.j ⊢J=Hom⁡E
functhinc.d ⊢φ→D∈Cat
functhinc.e No typesetting found for |- ( ph -> E e. ThinCat ) with typecode |-
functhinc.f ⊢φ→F:B⟶C
functhinc.k ⊢K=x∈B,y∈B⟼xHy×F⁡xJF⁡y
functhinc.1 ⊢φ→∀z∈B∀w∈BF⁡zJF⁡w=∅→zHw=∅
Assertion functhinc ⊢φ→FDFuncEG↔G=K

Proof

Step Hyp Ref Expression
1 functhinc.b ⊢B=BaseD
2 functhinc.c ⊢C=BaseE
3 functhinc.h ⊢H=Hom⁡D
4 functhinc.j ⊢J=Hom⁡E
5 functhinc.d ⊢φ→D∈Cat
6 functhinc.e Could not format ( ph -> E e. ThinCat ) : No typesetting found for |- ( ph -> E e. ThinCat ) with typecode |-
7 functhinc.f ⊢φ→F:B⟶C
8 functhinc.k ⊢K=x∈B,y∈B⟼xHy×F⁡xJF⁡y
9 functhinc.1 ⊢φ→∀z∈B∀w∈BF⁡zJF⁡w=∅→zHw=∅
10 eqid ⊢Id⁡D=Id⁡D
11 eqid ⊢Id⁡E=Id⁡E
12 eqid ⊢comp⁡D=comp⁡D
13 eqid ⊢comp⁡E=comp⁡E
14 6 thinccd ⊢φ→E∈Cat
15 1 2 3 4 10 11 12 13 5 14 isfunc ⊢φ→FDFuncEG↔F:B⟶C∧G∈⨉c∈B×BF⁡1st⁡cJF⁡2nd⁡cH⁡c∧∀a∈BaGa⁡Id⁡D⁡a=Id⁡E⁡F⁡a∧∀b∈B∀c∈B∀f∈aHb∀g∈bHcaGc⁡gabcomp⁡Dcf=bGc⁡gF⁡aF⁡bcomp⁡EF⁡caGb⁡f
16 3anass ⊢F:B⟶C∧G∈⨉c∈B×BF⁡1st⁡cJF⁡2nd⁡cH⁡c∧∀a∈BaGa⁡Id⁡D⁡a=Id⁡E⁡F⁡a∧∀b∈B∀c∈B∀f∈aHb∀g∈bHcaGc⁡gabcomp⁡Dcf=bGc⁡gF⁡aF⁡bcomp⁡EF⁡caGb⁡f↔F:B⟶C∧G∈⨉c∈B×BF⁡1st⁡cJF⁡2nd⁡cH⁡c∧∀a∈BaGa⁡Id⁡D⁡a=Id⁡E⁡F⁡a∧∀b∈B∀c∈B∀f∈aHb∀g∈bHcaGc⁡gabcomp⁡Dcf=bGc⁡gF⁡aF⁡bcomp⁡EF⁡caGb⁡f
17 15 16 bitrdi ⊢φ→FDFuncEG↔F:B⟶C∧G∈⨉c∈B×BF⁡1st⁡cJF⁡2nd⁡cH⁡c∧∀a∈BaGa⁡Id⁡D⁡a=Id⁡E⁡F⁡a∧∀b∈B∀c∈B∀f∈aHb∀g∈bHcaGc⁡gabcomp⁡Dcf=bGc⁡gF⁡aF⁡bcomp⁡EF⁡caGb⁡f
18 7 17 mpbirand ⊢φ→FDFuncEG↔G∈⨉c∈B×BF⁡1st⁡cJF⁡2nd⁡cH⁡c∧∀a∈BaGa⁡Id⁡D⁡a=Id⁡E⁡F⁡a∧∀b∈B∀c∈B∀f∈aHb∀g∈bHcaGc⁡gabcomp⁡Dcf=bGc⁡gF⁡aF⁡bcomp⁡EF⁡caGb⁡f
19 funcf2lem ⊢G∈⨉c∈B×BF⁡1st⁡cJF⁡2nd⁡cH⁡c↔G∈V∧GFnB×B∧∀v∈B∀u∈BvGu:vHu⟶F⁡vJF⁡u
20 simprl ⊢φ∧v∈B∧u∈B→v∈B
21 simprr ⊢φ∧v∈B∧u∈B→u∈B
22 9 adantr ⊢φ∧v∈B∧u∈B→∀z∈B∀w∈BF⁡zJF⁡w=∅→zHw=∅
23 20 21 22 functhinclem2 ⊢φ∧v∈B∧u∈B→F⁡vJF⁡u=∅→vHu=∅
24 1 2 3 4 6 7 8 23 functhinclem1 ⊢φ→G∈V∧GFnB×B∧∀v∈B∀u∈BvGu:vHu⟶F⁡vJF⁡u↔G=K
25 19 24 bitrid ⊢φ→G∈⨉c∈B×BF⁡1st⁡cJF⁡2nd⁡cH⁡c↔G=K
26 25 anbi1d ⊢φ→G∈⨉c∈B×BF⁡1st⁡cJF⁡2nd⁡cH⁡c∧∀a∈BaGa⁡Id⁡D⁡a=Id⁡E⁡F⁡a∧∀b∈B∀c∈B∀f∈aHb∀g∈bHcaGc⁡gabcomp⁡Dcf=bGc⁡gF⁡aF⁡bcomp⁡EF⁡caGb⁡f↔G=K∧∀a∈BaGa⁡Id⁡D⁡a=Id⁡E⁡F⁡a∧∀b∈B∀c∈B∀f∈aHb∀g∈bHcaGc⁡gabcomp⁡Dcf=bGc⁡gF⁡aF⁡bcomp⁡EF⁡caGb⁡f
27 18 26 bitrd ⊢φ→FDFuncEG↔G=K∧∀a∈BaGa⁡Id⁡D⁡a=Id⁡E⁡F⁡a∧∀b∈B∀c∈B∀f∈aHb∀g∈bHcaGc⁡gabcomp⁡Dcf=bGc⁡gF⁡aF⁡bcomp⁡EF⁡caGb⁡f
28 1 2 3 4 5 6 7 8 9 10 11 12 13 functhinclem4 ⊢φ∧G=K→∀a∈BaGa⁡Id⁡D⁡a=Id⁡E⁡F⁡a∧∀b∈B∀c∈B∀f∈aHb∀g∈bHcaGc⁡gabcomp⁡Dcf=bGc⁡gF⁡aF⁡bcomp⁡EF⁡caGb⁡f
29 27 28 mpbiran3d ⊢φ→FDFuncEG↔G=K