fucval

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

	Ref	Expression
Hypotheses	fucval.q	$⊢ Q = C FuncCat D$
	fucval.b	$⊢ B = C Func D$
	fucval.n	$⊢ N = C Nat D$
	fucval.a	$⊢ A = {Base}_{C}$
	fucval.o	$⊢ \underset{˙}{\cdot} = comp (D)$
	fucval.c	$⊢ φ \to C \in Cat$
	fucval.d	$⊢ φ \to D \in Cat$
	fucval.x	$⊢ φ \to \underset{˙}{∙} = (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))$
Assertion	fucval	$⊢ φ \to Q = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\}$

Proof

Step	Hyp	Ref	Expression
1		fucval.q	$⊢ Q = C FuncCat D$
2		fucval.b	$⊢ B = C Func D$
3		fucval.n	$⊢ N = C Nat D$
4		fucval.a	$⊢ A = {Base}_{C}$
5		fucval.o	$⊢ \underset{˙}{\cdot} = comp (D)$
6		fucval.c	$⊢ φ \to C \in Cat$
7		fucval.d	$⊢ φ \to D \in Cat$
8		fucval.x	$⊢ φ \to \underset{˙}{∙} = (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))$
9		df-fuc	$⊢ FuncCat = (t \in Cat, u \in Cat ⟼ \{⟨{Base}_{ndx}, t Func u⟩, ⟨Hom (ndx), t Nat u⟩, ⟨comp (ndx), (v \in ((t Func u) \times (t Func u)), h \in (t Func u) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))))⟩\})$
10	9	a1i	$⊢ φ \to FuncCat = (t \in Cat, u \in Cat ⟼ \{⟨{Base}_{ndx}, t Func u⟩, ⟨Hom (ndx), t Nat u⟩, ⟨comp (ndx), (v \in ((t Func u) \times (t Func u)), h \in (t Func u) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))))⟩\})$
11		simprl	$⊢ (φ \land (t = C \land u = D)) \to t = C$
12		simprr	$⊢ (φ \land (t = C \land u = D)) \to u = D$
13	11 12	oveq12d	$⊢ (φ \land (t = C \land u = D)) \to t Func u = C Func D$
14	13 2	eqtr4di	$⊢ (φ \land (t = C \land u = D)) \to t Func u = B$
15	14	opeq2d	$⊢ (φ \land (t = C \land u = D)) \to ⟨{Base}_{ndx}, t Func u⟩ = ⟨{Base}_{ndx}, B⟩$
16	11 12	oveq12d	$⊢ (φ \land (t = C \land u = D)) \to t Nat u = C Nat D$
17	16 3	eqtr4di	$⊢ (φ \land (t = C \land u = D)) \to t Nat u = N$
18	17	opeq2d	$⊢ (φ \land (t = C \land u = D)) \to ⟨Hom (ndx), t Nat u⟩ = ⟨Hom (ndx), N⟩$
19	14	sqxpeqd	$⊢ (φ \land (t = C \land u = D)) \to (t Func u) \times (t Func u) = B \times B$
20	17	oveqd	$⊢ (φ \land (t = C \land u = D)) \to g (t Nat u) h = g N h$
21	17	oveqd	$⊢ (φ \land (t = C \land u = D)) \to f (t Nat u) g = f N g$
22	11	fveq2d	$⊢ (φ \land (t = C \land u = D)) \to {Base}_{t} = {Base}_{C}$
23	22 4	eqtr4di	$⊢ (φ \land (t = C \land u = D)) \to {Base}_{t} = A$
24	12	fveq2d	$⊢ (φ \land (t = C \land u = D)) \to comp (u) = comp (D)$
25	24 5	eqtr4di	$⊢ (φ \land (t = C \land u = D)) \to comp (u) = \underset{˙}{\cdot}$
26	25	oveqd	$⊢ (φ \land (t = C \land u = D)) \to ⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x) = ⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)$
27	26	oveqd	$⊢ (φ \land (t = C \land u = D)) \to b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x) = b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x)$
28	23 27	mpteq12dv	$⊢ (φ \land (t = C \land u = D)) \to (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x)) = (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))$
29	20 21 28	mpoeq123dv	$⊢ (φ \land (t = C \land u = D)) \to (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))) = (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x)))$
30	29	csbeq2dv	$⊢ (φ \land (t = C \land u = D)) \to ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))) = ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x)))$
31	30	csbeq2dv	$⊢ (φ \land (t = C \land u = D)) \to ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))) = ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x)))$
32	19 14 31	mpoeq123dv	$⊢ (φ \land (t = C \land u = D)) \to (v \in ((t Func u) \times (t Func u)), h \in (t Func u) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x)))) = (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))$
33	8	adantr	$⊢ (φ \land (t = C \land u = D)) \to \underset{˙}{∙} = (v \in (B \times B), h \in B ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g N h), a \in (f N g) ⟼ (x \in A ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ \underset{˙}{\cdot} 1^{st} (h) (x)) a (x))))$
34	32 33	eqtr4d	$⊢ (φ \land (t = C \land u = D)) \to (v \in ((t Func u) \times (t Func u)), h \in (t Func u) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x)))) = \underset{˙}{∙}$
35	34	opeq2d	$⊢ (φ \land (t = C \land u = D)) \to ⟨comp (ndx), (v \in ((t Func u) \times (t Func u)), h \in (t Func u) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))))⟩ = ⟨comp (ndx), \underset{˙}{∙}⟩$
36	15 18 35	tpeq123d	$⊢ (φ \land (t = C \land u = D)) \to \{⟨{Base}_{ndx}, t Func u⟩, ⟨Hom (ndx), t Nat u⟩, ⟨comp (ndx), (v \in ((t Func u) \times (t Func u)), h \in (t Func u) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (t Nat u) h), a \in (f (t Nat u) g) ⟼ (x \in {Base}_{t} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (u) 1^{st} (h) (x)) a (x))))⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\}$
37		tpex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\} \in V$
38	37	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\} \in V$
39	10 36 6 7 38	ovmpod	$⊢ φ \to C FuncCat D = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\}$
40	1 39	syl5eq	$⊢ φ \to Q = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), N⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\}$

Metamath Proof Explorer

Theorem fucval

Proof