Metamath Proof Explorer

Theorem fthcomf

Description: Source categories of a faithful functor have the same base, hom-sets and composition operation if the composition is compatible in images of the functor. (Contributed by Zhi Wang, 10-Nov-2025)

Ref Expression
Hypotheses fthcomf.1 ⊢ φ → F A Faith C G
fthcomf.2 ⊢ φ → F B Func D G
fthcomf.3 ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → y G z ⁡ g F ⁡ x F ⁡ y comp ⁡ C F ⁡ z x G y ⁡ f = y G z ⁡ g F ⁡ x F ⁡ y comp ⁡ D F ⁡ z x G y ⁡ f
Assertion fthcomf ⊢ φ → comp 𝑓 ⁡ A = comp 𝑓 ⁡ B

Proof

Step Hyp Ref Expression
1 fthcomf.1 ⊢ φ → F A Faith C G
2 fthcomf.2 ⊢ φ → F B Func D G
3 fthcomf.3 ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → y G z ⁡ g F ⁡ x F ⁡ y comp ⁡ C F ⁡ z x G y ⁡ f = y G z ⁡ g F ⁡ x F ⁡ y comp ⁡ D F ⁡ z x G y ⁡ f
4 eqid ⊢ Base A = Base A
5 eqid ⊢ Hom ⁡ A = Hom ⁡ A
6 eqid ⊢ comp ⁡ A = comp ⁡ A
7 eqid ⊢ comp ⁡ C = comp ⁡ C
8 1 ad2antrr ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → F A Faith C G
9 fthfunc ⊢ A Faith C ⊆ A Func C
10 9 ssbri ⊢ F A Faith C G → F A Func C G
11 8 10 syl ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → F A Func C G
12 simplr1 ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → x ∈ Base A
13 simplr2 ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → y ∈ Base A
14 simplr3 ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → z ∈ Base A
15 simprl ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → f ∈ x Hom ⁡ A y
16 simprr ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → g ∈ y Hom ⁡ A z
17 4 5 6 7 11 12 13 14 15 16 funcco ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → x G z ⁡ g x y comp ⁡ A z f = y G z ⁡ g F ⁡ x F ⁡ y comp ⁡ C F ⁡ z x G y ⁡ f
18 eqid ⊢ Base B = Base B
19 eqid ⊢ Hom ⁡ B = Hom ⁡ B
20 eqid ⊢ comp ⁡ B = comp ⁡ B
21 eqid ⊢ comp ⁡ D = comp ⁡ D
22 2 ad2antrr ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → F B Func D G
23 1 10 syl ⊢ φ → F A Func C G
24 23 2 funchomf ⊢ φ → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B
25 24 homfeqbas ⊢ φ → Base A = Base B
26 25 ad2antrr ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → Base A = Base B
27 12 26 eleqtrd ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → x ∈ Base B
28 13 26 eleqtrd ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → y ∈ Base B
29 14 26 eleqtrd ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → z ∈ Base B
30 24 ad2antrr ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B
31 4 5 19 30 12 13 homfeqval ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → x Hom ⁡ A y = x Hom ⁡ B y
32 15 31 eleqtrd ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → f ∈ x Hom ⁡ B y
33 4 5 19 30 13 14 homfeqval ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → y Hom ⁡ A z = y Hom ⁡ B z
34 16 33 eleqtrd ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → g ∈ y Hom ⁡ B z
35 18 19 20 21 22 27 28 29 32 34 funcco ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → x G z ⁡ g x y comp ⁡ B z f = y G z ⁡ g F ⁡ x F ⁡ y comp ⁡ D F ⁡ z x G y ⁡ f
36 3 17 35 3eqtr4d ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → x G z ⁡ g x y comp ⁡ A z f = x G z ⁡ g x y comp ⁡ B z f
37 eqid ⊢ Hom ⁡ C = Hom ⁡ C
38 23 funcrcl2 ⊢ φ → A ∈ Cat
39 38 ad2antrr ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → A ∈ Cat
40 4 5 6 39 12 13 14 15 16 catcocl ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → g x y comp ⁡ A z f ∈ x Hom ⁡ A z
41 2 funcrcl2 ⊢ φ → B ∈ Cat
42 41 ad2antrr ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → B ∈ Cat
43 18 19 20 42 27 28 29 32 34 catcocl ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → g x y comp ⁡ B z f ∈ x Hom ⁡ B z
44 4 5 19 30 12 14 homfeqval ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → x Hom ⁡ A z = x Hom ⁡ B z
45 43 44 eleqtrrd ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → g x y comp ⁡ B z f ∈ x Hom ⁡ A z
46 4 5 37 8 12 14 40 45 fthi ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → x G z ⁡ g x y comp ⁡ A z f = x G z ⁡ g x y comp ⁡ B z f ↔ g x y comp ⁡ A z f = g x y comp ⁡ B z f
47 36 46 mpbid ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A ∧ f ∈ x Hom ⁡ A y ∧ g ∈ y Hom ⁡ A z → g x y comp ⁡ A z f = g x y comp ⁡ B z f
48 47 ralrimivva ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A ∧ z ∈ Base A → ∀ f ∈ x Hom ⁡ A y ∀ g ∈ y Hom ⁡ A z g x y comp ⁡ A z f = g x y comp ⁡ B z f
49 48 ralrimivvva ⊢ φ → ∀ x ∈ Base A ∀ y ∈ Base A ∀ z ∈ Base A ∀ f ∈ x Hom ⁡ A y ∀ g ∈ y Hom ⁡ A z g x y comp ⁡ A z f = g x y comp ⁡ B z f
50 eqidd ⊢ φ → Base A = Base A
51 6 20 5 50 25 24 comfeq ⊢ φ → comp 𝑓 ⁡ A = comp 𝑓 ⁡ B ↔ ∀ x ∈ Base A ∀ y ∈ Base A ∀ z ∈ Base A ∀ f ∈ x Hom ⁡ A y ∀ g ∈ y Hom ⁡ A z g x y comp ⁡ A z f = g x y comp ⁡ B z f
52 49 51 mpbird ⊢ φ → comp 𝑓 ⁡ A = comp 𝑓 ⁡ B