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 ), and can be obtained from funcf2 , f002 , and ralrimivva . (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Hypotheses functhinc.b ⊢ B = Base D
functhinc.c ⊢ C = Base E
functhinc.h ⊢ H = Hom ⁡ D
functhinc.j ⊢ J = Hom ⁡ E
functhinc.d ⊢ φ → D ∈ Cat
functhinc.e ⊢ φ → E ∈ ThinCat
functhinc.f ⊢ φ → F : B ⟶ C
functhinc.k ⊢ K = x ∈ B , y ∈ B ⟼ x H y × F ⁡ x J F ⁡ y
functhinc.1 ⊢ φ → ∀ z ∈ B ∀ w ∈ B F ⁡ z J F ⁡ w = ∅ → z H w = ∅
Assertion functhinc ⊢ φ → F D Func E G ↔ G = K

Proof

Step Hyp Ref Expression
1 functhinc.b ⊢ B = Base D
2 functhinc.c ⊢ C = Base E
3 functhinc.h ⊢ H = Hom ⁡ D
4 functhinc.j ⊢ J = Hom ⁡ E
5 functhinc.d ⊢ φ → D ∈ Cat
6 functhinc.e ⊢ φ → E ∈ ThinCat
7 functhinc.f ⊢ φ → F : B ⟶ C
8 functhinc.k ⊢ K = x ∈ B , y ∈ B ⟼ x H y × F ⁡ x J F ⁡ y
9 functhinc.1 ⊢ φ → ∀ z ∈ B ∀ w ∈ B F ⁡ z J F ⁡ w = ∅ → z H w = ∅
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 ⊢ φ → F D Func E G ↔ F : B ⟶ C ∧ G ∈ ⨉ c ∈ B × B F ⁡ 1 st ⁡ c J F ⁡ 2 nd ⁡ c H ⁡ c ∧ ∀ a ∈ B a G a ⁡ Id ⁡ D ⁡ a = Id ⁡ E ⁡ F ⁡ a ∧ ∀ b ∈ B ∀ c ∈ B ∀ f ∈ a H b ∀ g ∈ b H c a G c ⁡ g a b comp ⁡ D c f = b G c ⁡ g F ⁡ a F ⁡ b comp ⁡ E F ⁡ c a G b ⁡ f
16 3anass ⊢ F : B ⟶ C ∧ G ∈ ⨉ c ∈ B × B F ⁡ 1 st ⁡ c J F ⁡ 2 nd ⁡ c H ⁡ c ∧ ∀ a ∈ B a G a ⁡ Id ⁡ D ⁡ a = Id ⁡ E ⁡ F ⁡ a ∧ ∀ b ∈ B ∀ c ∈ B ∀ f ∈ a H b ∀ g ∈ b H c a G c ⁡ g a b comp ⁡ D c f = b G c ⁡ g F ⁡ a F ⁡ b comp ⁡ E F ⁡ c a G b ⁡ f ↔ F : B ⟶ C ∧ G ∈ ⨉ c ∈ B × B F ⁡ 1 st ⁡ c J F ⁡ 2 nd ⁡ c H ⁡ c ∧ ∀ a ∈ B a G a ⁡ Id ⁡ D ⁡ a = Id ⁡ E ⁡ F ⁡ a ∧ ∀ b ∈ B ∀ c ∈ B ∀ f ∈ a H b ∀ g ∈ b H c a G c ⁡ g a b comp ⁡ D c f = b G c ⁡ g F ⁡ a F ⁡ b comp ⁡ E F ⁡ c a G b ⁡ f
17 15 16 bitrdi ⊢ φ → F D Func E G ↔ F : B ⟶ C ∧ G ∈ ⨉ c ∈ B × B F ⁡ 1 st ⁡ c J F ⁡ 2 nd ⁡ c H ⁡ c ∧ ∀ a ∈ B a G a ⁡ Id ⁡ D ⁡ a = Id ⁡ E ⁡ F ⁡ a ∧ ∀ b ∈ B ∀ c ∈ B ∀ f ∈ a H b ∀ g ∈ b H c a G c ⁡ g a b comp ⁡ D c f = b G c ⁡ g F ⁡ a F ⁡ b comp ⁡ E F ⁡ c a G b ⁡ f
18 7 17 mpbirand ⊢ φ → F D Func E G ↔ G ∈ ⨉ c ∈ B × B F ⁡ 1 st ⁡ c J F ⁡ 2 nd ⁡ c H ⁡ c ∧ ∀ a ∈ B a G a ⁡ Id ⁡ D ⁡ a = Id ⁡ E ⁡ F ⁡ a ∧ ∀ b ∈ B ∀ c ∈ B ∀ f ∈ a H b ∀ g ∈ b H c a G c ⁡ g a b comp ⁡ D c f = b G c ⁡ g F ⁡ a F ⁡ b comp ⁡ E F ⁡ c a G b ⁡ f
19 funcf2lem ⊢ G ∈ ⨉ c ∈ B × B F ⁡ 1 st ⁡ c J F ⁡ 2 nd ⁡ c H ⁡ c ↔ G ∈ V ∧ G Fn B × B ∧ ∀ v ∈ B ∀ u ∈ B v G u : v H u ⟶ F ⁡ v J F ⁡ 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 ∈ B F ⁡ z J F ⁡ w = ∅ → z H w = ∅
23 20 21 22 functhinclem2 ⊢ φ ∧ v ∈ B ∧ u ∈ B → F ⁡ v J F ⁡ u = ∅ → v H u = ∅
24 1 2 3 4 6 7 8 23 functhinclem1 ⊢ φ → G ∈ V ∧ G Fn B × B ∧ ∀ v ∈ B ∀ u ∈ B v G u : v H u ⟶ F ⁡ v J F ⁡ u ↔ G = K
25 19 24 bitrid ⊢ φ → G ∈ ⨉ c ∈ B × B F ⁡ 1 st ⁡ c J F ⁡ 2 nd ⁡ c H ⁡ c ↔ G = K
26 25 anbi1d ⊢ φ → G ∈ ⨉ c ∈ B × B F ⁡ 1 st ⁡ c J F ⁡ 2 nd ⁡ c H ⁡ c ∧ ∀ a ∈ B a G a ⁡ Id ⁡ D ⁡ a = Id ⁡ E ⁡ F ⁡ a ∧ ∀ b ∈ B ∀ c ∈ B ∀ f ∈ a H b ∀ g ∈ b H c a G c ⁡ g a b comp ⁡ D c f = b G c ⁡ g F ⁡ a F ⁡ b comp ⁡ E F ⁡ c a G b ⁡ f ↔ G = K ∧ ∀ a ∈ B a G a ⁡ Id ⁡ D ⁡ a = Id ⁡ E ⁡ F ⁡ a ∧ ∀ b ∈ B ∀ c ∈ B ∀ f ∈ a H b ∀ g ∈ b H c a G c ⁡ g a b comp ⁡ D c f = b G c ⁡ g F ⁡ a F ⁡ b comp ⁡ E F ⁡ c a G b ⁡ f
27 18 26 bitrd ⊢ φ → F D Func E G ↔ G = K ∧ ∀ a ∈ B a G a ⁡ Id ⁡ D ⁡ a = Id ⁡ E ⁡ F ⁡ a ∧ ∀ b ∈ B ∀ c ∈ B ∀ f ∈ a H b ∀ g ∈ b H c a G c ⁡ g a b comp ⁡ D c f = b G c ⁡ g F ⁡ a F ⁡ b comp ⁡ E F ⁡ c a G b ⁡ f
28 1 2 3 4 5 6 7 8 9 10 11 12 13 functhinclem4 ⊢ φ ∧ G = K → ∀ a ∈ B a G a ⁡ Id ⁡ D ⁡ a = Id ⁡ E ⁡ F ⁡ a ∧ ∀ b ∈ B ∀ c ∈ B ∀ f ∈ a H b ∀ g ∈ b H c a G c ⁡ g a b comp ⁡ D c f = b G c ⁡ g F ⁡ a F ⁡ b comp ⁡ E F ⁡ c a G b ⁡ f
29 27 28 mpbiran3d ⊢ φ → F D Func E G ↔ G = K