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

Theorem isfull 16955
Description: Value of the set of full functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.)
Hypotheses
Ref Expression
isfull.b 𝐵 = (Base‘𝐶)
isfull.j 𝐽 = (Hom ‘𝐷)
Assertion
Ref Expression
isfull (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦))))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝐽,𝑦   𝑥,𝐹,𝑦   𝑥,𝐺,𝑦

Proof of Theorem isfull
Dummy variables 𝑐 𝑑 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fullfunc 16951 . . 3 (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷)
21ssbri 4931 . 2 (𝐹(𝐶 Full 𝐷)𝐺𝐹(𝐶 Func 𝐷)𝐺)
3 df-br 4887 . . . . . . 7 (𝐹(𝐶 Func 𝐷)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷))
4 funcrcl 16908 . . . . . . 7 (⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
53, 4sylbi 209 . . . . . 6 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
6 oveq12 6931 . . . . . . . . . 10 ((𝑐 = 𝐶𝑑 = 𝐷) → (𝑐 Func 𝑑) = (𝐶 Func 𝐷))
76breqd 4897 . . . . . . . . 9 ((𝑐 = 𝐶𝑑 = 𝐷) → (𝑓(𝑐 Func 𝑑)𝑔𝑓(𝐶 Func 𝐷)𝑔))
8 simpl 476 . . . . . . . . . . . 12 ((𝑐 = 𝐶𝑑 = 𝐷) → 𝑐 = 𝐶)
98fveq2d 6450 . . . . . . . . . . 11 ((𝑐 = 𝐶𝑑 = 𝐷) → (Base‘𝑐) = (Base‘𝐶))
10 isfull.b . . . . . . . . . . 11 𝐵 = (Base‘𝐶)
119, 10syl6eqr 2831 . . . . . . . . . 10 ((𝑐 = 𝐶𝑑 = 𝐷) → (Base‘𝑐) = 𝐵)
12 simpr 479 . . . . . . . . . . . . . . 15 ((𝑐 = 𝐶𝑑 = 𝐷) → 𝑑 = 𝐷)
1312fveq2d 6450 . . . . . . . . . . . . . 14 ((𝑐 = 𝐶𝑑 = 𝐷) → (Hom ‘𝑑) = (Hom ‘𝐷))
14 isfull.j . . . . . . . . . . . . . 14 𝐽 = (Hom ‘𝐷)
1513, 14syl6eqr 2831 . . . . . . . . . . . . 13 ((𝑐 = 𝐶𝑑 = 𝐷) → (Hom ‘𝑑) = 𝐽)
1615oveqd 6939 . . . . . . . . . . . 12 ((𝑐 = 𝐶𝑑 = 𝐷) → ((𝑓𝑥)(Hom ‘𝑑)(𝑓𝑦)) = ((𝑓𝑥)𝐽(𝑓𝑦)))
1716eqeq2d 2787 . . . . . . . . . . 11 ((𝑐 = 𝐶𝑑 = 𝐷) → (ran (𝑥𝑔𝑦) = ((𝑓𝑥)(Hom ‘𝑑)(𝑓𝑦)) ↔ ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦))))
1811, 17raleqbidv 3325 . . . . . . . . . 10 ((𝑐 = 𝐶𝑑 = 𝐷) → (∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓𝑥)(Hom ‘𝑑)(𝑓𝑦)) ↔ ∀𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦))))
1911, 18raleqbidv 3325 . . . . . . . . 9 ((𝑐 = 𝐶𝑑 = 𝐷) → (∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓𝑥)(Hom ‘𝑑)(𝑓𝑦)) ↔ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦))))
207, 19anbi12d 624 . . . . . . . 8 ((𝑐 = 𝐶𝑑 = 𝐷) → ((𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓𝑥)(Hom ‘𝑑)(𝑓𝑦))) ↔ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))))
2120opabbidv 4952 . . . . . . 7 ((𝑐 = 𝐶𝑑 = 𝐷) → {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓𝑥)(Hom ‘𝑑)(𝑓𝑦)))} = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))})
22 df-full 16949 . . . . . . 7 Full = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓𝑥)(Hom ‘𝑑)(𝑓𝑦)))})
23 ovex 6954 . . . . . . . 8 (𝐶 Func 𝐷) ∈ V
24 simpl 476 . . . . . . . . . 10 ((𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦))) → 𝑓(𝐶 Func 𝐷)𝑔)
2524ssopab2i 5240 . . . . . . . . 9 {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))} ⊆ {⟨𝑓, 𝑔⟩ ∣ 𝑓(𝐶 Func 𝐷)𝑔}
26 opabss 4950 . . . . . . . . 9 {⟨𝑓, 𝑔⟩ ∣ 𝑓(𝐶 Func 𝐷)𝑔} ⊆ (𝐶 Func 𝐷)
2725, 26sstri 3829 . . . . . . . 8 {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))} ⊆ (𝐶 Func 𝐷)
2823, 27ssexi 5040 . . . . . . 7 {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))} ∈ V
2921, 22, 28ovmpt2a 7068 . . . . . 6 ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Full 𝐷) = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))})
305, 29syl 17 . . . . 5 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 Full 𝐷) = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))})
3130breqd 4897 . . . 4 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Full 𝐷)𝐺𝐹{⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))}𝐺))
32 relfunc 16907 . . . . . 6 Rel (𝐶 Func 𝐷)
3332brrelex12i 5405 . . . . 5 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹 ∈ V ∧ 𝐺 ∈ V))
34 breq12 4891 . . . . . . 7 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓(𝐶 Func 𝐷)𝑔𝐹(𝐶 Func 𝐷)𝐺))
35 simpr 479 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → 𝑔 = 𝐺)
3635oveqd 6939 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
3736rneqd 5598 . . . . . . . . 9 ((𝑓 = 𝐹𝑔 = 𝐺) → ran (𝑥𝑔𝑦) = ran (𝑥𝐺𝑦))
38 simpl 476 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → 𝑓 = 𝐹)
3938fveq1d 6448 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓𝑥) = (𝐹𝑥))
4038fveq1d 6448 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓𝑦) = (𝐹𝑦))
4139, 40oveq12d 6940 . . . . . . . . 9 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑓𝑥)𝐽(𝑓𝑦)) = ((𝐹𝑥)𝐽(𝐹𝑦)))
4237, 41eqeq12d 2792 . . . . . . . 8 ((𝑓 = 𝐹𝑔 = 𝐺) → (ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)) ↔ ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦))))
43422ralbidv 3170 . . . . . . 7 ((𝑓 = 𝐹𝑔 = 𝐺) → (∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)) ↔ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦))))
4434, 43anbi12d 624 . . . . . 6 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦))) ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦)))))
45 eqid 2777 . . . . . 6 {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))} = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))}
4644, 45brabga 5226 . . . . 5 ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹{⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))}𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦)))))
4733, 46syl 17 . . . 4 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹{⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))}𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦)))))
4831, 47bitrd 271 . . 3 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦)))))
4948bianabs 537 . 2 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Full 𝐷)𝐺 ↔ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦))))
502, 49biadanii 813 1 (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 386   = wceq 1601  wcel 2106  wral 3089  Vcvv 3397  cop 4403   class class class wbr 4886  {copab 4948  ran crn 5356  cfv 6135  (class class class)co 6922  Basecbs 16255  Hom chom 16349  Catccat 16710   Func cfunc 16899   Full cful 16947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fv 6143  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-1st 7445  df-2nd 7446  df-func 16903  df-full 16949
This theorem is referenced by:  isfull2  16956  fullpropd  16965  fulloppc  16967  fullres2c  16984
  Copyright terms: Public domain W3C validator