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

Theorem catcval 17185
 Description: Value of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017.)
Hypotheses
Ref Expression
catcval.c 𝐶 = (CatCat‘𝑈)
catcval.u (𝜑𝑈𝑉)
catcval.b (𝜑𝐵 = (𝑈 ∩ Cat))
catcval.h (𝜑𝐻 = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥 Func 𝑦)))
catcval.o (𝜑· = (𝑣 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔func 𝑓))))
Assertion
Ref Expression
catcval (𝜑𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
Distinct variable groups:   𝑥,𝑣,𝑦,𝑧,𝐵   𝜑,𝑣,𝑥,𝑦,𝑧   𝑣,𝑈,𝑥,𝑦,𝑧   𝑓,𝑔,𝑣,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑓,𝑔)   𝐵(𝑓,𝑔)   𝐶(𝑥,𝑦,𝑧,𝑣,𝑓,𝑔)   · (𝑥,𝑦,𝑧,𝑣,𝑓,𝑔)   𝑈(𝑓,𝑔)   𝐻(𝑥,𝑦,𝑧,𝑣,𝑓,𝑔)   𝑉(𝑥,𝑦,𝑧,𝑣,𝑓,𝑔)

Proof of Theorem catcval
Dummy variables 𝑢 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 catcval.c . 2 𝐶 = (CatCat‘𝑈)
2 df-catc 17184 . . 3 CatCat = (𝑢 ∈ V ↦ (𝑢 ∩ Cat) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 Func 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔func 𝑓)))⟩})
3 vex 3439 . . . . . 6 𝑢 ∈ V
43inex1 5115 . . . . 5 (𝑢 ∩ Cat) ∈ V
54a1i 11 . . . 4 ((𝜑𝑢 = 𝑈) → (𝑢 ∩ Cat) ∈ V)
6 simpr 485 . . . . . 6 ((𝜑𝑢 = 𝑈) → 𝑢 = 𝑈)
76ineq1d 4110 . . . . 5 ((𝜑𝑢 = 𝑈) → (𝑢 ∩ Cat) = (𝑈 ∩ Cat))
8 catcval.b . . . . . 6 (𝜑𝐵 = (𝑈 ∩ Cat))
98adantr 481 . . . . 5 ((𝜑𝑢 = 𝑈) → 𝐵 = (𝑈 ∩ Cat))
107, 9eqtr4d 2833 . . . 4 ((𝜑𝑢 = 𝑈) → (𝑢 ∩ Cat) = 𝐵)
11 simpr 485 . . . . . 6 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
1211opeq2d 4719 . . . . 5 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx), 𝐵⟩)
13 eqidd 2795 . . . . . . . 8 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 Func 𝑦) = (𝑥 Func 𝑦))
1411, 11, 13mpoeq123dv 7090 . . . . . . 7 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 Func 𝑦)) = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥 Func 𝑦)))
15 catcval.h . . . . . . . 8 (𝜑𝐻 = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥 Func 𝑦)))
1615ad2antrr 722 . . . . . . 7 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 𝐻 = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥 Func 𝑦)))
1714, 16eqtr4d 2833 . . . . . 6 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 Func 𝑦)) = 𝐻)
1817opeq2d 4719 . . . . 5 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 Func 𝑦))⟩ = ⟨(Hom ‘ndx), 𝐻⟩)
1911sqxpeqd 5478 . . . . . . . 8 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵))
20 eqidd 2795 . . . . . . . 8 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑔 ∈ ((2nd𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔func 𝑓)) = (𝑔 ∈ ((2nd𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔func 𝑓)))
2119, 11, 20mpoeq123dv 7090 . . . . . . 7 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔func 𝑓))) = (𝑣 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔func 𝑓))))
22 catcval.o . . . . . . . 8 (𝜑· = (𝑣 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔func 𝑓))))
2322ad2antrr 722 . . . . . . 7 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧𝐵 ↦ (𝑔 ∈ ((2nd𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔func 𝑓))))
2421, 23eqtr4d 2833 . . . . . 6 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔func 𝑓))) = · )
2524opeq2d 4719 . . . . 5 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔func 𝑓)))⟩ = ⟨(comp‘ndx), · ⟩)
2612, 18, 25tpeq123d 4593 . . . 4 (((𝜑𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 Func 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔func 𝑓)))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
275, 10, 26csbied2 3847 . . 3 ((𝜑𝑢 = 𝑈) → (𝑢 ∩ Cat) / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥𝑏, 𝑦𝑏 ↦ (𝑥 Func 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧𝑏 ↦ (𝑔 ∈ ((2nd𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔func 𝑓)))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
28 catcval.u . . . 4 (𝜑𝑈𝑉)
2928elexd 3456 . . 3 (𝜑𝑈 ∈ V)
30 tpex 7330 . . . 4 {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} ∈ V
3130a1i 11 . . 3 (𝜑 → {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} ∈ V)
322, 27, 29, 31fvmptd2 6645 . 2 (𝜑 → (CatCat‘𝑈) = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
331, 32syl5eq 2842 1 (𝜑𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522   ∈ wcel 2080  Vcvv 3436  ⦋csb 3813   ∩ cin 3860  {ctp 4478  ⟨cop 4480   × cxp 5444  ‘cfv 6228  (class class class)co 7019   ∈ cmpo 7021  2nd c2nd 7547  ndxcnx 16309  Basecbs 16312  Hom chom 16405  compcco 16406  Catccat 16764   Func cfunc 16953   ∘func ccofu 16955  CatCatccatc 17183 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-sep 5097  ax-nul 5104  ax-pr 5224  ax-un 7322 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ral 3109  df-rex 3110  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-nul 4214  df-if 4384  df-sn 4475  df-pr 4477  df-tp 4479  df-op 4481  df-uni 4748  df-br 4965  df-opab 5027  df-mpt 5044  df-id 5351  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-iota 6192  df-fun 6230  df-fv 6236  df-oprab 7023  df-mpo 7024  df-catc 17184 This theorem is referenced by:  catcbas  17186  catchomfval  17187  catccofval  17189
 Copyright terms: Public domain W3C validator