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

Theorem fthsetcestrc 17413
 Description: The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is faithful. (Contributed by AV, 31-Mar-2020.)
Hypotheses
Ref Expression
funcsetcestrc.s 𝑆 = (SetCat‘𝑈)
funcsetcestrc.c 𝐶 = (Base‘𝑆)
funcsetcestrc.f (𝜑𝐹 = (𝑥𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))
funcsetcestrc.u (𝜑𝑈 ∈ WUni)
funcsetcestrc.o (𝜑 → ω ∈ 𝑈)
funcsetcestrc.g (𝜑𝐺 = (𝑥𝐶, 𝑦𝐶 ↦ ( I ↾ (𝑦m 𝑥))))
funcsetcestrc.e 𝐸 = (ExtStrCat‘𝑈)
Assertion
Ref Expression
fthsetcestrc (𝜑𝐹(𝑆 Faith 𝐸)𝐺)
Distinct variable groups:   𝑥,𝐶   𝜑,𝑥   𝑦,𝐶,𝑥   𝜑,𝑦   𝑥,𝐸
Allowed substitution hints:   𝑆(𝑥,𝑦)   𝑈(𝑥,𝑦)   𝐸(𝑦)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)

Proof of Theorem fthsetcestrc
Dummy variables 𝑎 𝑏 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funcsetcestrc.s . . 3 𝑆 = (SetCat‘𝑈)
2 funcsetcestrc.c . . 3 𝐶 = (Base‘𝑆)
3 funcsetcestrc.f . . 3 (𝜑𝐹 = (𝑥𝐶 ↦ {⟨(Base‘ndx), 𝑥⟩}))
4 funcsetcestrc.u . . 3 (𝜑𝑈 ∈ WUni)
5 funcsetcestrc.o . . 3 (𝜑 → ω ∈ 𝑈)
6 funcsetcestrc.g . . 3 (𝜑𝐺 = (𝑥𝐶, 𝑦𝐶 ↦ ( I ↾ (𝑦m 𝑥))))
7 funcsetcestrc.e . . 3 𝐸 = (ExtStrCat‘𝑈)
81, 2, 3, 4, 5, 6, 7funcsetcestrc 17412 . 2 (𝜑𝐹(𝑆 Func 𝐸)𝐺)
91, 2, 3, 4, 5, 6, 7funcsetcestrclem8 17410 . . . 4 ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → (𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)⟶((𝐹𝑎)(Hom ‘𝐸)(𝐹𝑏)))
104adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → 𝑈 ∈ WUni)
11 eqid 2824 . . . . . . . . . . . . 13 (Hom ‘𝑆) = (Hom ‘𝑆)
121, 4setcbas 17336 . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 = (Base‘𝑆))
1312, 2syl6reqr 2878 . . . . . . . . . . . . . . . . 17 (𝜑𝐶 = 𝑈)
1413eleq2d 2901 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑎𝐶𝑎𝑈))
1514biimpcd 252 . . . . . . . . . . . . . . 15 (𝑎𝐶 → (𝜑𝑎𝑈))
1615adantr 484 . . . . . . . . . . . . . 14 ((𝑎𝐶𝑏𝐶) → (𝜑𝑎𝑈))
1716impcom 411 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → 𝑎𝑈)
1813eleq2d 2901 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑏𝐶𝑏𝑈))
1918biimpcd 252 . . . . . . . . . . . . . . 15 (𝑏𝐶 → (𝜑𝑏𝑈))
2019adantl 485 . . . . . . . . . . . . . 14 ((𝑎𝐶𝑏𝐶) → (𝜑𝑏𝑈))
2120impcom 411 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → 𝑏𝑈)
221, 10, 11, 17, 21setchom 17338 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → (𝑎(Hom ‘𝑆)𝑏) = (𝑏m 𝑎))
2322eleq2d 2901 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → ( ∈ (𝑎(Hom ‘𝑆)𝑏) ↔ ∈ (𝑏m 𝑎)))
241, 2, 3, 4, 5, 6funcsetcestrclem6 17408 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝐶𝑏𝐶) ∧ ∈ (𝑏m 𝑎)) → ((𝑎𝐺𝑏)‘) = )
25243expia 1118 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → ( ∈ (𝑏m 𝑎) → ((𝑎𝐺𝑏)‘) = ))
2623, 25sylbid 243 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → ( ∈ (𝑎(Hom ‘𝑆)𝑏) → ((𝑎𝐺𝑏)‘) = ))
2726com12 32 . . . . . . . . 9 ( ∈ (𝑎(Hom ‘𝑆)𝑏) → ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → ((𝑎𝐺𝑏)‘) = ))
2827adantr 484 . . . . . . . 8 (( ∈ (𝑎(Hom ‘𝑆)𝑏) ∧ 𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)) → ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → ((𝑎𝐺𝑏)‘) = ))
2928impcom 411 . . . . . . 7 (((𝜑 ∧ (𝑎𝐶𝑏𝐶)) ∧ ( ∈ (𝑎(Hom ‘𝑆)𝑏) ∧ 𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏))) → ((𝑎𝐺𝑏)‘) = )
3022eleq2d 2901 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → (𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏) ↔ 𝑘 ∈ (𝑏m 𝑎)))
311, 2, 3, 4, 5, 6funcsetcestrclem6 17408 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑎𝐶𝑏𝐶) ∧ 𝑘 ∈ (𝑏m 𝑎)) → ((𝑎𝐺𝑏)‘𝑘) = 𝑘)
32313expia 1118 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → (𝑘 ∈ (𝑏m 𝑎) → ((𝑎𝐺𝑏)‘𝑘) = 𝑘))
3330, 32sylbid 243 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → (𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏) → ((𝑎𝐺𝑏)‘𝑘) = 𝑘))
3433com12 32 . . . . . . . . 9 (𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏) → ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → ((𝑎𝐺𝑏)‘𝑘) = 𝑘))
3534adantl 485 . . . . . . . 8 (( ∈ (𝑎(Hom ‘𝑆)𝑏) ∧ 𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)) → ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → ((𝑎𝐺𝑏)‘𝑘) = 𝑘))
3635impcom 411 . . . . . . 7 (((𝜑 ∧ (𝑎𝐶𝑏𝐶)) ∧ ( ∈ (𝑎(Hom ‘𝑆)𝑏) ∧ 𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏))) → ((𝑎𝐺𝑏)‘𝑘) = 𝑘)
3729, 36eqeq12d 2840 . . . . . 6 (((𝜑 ∧ (𝑎𝐶𝑏𝐶)) ∧ ( ∈ (𝑎(Hom ‘𝑆)𝑏) ∧ 𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏))) → (((𝑎𝐺𝑏)‘) = ((𝑎𝐺𝑏)‘𝑘) ↔ = 𝑘))
3837biimpd 232 . . . . 5 (((𝜑 ∧ (𝑎𝐶𝑏𝐶)) ∧ ( ∈ (𝑎(Hom ‘𝑆)𝑏) ∧ 𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏))) → (((𝑎𝐺𝑏)‘) = ((𝑎𝐺𝑏)‘𝑘) → = 𝑘))
3938ralrimivva 3186 . . . 4 ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → ∀ ∈ (𝑎(Hom ‘𝑆)𝑏)∀𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)(((𝑎𝐺𝑏)‘) = ((𝑎𝐺𝑏)‘𝑘) → = 𝑘))
40 dff13 7003 . . . 4 ((𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)–1-1→((𝐹𝑎)(Hom ‘𝐸)(𝐹𝑏)) ↔ ((𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)⟶((𝐹𝑎)(Hom ‘𝐸)(𝐹𝑏)) ∧ ∀ ∈ (𝑎(Hom ‘𝑆)𝑏)∀𝑘 ∈ (𝑎(Hom ‘𝑆)𝑏)(((𝑎𝐺𝑏)‘) = ((𝑎𝐺𝑏)‘𝑘) → = 𝑘)))
419, 39, 40sylanbrc 586 . . 3 ((𝜑 ∧ (𝑎𝐶𝑏𝐶)) → (𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)–1-1→((𝐹𝑎)(Hom ‘𝐸)(𝐹𝑏)))
4241ralrimivva 3186 . 2 (𝜑 → ∀𝑎𝐶𝑏𝐶 (𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)–1-1→((𝐹𝑎)(Hom ‘𝐸)(𝐹𝑏)))
43 eqid 2824 . . 3 (Hom ‘𝐸) = (Hom ‘𝐸)
442, 11, 43isfth2 17183 . 2 (𝐹(𝑆 Faith 𝐸)𝐺 ↔ (𝐹(𝑆 Func 𝐸)𝐺 ∧ ∀𝑎𝐶𝑏𝐶 (𝑎𝐺𝑏):(𝑎(Hom ‘𝑆)𝑏)–1-1→((𝐹𝑎)(Hom ‘𝐸)(𝐹𝑏))))
458, 42, 44sylanbrc 586 1 (𝜑𝐹(𝑆 Faith 𝐸)𝐺)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2115  ∀wral 3133  {csn 4550  ⟨cop 4556   class class class wbr 5053   ↦ cmpt 5133   I cid 5447   ↾ cres 5545  ⟶wf 6340  –1-1→wf1 6341  ‘cfv 6344  (class class class)co 7146   ∈ cmpo 7148  ωcom 7571   ↑m cmap 8398  WUnicwun 10116  ndxcnx 16478  Basecbs 16481  Hom chom 16574   Func cfunc 17122   Faith cfth 17171  SetCatcsetc 17333  ExtStrCatcestrc 17370 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7452  ax-inf2 9097  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4826  df-int 4864  df-iun 4908  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6136  df-ord 6182  df-on 6183  df-lim 6184  df-suc 6185  df-iota 6303  df-fun 6346  df-fn 6347  df-f 6348  df-f1 6349  df-fo 6350  df-f1o 6351  df-fv 6352  df-riota 7104  df-ov 7149  df-oprab 7150  df-mpo 7151  df-om 7572  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-oadd 8098  df-omul 8099  df-er 8281  df-ec 8283  df-qs 8287  df-map 8400  df-pm 8401  df-ixp 8454  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-wun 10118  df-ni 10288  df-pli 10289  df-mi 10290  df-lti 10291  df-plpq 10324  df-mpq 10325  df-ltpq 10326  df-enq 10327  df-nq 10328  df-erq 10329  df-plq 10330  df-mq 10331  df-1nq 10332  df-rq 10333  df-ltnq 10334  df-np 10397  df-plp 10399  df-ltp 10401  df-enr 10471  df-nr 10472  df-c 10537  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-nn 11633  df-2 11695  df-3 11696  df-4 11697  df-5 11698  df-6 11699  df-7 11700  df-8 11701  df-9 11702  df-n0 11893  df-z 11977  df-dec 12094  df-uz 12239  df-fz 12893  df-struct 16483  df-ndx 16484  df-slot 16485  df-base 16487  df-hom 16587  df-cco 16588  df-cat 16937  df-cid 16938  df-func 17126  df-fth 17173  df-setc 17334  df-estrc 17371 This theorem is referenced by:  embedsetcestrc  17415
 Copyright terms: Public domain W3C validator