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

Theorem catsubcat 17207
Description: For any category 𝐶, 𝐶 itself is a (full) subcategory of 𝐶, see example 4.3(1.b) in [Adamek] p. 48. (Contributed by AV, 23-Apr-2020.)
Assertion
Ref Expression
catsubcat (𝐶 ∈ Cat → (Homf𝐶) ∈ (Subcat‘𝐶))

Proof of Theorem catsubcat
Dummy variables 𝑓 𝑔 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssidd 3898 . . 3 (𝐶 ∈ Cat → (Base‘𝐶) ⊆ (Base‘𝐶))
2 ssidd 3898 . . . 4 ((𝐶 ∈ Cat ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(Homf𝐶)𝑦) ⊆ (𝑥(Homf𝐶)𝑦))
32ralrimivva 3103 . . 3 (𝐶 ∈ Cat → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(Homf𝐶)𝑦) ⊆ (𝑥(Homf𝐶)𝑦))
4 eqid 2738 . . . . . 6 (Homf𝐶) = (Homf𝐶)
5 eqid 2738 . . . . . 6 (Base‘𝐶) = (Base‘𝐶)
64, 5homffn 17060 . . . . 5 (Homf𝐶) Fn ((Base‘𝐶) × (Base‘𝐶))
76a1i 11 . . . 4 (𝐶 ∈ Cat → (Homf𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)))
8 fvexd 6683 . . . 4 (𝐶 ∈ Cat → (Base‘𝐶) ∈ V)
97, 7, 8isssc 17188 . . 3 (𝐶 ∈ Cat → ((Homf𝐶) ⊆cat (Homf𝐶) ↔ ((Base‘𝐶) ⊆ (Base‘𝐶) ∧ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(Homf𝐶)𝑦) ⊆ (𝑥(Homf𝐶)𝑦))))
101, 3, 9mpbir2and 713 . 2 (𝐶 ∈ Cat → (Homf𝐶) ⊆cat (Homf𝐶))
11 eqid 2738 . . . . . 6 (Hom ‘𝐶) = (Hom ‘𝐶)
12 eqid 2738 . . . . . 6 (Id‘𝐶) = (Id‘𝐶)
13 simpl 486 . . . . . 6 ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
14 simpr 488 . . . . . 6 ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
155, 11, 12, 13, 14catidcl 17049 . . . . 5 ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
164, 5, 11, 14, 14homfval 17059 . . . . 5 ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑥(Homf𝐶)𝑥) = (𝑥(Hom ‘𝐶)𝑥))
1715, 16eleqtrrd 2836 . . . 4 ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Homf𝐶)𝑥))
18 eqid 2738 . . . . . . . 8 (comp‘𝐶) = (comp‘𝐶)
1913adantr 484 . . . . . . . . 9 (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
2019adantr 484 . . . . . . . 8 ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Homf𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Homf𝐶)𝑧))) → 𝐶 ∈ Cat)
2114adantr 484 . . . . . . . . 9 (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
2221adantr 484 . . . . . . . 8 ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Homf𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Homf𝐶)𝑧))) → 𝑥 ∈ (Base‘𝐶))
23 simpl 486 . . . . . . . . . 10 ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶))
2423adantl 485 . . . . . . . . 9 (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
2524adantr 484 . . . . . . . 8 ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Homf𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Homf𝐶)𝑧))) → 𝑦 ∈ (Base‘𝐶))
26 simpr 488 . . . . . . . . . 10 ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) → 𝑧 ∈ (Base‘𝐶))
2726adantl 485 . . . . . . . . 9 (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → 𝑧 ∈ (Base‘𝐶))
2827adantr 484 . . . . . . . 8 ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Homf𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Homf𝐶)𝑧))) → 𝑧 ∈ (Base‘𝐶))
294, 5, 11, 21, 24homfval 17059 . . . . . . . . . . . 12 (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (𝑥(Homf𝐶)𝑦) = (𝑥(Hom ‘𝐶)𝑦))
3029eleq2d 2818 . . . . . . . . . . 11 (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (𝑓 ∈ (𝑥(Homf𝐶)𝑦) ↔ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)))
3130biimpcd 252 . . . . . . . . . 10 (𝑓 ∈ (𝑥(Homf𝐶)𝑦) → (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)))
3231adantr 484 . . . . . . . . 9 ((𝑓 ∈ (𝑥(Homf𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Homf𝐶)𝑧)) → (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)))
3332impcom 411 . . . . . . . 8 ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Homf𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Homf𝐶)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
344, 5, 11, 24, 27homfval 17059 . . . . . . . . . . . 12 (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (𝑦(Homf𝐶)𝑧) = (𝑦(Hom ‘𝐶)𝑧))
3534eleq2d 2818 . . . . . . . . . . 11 (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (𝑔 ∈ (𝑦(Homf𝐶)𝑧) ↔ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))
3635biimpd 232 . . . . . . . . . 10 (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (𝑔 ∈ (𝑦(Homf𝐶)𝑧) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))
3736adantld 494 . . . . . . . . 9 (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ((𝑓 ∈ (𝑥(Homf𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Homf𝐶)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))
3837imp 410 . . . . . . . 8 ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Homf𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Homf𝐶)𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
395, 11, 18, 20, 22, 25, 28, 33, 38catcocl 17052 . . . . . . 7 ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Homf𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Homf𝐶)𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
404, 5, 11, 21, 27homfval 17059 . . . . . . . 8 (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → (𝑥(Homf𝐶)𝑧) = (𝑥(Hom ‘𝐶)𝑧))
4140adantr 484 . . . . . . 7 ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Homf𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Homf𝐶)𝑧))) → (𝑥(Homf𝐶)𝑧) = (𝑥(Hom ‘𝐶)𝑧))
4239, 41eleqtrrd 2836 . . . . . 6 ((((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Homf𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Homf𝐶)𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Homf𝐶)𝑧))
4342ralrimivva 3103 . . . . 5 (((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Homf𝐶)𝑦)∀𝑔 ∈ (𝑦(Homf𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Homf𝐶)𝑧))
4443ralrimivva 3103 . . . 4 ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Homf𝐶)𝑦)∀𝑔 ∈ (𝑦(Homf𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Homf𝐶)𝑧))
4517, 44jca 515 . . 3 ((𝐶 ∈ Cat ∧ 𝑥 ∈ (Base‘𝐶)) → (((Id‘𝐶)‘𝑥) ∈ (𝑥(Homf𝐶)𝑥) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Homf𝐶)𝑦)∀𝑔 ∈ (𝑦(Homf𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Homf𝐶)𝑧)))
4645ralrimiva 3096 . 2 (𝐶 ∈ Cat → ∀𝑥 ∈ (Base‘𝐶)(((Id‘𝐶)‘𝑥) ∈ (𝑥(Homf𝐶)𝑥) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Homf𝐶)𝑦)∀𝑔 ∈ (𝑦(Homf𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Homf𝐶)𝑧)))
47 id 22 . . 3 (𝐶 ∈ Cat → 𝐶 ∈ Cat)
484, 12, 18, 47, 7issubc2 17204 . 2 (𝐶 ∈ Cat → ((Homf𝐶) ∈ (Subcat‘𝐶) ↔ ((Homf𝐶) ⊆cat (Homf𝐶) ∧ ∀𝑥 ∈ (Base‘𝐶)(((Id‘𝐶)‘𝑥) ∈ (𝑥(Homf𝐶)𝑥) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Homf𝐶)𝑦)∀𝑔 ∈ (𝑦(Homf𝐶)𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Homf𝐶)𝑧)))))
4910, 46, 48mpbir2and 713 1 (𝐶 ∈ Cat → (Homf𝐶) ∈ (Subcat‘𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1542  wcel 2113  wral 3053  Vcvv 3397  wss 3841  cop 4519   class class class wbr 5027   × cxp 5517   Fn wfn 6328  cfv 6333  (class class class)co 7164  Basecbs 16579  Hom chom 16672  compcco 16673  Catccat 17031  Idccid 17032  Homf chomf 17033  cat cssc 17175  Subcatcsubc 17177
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7121  df-ov 7167  df-oprab 7168  df-mpo 7169  df-1st 7707  df-2nd 7708  df-pm 8433  df-ixp 8501  df-cat 17035  df-cid 17036  df-homf 17037  df-ssc 17178  df-subc 17180
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator