Theorem fullfunc 17807

Description: A full functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017.)

Assertion

Ref	Expression
fullfunc	⊢ (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷)

Proof of Theorem fullfunc

Dummy variables 𝑐 𝑑 𝑓 𝑔 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 7348	. . . 4 ⊢ (𝑐 = 𝐶 → (𝑐 Full 𝑑) = (𝐶 Full 𝑑))
2		oveq1 7348	. . . 4 ⊢ (𝑐 = 𝐶 → (𝑐 Func 𝑑) = (𝐶 Func 𝑑))
3	1, 2	sseq12d 3966	. . 3 ⊢ (𝑐 = 𝐶 → ((𝑐 Full 𝑑) ⊆ (𝑐 Func 𝑑) ↔ (𝐶 Full 𝑑) ⊆ (𝐶 Func 𝑑)))
4		oveq2 7349	. . . 4 ⊢ (𝑑 = 𝐷 → (𝐶 Full 𝑑) = (𝐶 Full 𝐷))
5		oveq2 7349	. . . 4 ⊢ (𝑑 = 𝐷 → (𝐶 Func 𝑑) = (𝐶 Func 𝐷))
6	4, 5	sseq12d 3966	. . 3 ⊢ (𝑑 = 𝐷 → ((𝐶 Full 𝑑) ⊆ (𝐶 Func 𝑑) ↔ (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷)))
7		ovex 7374	. . . . . 6 ⊢ (𝑐 Func 𝑑) ∈ V
8		simpl 482	. . . . . . . 8 ⊢ ((𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦))) → 𝑓(𝑐 Func 𝑑)𝑔)
9	8	ssopab2i 5488	. . . . . . 7 ⊢ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))} ⊆ {⟨𝑓, 𝑔⟩ ∣ 𝑓(𝑐 Func 𝑑)𝑔}
10		opabss 5153	. . . . . . 7 ⊢ {⟨𝑓, 𝑔⟩ ∣ 𝑓(𝑐 Func 𝑑)𝑔} ⊆ (𝑐 Func 𝑑)
11	9, 10	sstri 3942	. . . . . 6 ⊢ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))} ⊆ (𝑐 Func 𝑑)
12	7, 11	ssexi 5258	. . . . 5 ⊢ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))} ∈ V
13		df-full 17805	. . . . . 6 ⊢ Full = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))})
14	13	ovmpt4g 7488	. . . . 5 ⊢ ((𝑐 ∈ Cat ∧ 𝑑 ∈ Cat ∧ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))} ∈ V) → (𝑐 Full 𝑑) = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))})
15	12, 14	mp3an3 1452	. . . 4 ⊢ ((𝑐 ∈ Cat ∧ 𝑑 ∈ Cat) → (𝑐 Full 𝑑) = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))})
16	15, 11	eqsstrdi 3977	. . 3 ⊢ ((𝑐 ∈ Cat ∧ 𝑑 ∈ Cat) → (𝑐 Full 𝑑) ⊆ (𝑐 Func 𝑑))
17	3, 6, 16	vtocl2ga 3531	. 2 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷))
18	13	mpondm0 7581	. . 3 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Full 𝐷) = ∅)
19		0ss 4348	. . 3 ⊢ ∅ ⊆ (𝐶 Func 𝐷)
20	18, 19	eqsstrdi 3977	. 2 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷))
21	17, 20	pm2.61i 182	1 ⊢ (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷)

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1541   ∈ wcel 2110  ∀wral 3045  Vcvv 3434   ⊆ wss 3900  ∅c0 4281   class class class wbr 5089  {copab 5151  ran crn 5615  ‘cfv 6477  (class class class)co 7341  Basecbs 17112  Hom chom 17164  Catccat 17562   Func cfunc 17753   Full cful 17803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-iota 6433  df-fun 6479  df-fv 6485  df-ov 7344  df-oprab 7345  df-mpo 7346  df-full 17805

This theorem is referenced by:  relfull  17809  isfull  17811  fulloppc  17823  cofull  17835  catcisolem  18009  catciso  18010  imasubc  49162  imasubc2  49163  idfullsubc  49172  fulloppf  49174  uptrlem1  49221  uptrlem2  49222  uptrlem3  49223  uptra  49226  uptrar  49227  uobeqw  49230  uobeq  49231  uptr2  49232  uptr2a  49233  fucoppcfunc  49423  fullthinc2  49462  thincciso  49464  fulltermc2  49523  termfucterm  49555  uobeqterm  49557