Theorem catcval 17484

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.

Step	Hyp	Ref	Expression
1		catcval.c	. 2 ⊢ 𝐶 = (CatCat‘𝑈)
2		df-catc 17483	. . 3 ⊢ CatCat = (𝑢 ∈ V ↦ ⦋(𝑢 ∩ Cat) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))⟩})
3		vex 3404	. . . . . 6 ⊢ 𝑢 ∈ V
4	3	inex1 5195	. . . . 5 ⊢ (𝑢 ∩ Cat) ∈ V
5	4	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Cat) ∈ V)
6		simpr 488	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 𝑢 = 𝑈)
7	6	ineq1d 4112	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Cat) = (𝑈 ∩ Cat))
8		catcval.b	. . . . . 6 ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat))
9	8	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 = 𝑈) → 𝐵 = (𝑈 ∩ Cat))
10	7, 9	eqtr4d 2777	. . . 4 ⊢ ((𝜑 ∧ 𝑢 = 𝑈) → (𝑢 ∩ Cat) = 𝐵)
11		simpr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
12	11	opeq2d 4778	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx), 𝐵⟩)
13		eqidd 2740	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 Func 𝑦) = (𝑥 Func 𝑦))
14	11, 11, 13	mpoeq123dv 7255	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦)) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 Func 𝑦)))
15		catcval.h	. . . . . . . 8 ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 Func 𝑦)))
16	15	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → 𝐻 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 Func 𝑦)))
17	14, 16	eqtr4d 2777	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦)) = 𝐻)
18	17	opeq2d 4778	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → ⟨(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦))⟩ = ⟨(Hom ‘ndx), 𝐻⟩)
19	11	sqxpeqd 5567	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵))
20		eqidd 2740	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)) = (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))
21	19, 11, 20	mpoeq123dv 7255	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓))) = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓))))
22		catcval.o	. . . . . . . 8 ⊢ (𝜑 → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓))))
23	22	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → · = (𝑣 ∈ (𝐵 × 𝐵), 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓))))
24	21, 23	eqtr4d 2777	. . . . . 6 ⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓))) = · )
25	24	opeq2d 4778	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))⟩ = ⟨(comp‘ndx), · ⟩)
26	12, 18, 25	tpeq123d 4649	. . . 4 ⊢ (((𝜑 ∧ 𝑢 = 𝑈) ∧ 𝑏 = 𝐵) → {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
27	5, 10, 26	csbied2 3837	. . 3 ⊢ ((𝜑 ∧ 𝑢 = 𝑈) → ⦋(𝑢 ∩ Cat) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx), (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ (𝑥 Func 𝑦))⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝑏 × 𝑏), 𝑧 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑣) Func 𝑧), 𝑓 ∈ ( Func ‘𝑣) ↦ (𝑔 ∘func 𝑓)))⟩} = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
28		catcval.u	. . . 4 ⊢ (𝜑 → 𝑈 ∈ 𝑉)
29	28	elexd 3420	. . 3 ⊢ (𝜑 → 𝑈 ∈ V)
30		tpex 7500	. . . 4 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} ∈ V
31	30	a1i 11	. . 3 ⊢ (𝜑 → {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩} ∈ V)
32	2, 27, 29, 31	fvmptd2 6795	. 2 ⊢ (𝜑 → (CatCat‘𝑈) = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})
33	1, 32	syl5eq 2786	1 ⊢ (𝜑 → 𝐶 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), · ⟩})

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1542   ∈ wcel 2114  Vcvv 3400  ⦋csb 3800   ∩ cin 3852  {ctp 4530  ⟨cop 4532   × cxp 5533  ‘cfv 6349  (class class class)co 7182   ∈ cmpo 7184  2^nd c2nd 7725  ndxcnx 16595  Basecbs 16598  Hom chom 16691  compcco 16692  Catccat 17050   Func cfunc 17241   ∘_func ccofu 17243  CatCatccatc 17482

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 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pr 5306  ax-un 7491

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 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3402  df-sbc 3686  df-csb 3801  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4222  df-if 4425  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4807  df-br 5041  df-opab 5103  df-mpt 5121  df-id 5439  df-xp 5541  df-rel 5542  df-cnv 5543  df-co 5544  df-dm 5545  df-iota 6307  df-fun 6351  df-fv 6357  df-oprab 7186  df-mpo 7187  df-catc 17483

This theorem is referenced by:  catcbas  17485  catchomfval  17486  catccofval  17488