MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fthpropd Structured version   Visualization version   GIF version

Theorem fthpropd 17043
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.)
Hypotheses
Ref Expression
fullpropd.1 (𝜑 → (Homf𝐴) = (Homf𝐵))
fullpropd.2 (𝜑 → (compf𝐴) = (compf𝐵))
fullpropd.3 (𝜑 → (Homf𝐶) = (Homf𝐷))
fullpropd.4 (𝜑 → (compf𝐶) = (compf𝐷))
fullpropd.a (𝜑𝐴𝑉)
fullpropd.b (𝜑𝐵𝑉)
fullpropd.c (𝜑𝐶𝑉)
fullpropd.d (𝜑𝐷𝑉)
Assertion
Ref Expression
fthpropd (𝜑 → (𝐴 Faith 𝐶) = (𝐵 Faith 𝐷))

Proof of Theorem fthpropd
Dummy variables 𝑓 𝑔 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relfth 17031 . 2 Rel (𝐴 Faith 𝐶)
2 relfth 17031 . 2 Rel (𝐵 Faith 𝐷)
3 fullpropd.1 . . . . . 6 (𝜑 → (Homf𝐴) = (Homf𝐵))
4 fullpropd.2 . . . . . 6 (𝜑 → (compf𝐴) = (compf𝐵))
5 fullpropd.3 . . . . . 6 (𝜑 → (Homf𝐶) = (Homf𝐷))
6 fullpropd.4 . . . . . 6 (𝜑 → (compf𝐶) = (compf𝐷))
7 fullpropd.a . . . . . 6 (𝜑𝐴𝑉)
8 fullpropd.b . . . . . 6 (𝜑𝐵𝑉)
9 fullpropd.c . . . . . 6 (𝜑𝐶𝑉)
10 fullpropd.d . . . . . 6 (𝜑𝐷𝑉)
113, 4, 5, 6, 7, 8, 9, 10funcpropd 17022 . . . . 5 (𝜑 → (𝐴 Func 𝐶) = (𝐵 Func 𝐷))
1211breqd 4934 . . . 4 (𝜑 → (𝑓(𝐴 Func 𝐶)𝑔𝑓(𝐵 Func 𝐷)𝑔))
133homfeqbas 16818 . . . . 5 (𝜑 → (Base‘𝐴) = (Base‘𝐵))
1413raleqdv 3349 . . . . 5 (𝜑 → (∀𝑦 ∈ (Base‘𝐴)Fun (𝑥𝑔𝑦) ↔ ∀𝑦 ∈ (Base‘𝐵)Fun (𝑥𝑔𝑦)))
1513, 14raleqbidv 3335 . . . 4 (𝜑 → (∀𝑥 ∈ (Base‘𝐴)∀𝑦 ∈ (Base‘𝐴)Fun (𝑥𝑔𝑦) ↔ ∀𝑥 ∈ (Base‘𝐵)∀𝑦 ∈ (Base‘𝐵)Fun (𝑥𝑔𝑦)))
1612, 15anbi12d 621 . . 3 (𝜑 → ((𝑓(𝐴 Func 𝐶)𝑔 ∧ ∀𝑥 ∈ (Base‘𝐴)∀𝑦 ∈ (Base‘𝐴)Fun (𝑥𝑔𝑦)) ↔ (𝑓(𝐵 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ (Base‘𝐵)∀𝑦 ∈ (Base‘𝐵)Fun (𝑥𝑔𝑦))))
17 eqid 2772 . . . 4 (Base‘𝐴) = (Base‘𝐴)
1817isfth 17036 . . 3 (𝑓(𝐴 Faith 𝐶)𝑔 ↔ (𝑓(𝐴 Func 𝐶)𝑔 ∧ ∀𝑥 ∈ (Base‘𝐴)∀𝑦 ∈ (Base‘𝐴)Fun (𝑥𝑔𝑦)))
19 eqid 2772 . . . 4 (Base‘𝐵) = (Base‘𝐵)
2019isfth 17036 . . 3 (𝑓(𝐵 Faith 𝐷)𝑔 ↔ (𝑓(𝐵 Func 𝐷)𝑔 ∧ ∀𝑥 ∈ (Base‘𝐵)∀𝑦 ∈ (Base‘𝐵)Fun (𝑥𝑔𝑦)))
2116, 18, 203bitr4g 306 . 2 (𝜑 → (𝑓(𝐴 Faith 𝐶)𝑔𝑓(𝐵 Faith 𝐷)𝑔))
221, 2, 21eqbrrdiv 5511 1 (𝜑 → (𝐴 Faith 𝐶) = (𝐵 Faith 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387   = wceq 1507  wcel 2050  wral 3082   class class class wbr 4923  ccnv 5400  Fun wfun 6176  cfv 6182  (class class class)co 6970  Basecbs 16333  Homf chomf 16789  compfccomf 16790   Func cfunc 16976   Faith cfth 17025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-reu 3089  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5306  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-res 5413  df-ima 5414  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-1st 7495  df-2nd 7496  df-map 8202  df-ixp 8254  df-cat 16791  df-cid 16792  df-homf 16793  df-comf 16794  df-func 16980  df-fth 17027
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator