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

Theorem isfth 16888
Description: Value of the set of faithful functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.)
Hypothesis
Ref Expression
isfth.b 𝐵 = (Base‘𝐶)
Assertion
Ref Expression
isfth (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝐺𝑦)))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝐹,𝑦   𝑥,𝐺,𝑦

Proof of Theorem isfth
Dummy variables 𝑐 𝑑 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fthfunc 16881 . . 3 (𝐶 Faith 𝐷) ⊆ (𝐶 Func 𝐷)
21ssbri 4888 . 2 (𝐹(𝐶 Faith 𝐷)𝐺𝐹(𝐶 Func 𝐷)𝐺)
3 df-br 4844 . . . . . . 7 (𝐹(𝐶 Func 𝐷)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷))
4 funcrcl 16837 . . . . . . 7 (⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
53, 4sylbi 209 . . . . . 6 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
6 oveq12 6887 . . . . . . . . . 10 ((𝑐 = 𝐶𝑑 = 𝐷) → (𝑐 Func 𝑑) = (𝐶 Func 𝐷))
76breqd 4854 . . . . . . . . 9 ((𝑐 = 𝐶𝑑 = 𝐷) → (𝑓(𝑐 Func 𝑑)𝑔𝑓(𝐶 Func 𝐷)𝑔))
8 simpl 475 . . . . . . . . . . . 12 ((𝑐 = 𝐶𝑑 = 𝐷) → 𝑐 = 𝐶)
98fveq2d 6415 . . . . . . . . . . 11 ((𝑐 = 𝐶𝑑 = 𝐷) → (Base‘𝑐) = (Base‘𝐶))
10 isfth.b . . . . . . . . . . 11 𝐵 = (Base‘𝐶)
119, 10syl6eqr 2851 . . . . . . . . . 10 ((𝑐 = 𝐶𝑑 = 𝐷) → (Base‘𝑐) = 𝐵)
1211raleqdv 3327 . . . . . . . . . 10 ((𝑐 = 𝐶𝑑 = 𝐷) → (∀𝑦 ∈ (Base‘𝑐)Fun (𝑥𝑔𝑦) ↔ ∀𝑦𝐵 Fun (𝑥𝑔𝑦)))
1311, 12raleqbidv 3335 . . . . . . . . 9 ((𝑐 = 𝐶𝑑 = 𝐷) → (∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)Fun (𝑥𝑔𝑦) ↔ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦)))
147, 13anbi12d 625 . . . . . . . 8 ((𝑐 = 𝐶𝑑 = 𝐷) → ((𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)Fun (𝑥𝑔𝑦)) ↔ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦))))
1514opabbidv 4909 . . . . . . 7 ((𝑐 = 𝐶𝑑 = 𝐷) → {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)Fun (𝑥𝑔𝑦))} = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦))})
16 df-fth 16879 . . . . . . 7 Faith = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)Fun (𝑥𝑔𝑦))})
17 ovex 6910 . . . . . . . 8 (𝐶 Func 𝐷) ∈ V
18 simpl 475 . . . . . . . . . 10 ((𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦)) → 𝑓(𝐶 Func 𝐷)𝑔)
1918ssopab2i 5199 . . . . . . . . 9 {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦))} ⊆ {⟨𝑓, 𝑔⟩ ∣ 𝑓(𝐶 Func 𝐷)𝑔}
20 opabss 4907 . . . . . . . . 9 {⟨𝑓, 𝑔⟩ ∣ 𝑓(𝐶 Func 𝐷)𝑔} ⊆ (𝐶 Func 𝐷)
2119, 20sstri 3807 . . . . . . . 8 {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦))} ⊆ (𝐶 Func 𝐷)
2217, 21ssexi 4998 . . . . . . 7 {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦))} ∈ V
2315, 16, 22ovmpt2a 7025 . . . . . 6 ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Faith 𝐷) = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦))})
245, 23syl 17 . . . . 5 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 Faith 𝐷) = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦))})
2524breqd 4854 . . . 4 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Faith 𝐷)𝐺𝐹{⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦))}𝐺))
26 relfunc 16836 . . . . . 6 Rel (𝐶 Func 𝐷)
2726brrelex12i 5362 . . . . 5 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹 ∈ V ∧ 𝐺 ∈ V))
28 breq12 4848 . . . . . . 7 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓(𝐶 Func 𝐷)𝑔𝐹(𝐶 Func 𝐷)𝐺))
29 simpr 478 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → 𝑔 = 𝐺)
3029oveqd 6895 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
3130cnveqd 5501 . . . . . . . . 9 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
3231funeqd 6123 . . . . . . . 8 ((𝑓 = 𝐹𝑔 = 𝐺) → (Fun (𝑥𝑔𝑦) ↔ Fun (𝑥𝐺𝑦)))
33322ralbidv 3170 . . . . . . 7 ((𝑓 = 𝐹𝑔 = 𝐺) → (∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦) ↔ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝐺𝑦)))
3428, 33anbi12d 625 . . . . . 6 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦)) ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝐺𝑦))))
35 eqid 2799 . . . . . 6 {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦))} = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦))}
3634, 35brabga 5185 . . . . 5 ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹{⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦))}𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝐺𝑦))))
3727, 36syl 17 . . . 4 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹{⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝑔𝑦))}𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝐺𝑦))))
3825, 37bitrd 271 . . 3 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝐺𝑦))))
3938bianabs 538 . 2 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Faith 𝐷)𝐺 ↔ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝐺𝑦)))
402, 39biadan2 854 1 (𝐹(𝐶 Faith 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 Fun (𝑥𝐺𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 385   = wceq 1653  wcel 2157  wral 3089  Vcvv 3385  cop 4374   class class class wbr 4843  {copab 4905  ccnv 5311  Fun wfun 6095  cfv 6101  (class class class)co 6878  Basecbs 16184  Catccat 16639   Func cfunc 16828   Faith cfth 16877
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5097  ax-un 7183
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-iun 4712  df-br 4844  df-opab 4906  df-mpt 4923  df-id 5220  df-xp 5318  df-rel 5319  df-cnv 5320  df-co 5321  df-dm 5322  df-rn 5323  df-res 5324  df-ima 5325  df-iota 6064  df-fun 6103  df-fv 6109  df-ov 6881  df-oprab 6882  df-mpt2 6883  df-1st 7401  df-2nd 7402  df-func 16832  df-fth 16879
This theorem is referenced by:  isfth2  16889  fthpropd  16895  fthoppc  16897  fthres2b  16904  fthres2c  16905  fthres2  16906
  Copyright terms: Public domain W3C validator