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

Theorem ressffth 16864
Description: The inclusion functor from a full subcategory is a full and faithful functor, see also remark 4.4(2) in [Adamek] p. 49. (Contributed by Mario Carneiro, 27-Jan-2017.)
Hypotheses
Ref Expression
ressffth.d 𝐷 = (𝐶s 𝑆)
ressffth.i 𝐼 = (idfunc𝐷)
Assertion
Ref Expression
ressffth ((𝐶 ∈ Cat ∧ 𝑆𝑉) → 𝐼 ∈ ((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶)))

Proof of Theorem ressffth
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relfunc 16788 . . 3 Rel (𝐷 Func 𝐷)
2 ressffth.d . . . . 5 𝐷 = (𝐶s 𝑆)
3 resscat 16778 . . . . 5 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (𝐶s 𝑆) ∈ Cat)
42, 3syl5eqel 2847 . . . 4 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → 𝐷 ∈ Cat)
5 ressffth.i . . . . 5 𝐼 = (idfunc𝐷)
65idfucl 16807 . . . 4 (𝐷 ∈ Cat → 𝐼 ∈ (𝐷 Func 𝐷))
74, 6syl 17 . . 3 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → 𝐼 ∈ (𝐷 Func 𝐷))
8 1st2nd 7413 . . 3 ((Rel (𝐷 Func 𝐷) ∧ 𝐼 ∈ (𝐷 Func 𝐷)) → 𝐼 = ⟨(1st𝐼), (2nd𝐼)⟩)
91, 7, 8sylancr 581 . 2 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → 𝐼 = ⟨(1st𝐼), (2nd𝐼)⟩)
10 eqidd 2765 . . . . . . . . 9 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (Homf𝐷) = (Homf𝐷))
11 eqidd 2765 . . . . . . . . 9 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (compf𝐷) = (compf𝐷))
12 eqid 2764 . . . . . . . . . . . . . 14 (Base‘𝐶) = (Base‘𝐶)
1312ressinbas 16209 . . . . . . . . . . . . 13 (𝑆𝑉 → (𝐶s 𝑆) = (𝐶s (𝑆 ∩ (Base‘𝐶))))
1413adantl 473 . . . . . . . . . . . 12 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (𝐶s 𝑆) = (𝐶s (𝑆 ∩ (Base‘𝐶))))
152, 14syl5eq 2810 . . . . . . . . . . 11 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → 𝐷 = (𝐶s (𝑆 ∩ (Base‘𝐶))))
1615fveq2d 6378 . . . . . . . . . 10 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (Homf𝐷) = (Homf ‘(𝐶s (𝑆 ∩ (Base‘𝐶)))))
17 eqid 2764 . . . . . . . . . . . 12 (Homf𝐶) = (Homf𝐶)
18 simpl 474 . . . . . . . . . . . 12 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → 𝐶 ∈ Cat)
19 inss2 3992 . . . . . . . . . . . . 13 (𝑆 ∩ (Base‘𝐶)) ⊆ (Base‘𝐶)
2019a1i 11 . . . . . . . . . . . 12 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (𝑆 ∩ (Base‘𝐶)) ⊆ (Base‘𝐶))
21 eqid 2764 . . . . . . . . . . . 12 (𝐶s (𝑆 ∩ (Base‘𝐶))) = (𝐶s (𝑆 ∩ (Base‘𝐶)))
22 eqid 2764 . . . . . . . . . . . 12 (𝐶cat ((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))) = (𝐶cat ((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))
2312, 17, 18, 20, 21, 22fullresc 16777 . . . . . . . . . . 11 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → ((Homf ‘(𝐶s (𝑆 ∩ (Base‘𝐶)))) = (Homf ‘(𝐶cat ((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))) ∧ (compf‘(𝐶s (𝑆 ∩ (Base‘𝐶)))) = (compf‘(𝐶cat ((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))))))
2423simpld 488 . . . . . . . . . 10 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (Homf ‘(𝐶s (𝑆 ∩ (Base‘𝐶)))) = (Homf ‘(𝐶cat ((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))))
2516, 24eqtrd 2798 . . . . . . . . 9 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (Homf𝐷) = (Homf ‘(𝐶cat ((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))))
2615fveq2d 6378 . . . . . . . . . 10 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (compf𝐷) = (compf‘(𝐶s (𝑆 ∩ (Base‘𝐶)))))
2723simprd 489 . . . . . . . . . 10 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (compf‘(𝐶s (𝑆 ∩ (Base‘𝐶)))) = (compf‘(𝐶cat ((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))))
2826, 27eqtrd 2798 . . . . . . . . 9 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (compf𝐷) = (compf‘(𝐶cat ((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))))
29 ovex 6873 . . . . . . . . . . 11 (𝐶s 𝑆) ∈ V
302, 29eqeltri 2839 . . . . . . . . . 10 𝐷 ∈ V
3130a1i 11 . . . . . . . . 9 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → 𝐷 ∈ V)
32 ovex 6873 . . . . . . . . . 10 (𝐶cat ((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))) ∈ V
3332a1i 11 . . . . . . . . 9 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (𝐶cat ((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))) ∈ V)
3410, 11, 25, 28, 31, 31, 31, 33funcpropd 16826 . . . . . . . 8 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (𝐷 Func 𝐷) = (𝐷 Func (𝐶cat ((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))))
3512, 17, 18, 20fullsubc 16776 . . . . . . . . 9 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → ((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))) ∈ (Subcat‘𝐶))
36 funcres2 16824 . . . . . . . . 9 (((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))) ∈ (Subcat‘𝐶) → (𝐷 Func (𝐶cat ((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))) ⊆ (𝐷 Func 𝐶))
3735, 36syl 17 . . . . . . . 8 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (𝐷 Func (𝐶cat ((Homf𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))) ⊆ (𝐷 Func 𝐶))
3834, 37eqsstrd 3798 . . . . . . 7 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (𝐷 Func 𝐷) ⊆ (𝐷 Func 𝐶))
3938, 7sseldd 3761 . . . . . 6 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → 𝐼 ∈ (𝐷 Func 𝐶))
409, 39eqeltrrd 2844 . . . . 5 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → ⟨(1st𝐼), (2nd𝐼)⟩ ∈ (𝐷 Func 𝐶))
41 df-br 4809 . . . . 5 ((1st𝐼)(𝐷 Func 𝐶)(2nd𝐼) ↔ ⟨(1st𝐼), (2nd𝐼)⟩ ∈ (𝐷 Func 𝐶))
4240, 41sylibr 225 . . . 4 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (1st𝐼)(𝐷 Func 𝐶)(2nd𝐼))
43 f1oi 6356 . . . . . 6 ( I ↾ (𝑥(Hom ‘𝐷)𝑦)):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(𝑥(Hom ‘𝐷)𝑦)
44 eqid 2764 . . . . . . . 8 (Base‘𝐷) = (Base‘𝐷)
454adantr 472 . . . . . . . 8 (((𝐶 ∈ Cat ∧ 𝑆𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝐷 ∈ Cat)
46 eqid 2764 . . . . . . . 8 (Hom ‘𝐷) = (Hom ‘𝐷)
47 simprl 787 . . . . . . . 8 (((𝐶 ∈ Cat ∧ 𝑆𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝑥 ∈ (Base‘𝐷))
48 simprr 789 . . . . . . . 8 (((𝐶 ∈ Cat ∧ 𝑆𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝑦 ∈ (Base‘𝐷))
495, 44, 45, 46, 47, 48idfu2nd 16803 . . . . . . 7 (((𝐶 ∈ Cat ∧ 𝑆𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑥(2nd𝐼)𝑦) = ( I ↾ (𝑥(Hom ‘𝐷)𝑦)))
50 eqidd 2765 . . . . . . 7 (((𝐶 ∈ Cat ∧ 𝑆𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑥(Hom ‘𝐷)𝑦) = (𝑥(Hom ‘𝐷)𝑦))
51 eqid 2764 . . . . . . . . . 10 (Hom ‘𝐶) = (Hom ‘𝐶)
522, 51resshom 16345 . . . . . . . . 9 (𝑆𝑉 → (Hom ‘𝐶) = (Hom ‘𝐷))
5352ad2antlr 718 . . . . . . . 8 (((𝐶 ∈ Cat ∧ 𝑆𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (Hom ‘𝐶) = (Hom ‘𝐷))
545, 44, 45, 47idfu1 16806 . . . . . . . 8 (((𝐶 ∈ Cat ∧ 𝑆𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((1st𝐼)‘𝑥) = 𝑥)
555, 44, 45, 48idfu1 16806 . . . . . . . 8 (((𝐶 ∈ Cat ∧ 𝑆𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((1st𝐼)‘𝑦) = 𝑦)
5653, 54, 55oveq123d 6862 . . . . . . 7 (((𝐶 ∈ Cat ∧ 𝑆𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (((1st𝐼)‘𝑥)(Hom ‘𝐶)((1st𝐼)‘𝑦)) = (𝑥(Hom ‘𝐷)𝑦))
5749, 50, 56f1oeq123d 6315 . . . . . 6 (((𝐶 ∈ Cat ∧ 𝑆𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((𝑥(2nd𝐼)𝑦):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(((1st𝐼)‘𝑥)(Hom ‘𝐶)((1st𝐼)‘𝑦)) ↔ ( I ↾ (𝑥(Hom ‘𝐷)𝑦)):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(𝑥(Hom ‘𝐷)𝑦)))
5843, 57mpbiri 249 . . . . 5 (((𝐶 ∈ Cat ∧ 𝑆𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑥(2nd𝐼)𝑦):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(((1st𝐼)‘𝑥)(Hom ‘𝐶)((1st𝐼)‘𝑦)))
5958ralrimivva 3117 . . . 4 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → ∀𝑥 ∈ (Base‘𝐷)∀𝑦 ∈ (Base‘𝐷)(𝑥(2nd𝐼)𝑦):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(((1st𝐼)‘𝑥)(Hom ‘𝐶)((1st𝐼)‘𝑦)))
6044, 46, 51isffth2 16842 . . . 4 ((1st𝐼)((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))(2nd𝐼) ↔ ((1st𝐼)(𝐷 Func 𝐶)(2nd𝐼) ∧ ∀𝑥 ∈ (Base‘𝐷)∀𝑦 ∈ (Base‘𝐷)(𝑥(2nd𝐼)𝑦):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(((1st𝐼)‘𝑥)(Hom ‘𝐶)((1st𝐼)‘𝑦))))
6142, 59, 60sylanbrc 578 . . 3 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → (1st𝐼)((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))(2nd𝐼))
62 df-br 4809 . . 3 ((1st𝐼)((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))(2nd𝐼) ↔ ⟨(1st𝐼), (2nd𝐼)⟩ ∈ ((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶)))
6361, 62sylib 209 . 2 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → ⟨(1st𝐼), (2nd𝐼)⟩ ∈ ((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶)))
649, 63eqeltrd 2843 1 ((𝐶 ∈ Cat ∧ 𝑆𝑉) → 𝐼 ∈ ((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wcel 2155  wral 3054  Vcvv 3349  cin 3730  wss 3731  cop 4339   class class class wbr 4808   I cid 5183   × cxp 5274  cres 5278  Rel wrel 5281  1-1-ontowf1o 6066  cfv 6067  (class class class)co 6841  1st c1st 7363  2nd c2nd 7364  Basecbs 16131  s cress 16132  Hom chom 16226  Catccat 16591  Homf chomf 16593  compfccomf 16594  cat cresc 16734  Subcatcsubc 16735   Func cfunc 16780  idfunccidfu 16781   Full cful 16828   Faith cfth 16829
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-1st 7365  df-2nd 7366  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-er 7946  df-map 8061  df-pm 8062  df-ixp 8113  df-en 8160  df-dom 8161  df-sdom 8162  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-nn 11274  df-2 11334  df-3 11335  df-4 11336  df-5 11337  df-6 11338  df-7 11339  df-8 11340  df-9 11341  df-n0 11538  df-z 11624  df-dec 11740  df-ndx 16134  df-slot 16135  df-base 16137  df-sets 16138  df-ress 16139  df-hom 16239  df-cco 16240  df-cat 16595  df-cid 16596  df-homf 16597  df-comf 16598  df-ssc 16736  df-resc 16737  df-subc 16738  df-func 16784  df-idfu 16785  df-full 16830  df-fth 16831
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator