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

Metamath Proof Explorer

Theorem fthpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same faithful functors. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fullpropd.1 ⊢ φ → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B
fullpropd.2 ⊢ φ → comp 𝑓 ⁡ A = comp 𝑓 ⁡ B
fullpropd.3 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
fullpropd.4 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
fullpropd.a ⊢ φ → A ∈ V
fullpropd.b ⊢ φ → B ∈ V
fullpropd.c ⊢ φ → C ∈ V
fullpropd.d ⊢ φ → D ∈ V
Assertion fthpropd ⊢ φ → A Faith C = B Faith D

Proof

Step Hyp Ref Expression
1 fullpropd.1 ⊢ φ → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B
2 fullpropd.2 ⊢ φ → comp 𝑓 ⁡ A = comp 𝑓 ⁡ B
3 fullpropd.3 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
4 fullpropd.4 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
5 fullpropd.a ⊢ φ → A ∈ V
6 fullpropd.b ⊢ φ → B ∈ V
7 fullpropd.c ⊢ φ → C ∈ V
8 fullpropd.d ⊢ φ → D ∈ V
9 relfth ⊢ Rel ⁡ A Faith C
10 relfth ⊢ Rel ⁡ B Faith D
11 1 2 3 4 5 6 7 8 funcpropd ⊢ φ → A Func C = B Func D
12 11 breqd ⊢ φ → f A Func C g ↔ f B Func D g
13 1 homfeqbas ⊢ φ → Base A = Base B
14 13 raleqdv ⊢ φ → ∀ y ∈ Base A Fun ⁡ x g y -1 ↔ ∀ y ∈ Base B Fun ⁡ x g y -1
15 13 14 raleqbidv ⊢ φ → ∀ x ∈ Base A ∀ y ∈ Base A Fun ⁡ x g y -1 ↔ ∀ x ∈ Base B ∀ y ∈ Base B Fun ⁡ x g y -1
16 12 15 anbi12d ⊢ φ → f A Func C g ∧ ∀ x ∈ Base A ∀ y ∈ Base A Fun ⁡ x g y -1 ↔ f B Func D g ∧ ∀ x ∈ Base B ∀ y ∈ Base B Fun ⁡ x g y -1
17 eqid ⊢ Base A = Base A
18 17 isfth ⊢ f A Faith C g ↔ f A Func C g ∧ ∀ x ∈ Base A ∀ y ∈ Base A Fun ⁡ x g y -1
19 eqid ⊢ Base B = Base B
20 19 isfth ⊢ f B Faith D g ↔ f B Func D g ∧ ∀ x ∈ Base B ∀ y ∈ Base B Fun ⁡ x g y -1
21 16 18 20 3bitr4g ⊢ φ → f A Faith C g ↔ f B Faith D g
22 9 10 21 eqbrrdiv ⊢ φ → A Faith C = B Faith D