Theorem fullfunc 17913

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 7388	. . . 4 ⊢ (𝑐 = 𝐶 → (𝑐 Full 𝑑) = (𝐶 Full 𝑑))
2		oveq1 7388	. . . 4 ⊢ (𝑐 = 𝐶 → (𝑐 Func 𝑑) = (𝐶 Func 𝑑))
3	1, 2	sseq12d 3960	. . 3 ⊢ (𝑐 = 𝐶 → ((𝑐 Full 𝑑) ⊆ (𝑐 Func 𝑑) ↔ (𝐶 Full 𝑑) ⊆ (𝐶 Func 𝑑)))
4		oveq2 7389	. . . 4 ⊢ (𝑑 = 𝐷 → (𝐶 Full 𝑑) = (𝐶 Full 𝐷))
5		oveq2 7389	. . . 4 ⊢ (𝑑 = 𝐷 → (𝐶 Func 𝑑) = (𝐶 Func 𝐷))
6	4, 5	sseq12d 3960	. . 3 ⊢ (𝑑 = 𝐷 → ((𝐶 Full 𝑑) ⊆ (𝐶 Func 𝑑) ↔ (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷)))
7		ovex 7414	. . . . . 6 ⊢ (𝑐 Func 𝑑) ∈ V
8		simpl 485	. . . . . . . 8 ⊢ ((𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦))) → 𝑓(𝑐 Func 𝑑)𝑔)
9	8	ssopab2i 5510	. . . . . . 7 ⊢ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))} ⊆ {⟨𝑓, 𝑔⟩ ∣ 𝑓(𝑐 Func 𝑑)𝑔}
10		opabss 5154	. . . . . . 7 ⊢ {⟨𝑓, 𝑔⟩ ∣ 𝑓(𝑐 Func 𝑑)𝑔} ⊆ (𝑐 Func 𝑑)
11	9, 10	sstri 3936	. . . . . 6 ⊢ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))} ⊆ (𝑐 Func 𝑑)
12	7, 11	ssexi 5268	. . . . 5 ⊢ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))} ∈ V
13		df-full 17911	. . . . . 6 ⊢ Full = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))})
14	13	ovmpt4g 7528	. . . . 5 ⊢ ((𝑐 ∈ Cat ∧ 𝑑 ∈ Cat ∧ {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))} ∈ V) → (𝑐 Full 𝑑) = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))})
15	12, 14	mp3an3 1461	. . . 4 ⊢ ((𝑐 ∈ Cat ∧ 𝑑 ∈ Cat) → (𝑐 Full 𝑑) = {⟨𝑓, 𝑔⟩ ∣ (𝑓(𝑐 Func 𝑑)𝑔 ∧ ∀𝑥 ∈ (Base‘𝑐)∀𝑦 ∈ (Base‘𝑐)ran (𝑥𝑔𝑦) = ((𝑓‘𝑥)(Hom ‘𝑑)(𝑓‘𝑦)))})
16	15, 11	eqsstrdi 3971	. . 3 ⊢ ((𝑐 ∈ Cat ∧ 𝑑 ∈ Cat) → (𝑐 Full 𝑑) ⊆ (𝑐 Func 𝑑))
17	3, 6, 16	vtocl2ga 3533	. 2 ⊢ ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷))
18	13	mpondm0 7621	. . 3 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Full 𝐷) = ∅)
19		0ss 4344	. . 3 ⊢ ∅ ⊆ (𝐶 Func 𝐷)
20	18, 19	eqsstrdi 3971	. 2 ⊢ (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷))
21	17, 20	pm2.61i 183	1 ⊢ (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷)

Syntax hints:  ¬ wn 3   ∧ wa 398   = wceq 1550   ∈ wcel 2132  ∀wral 3066  Vcvv 3444   ⊆ wss 3895  ∅c0 4276   class class class wbr 5090  {copab 5152  ran crn 5637  ‘cfv 6506  (class class class)co 7381  Basecbs 17217  Hom chom 17269  Catccat 17668   Func cfunc 17859   Full cful 17909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pr 5380

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-iota 6462  df-fun 6508  df-fv 6514  df-ov 7384  df-oprab 7385  df-mpo 7386  df-full 17911

This theorem is referenced by:  relfull  17915  isfull  17917  fulloppc  17929  cofull  17941  catcisolem  18115  catciso  18116  imasubc  49710  imasubc2  49711  idfullsubc  49720  fulloppf  49722  uptrlem1  49769  uptrlem2  49770  uptrlem3  49771  uptra  49774  uptrar  49775  uobeqw  49778  uobeq  49779  uptr2  49780  uptr2a  49781  fucoppcfunc  49971  fullthinc2  50010  thincciso  50012  fulltermc2  50071  termfucterm  50103  uobeqterm  50105