fuccofval - Metamath Proof Explorer

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

Theorem fuccofval 18117

Description: Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)

**Hypotheses**
Ref	Expression
fucval.q	⊢ 𝑄 = (𝐶 FuncCat 𝐷)
fucval.b	⊢ 𝐵 = (𝐶 Func 𝐷)
fucval.n	⊢ 𝑁 = (𝐶 Nat 𝐷)
fucval.a	⊢ 𝐴 = (Base‘𝐶)
fucval.o	⊢ · = (comp‘𝐷)
fucval.c	⊢ (𝜑 → 𝐶 ∈ Cat)
fucval.d	⊢ (𝜑 → 𝐷 ∈ Cat)
fuccofval.x	⊢ ∙ = (comp‘𝑄)

**Assertion**
Ref	Expression
fuccofval	⊢ (𝜑 → ∙ = (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))))

Distinct variable groups: 𝑣,ℎ,𝐵 𝑎,𝑏,𝑓,𝑔,ℎ,𝑣,𝑥,𝜑 𝐶,𝑎,𝑏,𝑓,𝑔,ℎ,𝑣,𝑥 𝐷,𝑎,𝑏,𝑓,𝑔,ℎ,𝑣,𝑥 Allowed substitution hints: 𝐴(𝑥, 𝑣, 𝑓, 𝑔, ℎ, 𝑎, 𝑏) 𝐵(𝑥, 𝑓, 𝑔, 𝑎, 𝑏) 𝑄(𝑥, 𝑣, 𝑓, 𝑔, ℎ, 𝑎, 𝑏) ∙ (𝑥, 𝑣, 𝑓, 𝑔, ℎ, 𝑎, 𝑏) · (𝑥, 𝑣, 𝑓, 𝑔, ℎ, 𝑎, 𝑏) 𝑁(𝑥, 𝑣, 𝑓, 𝑔, ℎ, 𝑎, 𝑏)

**Proof of Theorem fuccofval**
Step	Hyp	Ref	Expression
1		fucval.q	. . . 4 ⊢ 𝑄 = (𝐶 FuncCat 𝐷)
2		fucval.b	. . . 4 ⊢ 𝐵 = (𝐶 Func 𝐷)
3		fucval.n	. . . 4 ⊢ 𝑁 = (𝐶 Nat 𝐷)
4		fucval.a	. . . 4 ⊢ 𝐴 = (Base‘𝐶)
5		fucval.o	. . . 4 ⊢ · = (comp‘𝐷)
6		fucval.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Cat)
7		fucval.d	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Cat)
8		eqidd 2762	. . . 4 ⊢ (𝜑 → (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))) = (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))))
9	1, 2, 3, 4, 5, 6, 7, 8	fucval 18116	. . 3 ⊢ (𝜑 → 𝑄 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩})
10	9	fveq2d 6881	. 2 ⊢ (𝜑 → (comp‘𝑄) = (comp‘{⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩}))
11		fuccofval.x	. 2 ⊢ ∙ = (comp‘𝑄)
12	2	ovexi 7446	. . . . 5 ⊢ 𝐵 ∈ V
13	12, 12	xpex 7756	. . . 4 ⊢ (𝐵 × 𝐵) ∈ V
14	13, 12	mpoex 8081	. . 3 ⊢ (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))) ∈ V
15		catstr 18115	. . . 4 ⊢ {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩} Struct ⟨1, ;15⟩
16		ccoid 17565	. . . 4 ⊢ comp = Slot (comp‘ndx)
17		snsstp3 4779	. . . 4 ⊢ {⟨(comp‘ndx), (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩} ⊆ {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩}
18	15, 16, 17	strfv 17361	. . 3 ⊢ ((𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))) ∈ V → (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))) = (comp‘{⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩}))
19	14, 18	ax-mp 5	. 2 ⊢ (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))) = (comp‘{⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝑁⟩, ⟨(comp‘ndx), (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))⟩})
20	10, 11, 19	3eqtr4g 2821	1 ⊢ (𝜑 → ∙ = (𝑣 ∈ (𝐵 × 𝐵), ℎ ∈ 𝐵 ↦ ⦋(1^st ‘𝑣) / 𝑓⦌⦋(2^nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔𝑁ℎ), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥 ∈ 𝐴 ↦ ((𝑏‘𝑥)(⟨((1^st ‘𝑓)‘𝑥), ((1^st ‘𝑔)‘𝑥)⟩ · ((1^st ‘ℎ)‘𝑥))(𝑎‘𝑥))))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ∈ wcel 2145 Vcvv 3451 ⦋csb 3847 {ctp 4588 ⟨cop 4590 ↦ cmpt 5186 × cxp 5649 ‘cfv 6531 (class class class)co 7412 ∈ cmpo 7414 1^st c1st 7988 2^nd c2nd 7989 1c1 11182 5c5 12381 cdc 12795 ndxcnx 17351 Basecbs 17367 Hom chom 17419 compcco 17420 Catccat 17818 Func cfunc 18009 Nat cnat 18099 FuncCat cfuc 18100

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-er 8701 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-nn 12317 df-2 12386 df-3 12387 df-4 12388 df-5 12389 df-6 12390 df-7 12391 df-8 12392 df-9 12393 df-n0 12588 df-z 12675 df-dec 12796 df-uz 12947 df-fz 13621 df-struct 17305 df-slot 17340 df-ndx 17352 df-base 17368 df-hom 17432 df-cco 17433 df-fuc 18102

This theorem is used by: fucbas 18118 fuchom 18119 fucco 18120

W3C validator