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

Theorem isfull 16763
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 16759 . . 3 (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷)
21ssbri 4841 . 2 (𝐹(𝐶 Full 𝐷)𝐺𝐹(𝐶 Func 𝐷)𝐺)
3 df-br 4797 . . . . . . 7 (𝐹(𝐶 Func 𝐷)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷))
4 funcrcl 16716 . . . . . . 7 (⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
53, 4sylbi 207 . . . . . 6 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
6 oveq12 6814 . . . . . . . . . 10 ((𝑐 = 𝐶𝑑 = 𝐷) → (𝑐 Func 𝑑) = (𝐶 Func 𝐷))
76breqd 4807 . . . . . . . . 9 ((𝑐 = 𝐶𝑑 = 𝐷) → (𝑓(𝑐 Func 𝑑)𝑔𝑓(𝐶 Func 𝐷)𝑔))
8 simpl 474 . . . . . . . . . . . 12 ((𝑐 = 𝐶𝑑 = 𝐷) → 𝑐 = 𝐶)
98fveq2d 6348 . . . . . . . . . . 11 ((𝑐 = 𝐶𝑑 = 𝐷) → (Base‘𝑐) = (Base‘𝐶))
10 isfull.b . . . . . . . . . . 11 𝐵 = (Base‘𝐶)
119, 10syl6eqr 2804 . . . . . . . . . 10 ((𝑐 = 𝐶𝑑 = 𝐷) → (Base‘𝑐) = 𝐵)
12 simpr 479 . . . . . . . . . . . . . . 15 ((𝑐 = 𝐶𝑑 = 𝐷) → 𝑑 = 𝐷)
1312fveq2d 6348 . . . . . . . . . . . . . 14 ((𝑐 = 𝐶𝑑 = 𝐷) → (Hom ‘𝑑) = (Hom ‘𝐷))
14 isfull.j . . . . . . . . . . . . . 14 𝐽 = (Hom ‘𝐷)
1513, 14syl6eqr 2804 . . . . . . . . . . . . 13 ((𝑐 = 𝐶𝑑 = 𝐷) → (Hom ‘𝑑) = 𝐽)
1615oveqd 6822 . . . . . . . . . . . 12 ((𝑐 = 𝐶𝑑 = 𝐷) → ((𝑓𝑥)(Hom ‘𝑑)(𝑓𝑦)) = ((𝑓𝑥)𝐽(𝑓𝑦)))
1716eqeq2d 2762 . . . . . . . . . . 11 ((𝑐 = 𝐶𝑑 = 𝐷) → (ran (𝑥𝑔𝑦) = ((𝑓𝑥)(Hom ‘𝑑)(𝑓𝑦)) ↔ ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦))))
1811, 17raleqbidv 3283 . . . . . . . . . 10 ((𝑐 = 𝐶𝑑 = 𝐷) → (∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓𝑥)(Hom ‘𝑑)(𝑓𝑦)) ↔ ∀𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦))))
1911, 18raleqbidv 3283 . . . . . . . . 9 ((𝑐 = 𝐶𝑑 = 𝐷) → (∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓𝑥)(Hom ‘𝑑)(𝑓𝑦)) ↔ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦))))
207, 19anbi12d 749 . . . . . . . 8 ((𝑐 = 𝐶𝑑 = 𝐷) → ((𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓𝑥)(Hom ‘𝑑)(𝑓𝑦))) ↔ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))))
2120opabbidv 4860 . . . . . . 7 ((𝑐 = 𝐶𝑑 = 𝐷) → {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓𝑥)(Hom ‘𝑑)(𝑓𝑦)))} = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))})
22 df-full 16757 . . . . . . 7 Full = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓𝑥)(Hom ‘𝑑)(𝑓𝑦)))})
23 ovex 6833 . . . . . . . 8 (𝐶 Func 𝐷) ∈ V
24 simpl 474 . . . . . . . . . 10 ((𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦))) → 𝑓(𝐶 Func 𝐷)𝑔)
2524ssopab2i 5145 . . . . . . . . 9 {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))} ⊆ {⟨𝑓, 𝑔⟩ ∣ 𝑓(𝐶 Func 𝐷)𝑔}
26 opabss 4858 . . . . . . . . 9 {⟨𝑓, 𝑔⟩ ∣ 𝑓(𝐶 Func 𝐷)𝑔} ⊆ (𝐶 Func 𝐷)
2725, 26sstri 3745 . . . . . . . 8 {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))} ⊆ (𝐶 Func 𝐷)
2823, 27ssexi 4947 . . . . . . 7 {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))} ∈ V
2921, 22, 28ovmpt2a 6948 . . . . . 6 ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Full 𝐷) = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))})
305, 29syl 17 . . . . 5 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐶 Full 𝐷) = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))})
3130breqd 4807 . . . 4 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Full 𝐷)𝐺𝐹{⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))}𝐺))
32 relfunc 16715 . . . . . 6 Rel (𝐶 Func 𝐷)
33 brrelex12 5304 . . . . . 6 ((Rel (𝐶 Func 𝐷) ∧ 𝐹(𝐶 Func 𝐷)𝐺) → (𝐹 ∈ V ∧ 𝐺 ∈ V))
3432, 33mpan 708 . . . . 5 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹 ∈ V ∧ 𝐺 ∈ V))
35 breq12 4801 . . . . . . 7 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓(𝐶 Func 𝐷)𝑔𝐹(𝐶 Func 𝐷)𝐺))
36 simpr 479 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → 𝑔 = 𝐺)
3736oveqd 6822 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
3837rneqd 5500 . . . . . . . . 9 ((𝑓 = 𝐹𝑔 = 𝐺) → ran (𝑥𝑔𝑦) = ran (𝑥𝐺𝑦))
39 simpl 474 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → 𝑓 = 𝐹)
4039fveq1d 6346 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓𝑥) = (𝐹𝑥))
4139fveq1d 6346 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓𝑦) = (𝐹𝑦))
4240, 41oveq12d 6823 . . . . . . . . 9 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑓𝑥)𝐽(𝑓𝑦)) = ((𝐹𝑥)𝐽(𝐹𝑦)))
4338, 42eqeq12d 2767 . . . . . . . 8 ((𝑓 = 𝐹𝑔 = 𝐺) → (ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)) ↔ ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦))))
44432ralbidv 3119 . . . . . . 7 ((𝑓 = 𝐹𝑔 = 𝐺) → (∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)) ↔ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦))))
4535, 44anbi12d 749 . . . . . 6 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦))) ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦)))))
46 eqid 2752 . . . . . 6 {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))} = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))}
4745, 46brabga 5131 . . . . 5 ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹{⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))}𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦)))))
4834, 47syl 17 . . . 4 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹{⟨𝑓, 𝑔⟩ ∣ (𝑓(𝐶 Func 𝐷)𝑔 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝑔𝑦) = ((𝑓𝑥)𝐽(𝑓𝑦)))}𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦)))))
4931, 48bitrd 268 . . 3 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦)))))
5049bianabs 960 . 2 (𝐹(𝐶 Func 𝐷)𝐺 → (𝐹(𝐶 Full 𝐷)𝐺 ↔ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦))))
512, 50biadan2 677 1 (𝐹(𝐶 Full 𝐷)𝐺 ↔ (𝐹(𝐶 Func 𝐷)𝐺 ∧ ∀𝑥𝐵𝑦𝐵 ran (𝑥𝐺𝑦) = ((𝐹𝑥)𝐽(𝐹𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1624  wcel 2131  wral 3042  Vcvv 3332  cop 4319   class class class wbr 4796  {copab 4856  ran crn 5259  Rel wrel 5263  cfv 6041  (class class class)co 6805  Basecbs 16051  Hom chom 16146  Catccat 16518   Func cfunc 16707   Full cful 16755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-iota 6004  df-fun 6043  df-fv 6049  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-1st 7325  df-2nd 7326  df-func 16711  df-full 16757
This theorem is referenced by:  isfull2  16764  fullpropd  16773  fulloppc  16775  fullres2c  16792
  Copyright terms: Public domain W3C validator