fucpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same functor categories. (Contributed by Mario Carneiro, 26-Jan-2017)

	Ref	Expression
Hypotheses	fucpropd.1	$⊢ φ \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
	fucpropd.2	$⊢ φ \to {comp}_{𝑓} (A) = {comp}_{𝑓} (B)$
	fucpropd.3	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
	fucpropd.4	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
	fucpropd.a	$⊢ φ \to A \in Cat$
	fucpropd.b	$⊢ φ \to B \in Cat$
	fucpropd.c	$⊢ φ \to C \in Cat$
	fucpropd.d	$⊢ φ \to D \in Cat$
Assertion	fucpropd	$⊢ φ \to A FuncCat C = B FuncCat D$

Proof

Step	Hyp	Ref	Expression
1		fucpropd.1	$⊢ φ \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
2		fucpropd.2	$⊢ φ \to {comp}_{𝑓} (A) = {comp}_{𝑓} (B)$
3		fucpropd.3	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
4		fucpropd.4	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
5		fucpropd.a	$⊢ φ \to A \in Cat$
6		fucpropd.b	$⊢ φ \to B \in Cat$
7		fucpropd.c	$⊢ φ \to C \in Cat$
8		fucpropd.d	$⊢ φ \to D \in Cat$
9	1 2 3 4 5 6 7 8	funcpropd	$⊢ φ \to A Func C = B Func D$
10	9	opeq2d	$⊢ φ \to ⟨{Base}_{ndx}, A Func C⟩ = ⟨{Base}_{ndx}, B Func D⟩$
11	1 2 3 4 5 6 7 8	natpropd	$⊢ φ \to A Nat C = B Nat D$
12	11	opeq2d	$⊢ φ \to ⟨Hom (ndx), A Nat C⟩ = ⟨Hom (ndx), B Nat D⟩$
13	9	sqxpeqd	$⊢ φ \to (A Func C) \times (A Func C) = (B Func D) \times (B Func D)$
14	9	adantr	$⊢ (φ \land v \in ((A Func C) \times (A Func C))) \to A Func C = B Func D$
15		nfv	$⊢ Ⅎ f (φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C)))$
16		nfcsb1v	$⊢ \underline{Ⅎ} f ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)))$
17	16	a1i	$⊢ (φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \to \underline{Ⅎ} f ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)))$
18		fvexd	$⊢ (φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \to 1^{st} (v) \in V$
19		nfv	$⊢ Ⅎ g ((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v))$
20		nfcsb1v	$⊢ \underline{Ⅎ} g ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)))$
21	20	a1i	$⊢ ((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \to \underline{Ⅎ} g ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)))$
22		fvexd	$⊢ ((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \to 2^{nd} (v) \in V$
23	11	ad3antrrr	$⊢ (((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \to A Nat C = B Nat D$
24	23	oveqd	$⊢ (((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \to g (A Nat C) h = g (B Nat D) h$
25	23	oveqdr	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land b \in (g (A Nat C) h)) \to f (A Nat C) g = f (B Nat D) g$
26	1	homfeqbas	$⊢ φ \to {Base}_{A} = {Base}_{B}$
27	26	ad4antr	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to {Base}_{A} = {Base}_{B}$
28		eqid	$⊢ {Base}_{C} = {Base}_{C}$
29		eqid	$⊢ Hom (C) = Hom (C)$
30		eqid	$⊢ comp (C) = comp (C)$
31		eqid	$⊢ comp (D) = comp (D)$
32	3	ad5antr	$⊢ (((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \land x \in {Base}_{A}) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
33	4	ad5antr	$⊢ (((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \land x \in {Base}_{A}) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
34		eqid	$⊢ {Base}_{A} = {Base}_{A}$
35		relfunc	$⊢ Rel (A Func C)$
36		simpllr	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to f = 1^{st} (v)$
37		simp-4r	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))$
38	37	simpld	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to v \in ((A Func C) \times (A Func C))$
39		xp1st	$⊢ v \in ((A Func C) \times (A Func C)) \to 1^{st} (v) \in (A Func C)$
40	38 39	syl	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to 1^{st} (v) \in (A Func C)$
41	36 40	eqeltrd	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to f \in (A Func C)$
42		1st2ndbr	$⊢ (Rel (A Func C) \land f \in (A Func C)) \to 1^{st} (f) (A Func C) 2^{nd} (f)$
43	35 41 42	sylancr	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to 1^{st} (f) (A Func C) 2^{nd} (f)$
44	34 28 43	funcf1	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to 1^{st} (f) : {Base}_{A} ⟶ {Base}_{C}$
45	44	ffvelrnda	$⊢ (((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \land x \in {Base}_{A}) \to 1^{st} (f) (x) \in {Base}_{C}$
46		simplr	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to g = 2^{nd} (v)$
47		xp2nd	$⊢ v \in ((A Func C) \times (A Func C)) \to 2^{nd} (v) \in (A Func C)$
48	38 47	syl	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to 2^{nd} (v) \in (A Func C)$
49	46 48	eqeltrd	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to g \in (A Func C)$
50		1st2ndbr	$⊢ (Rel (A Func C) \land g \in (A Func C)) \to 1^{st} (g) (A Func C) 2^{nd} (g)$
51	35 49 50	sylancr	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to 1^{st} (g) (A Func C) 2^{nd} (g)$
52	34 28 51	funcf1	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to 1^{st} (g) : {Base}_{A} ⟶ {Base}_{C}$
53	52	ffvelrnda	$⊢ (((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \land x \in {Base}_{A}) \to 1^{st} (g) (x) \in {Base}_{C}$
54	37	simprd	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to h \in (A Func C)$
55		1st2ndbr	$⊢ (Rel (A Func C) \land h \in (A Func C)) \to 1^{st} (h) (A Func C) 2^{nd} (h)$
56	35 54 55	sylancr	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to 1^{st} (h) (A Func C) 2^{nd} (h)$
57	34 28 56	funcf1	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to 1^{st} (h) : {Base}_{A} ⟶ {Base}_{C}$
58	57	ffvelrnda	$⊢ (((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \land x \in {Base}_{A}) \to 1^{st} (h) (x) \in {Base}_{C}$
59		eqid	$⊢ A Nat C = A Nat C$
60		simplrr	$⊢ (((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \land x \in {Base}_{A}) \to a \in (f (A Nat C) g)$
61	59 60	nat1st2nd	$⊢ (((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \land x \in {Base}_{A}) \to a \in (⟨1^{st} (f), 2^{nd} (f)⟩ (A Nat C) ⟨1^{st} (g), 2^{nd} (g)⟩)$
62		simpr	$⊢ (((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \land x \in {Base}_{A}) \to x \in {Base}_{A}$
63	59 61 34 29 62	natcl	$⊢ (((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \land x \in {Base}_{A}) \to a (x) \in (1^{st} (f) (x) Hom (C) 1^{st} (g) (x))$
64		simplrl	$⊢ (((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \land x \in {Base}_{A}) \to b \in (g (A Nat C) h)$
65	59 64	nat1st2nd	$⊢ (((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \land x \in {Base}_{A}) \to b \in (⟨1^{st} (g), 2^{nd} (g)⟩ (A Nat C) ⟨1^{st} (h), 2^{nd} (h)⟩)$
66	59 65 34 29 62	natcl	$⊢ (((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \land x \in {Base}_{A}) \to b (x) \in (1^{st} (g) (x) Hom (C) 1^{st} (h) (x))$
67	28 29 30 31 32 33 45 53 58 63 66	comfeqval	$⊢ (((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \land x \in {Base}_{A}) \to b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (C) 1^{st} (h) (x)) a (x) = b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)$
68	27 67	mpteq12dva	$⊢ ((((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \land (b \in (g (A Nat C) h) \land a \in (f (A Nat C) g))) \to (x \in {Base}_{A} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (C) 1^{st} (h) (x)) a (x)) = (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x))$
69	24 25 68	mpoeq123dva	$⊢ (((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \to (b \in (g (A Nat C) h), a \in (f (A Nat C) g) ⟼ (x \in {Base}_{A} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (C) 1^{st} (h) (x)) a (x))) = (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)))$
70		csbeq1a	$⊢ g = 2^{nd} (v) \to (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x))) = ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)))$
71	70	adantl	$⊢ (((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \to (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x))) = ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)))$
72	69 71	eqtrd	$⊢ (((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \land g = 2^{nd} (v)) \to (b \in (g (A Nat C) h), a \in (f (A Nat C) g) ⟼ (x \in {Base}_{A} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (C) 1^{st} (h) (x)) a (x))) = ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)))$
73	19 21 22 72	csbiedf	$⊢ ((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \to ⦋ 2^{nd} (v) / g ⦌ (b \in (g (A Nat C) h), a \in (f (A Nat C) g) ⟼ (x \in {Base}_{A} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (C) 1^{st} (h) (x)) a (x))) = ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)))$
74		csbeq1a	$⊢ f = 1^{st} (v) \to ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x))) = ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)))$
75	74	adantl	$⊢ ((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \to ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x))) = ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)))$
76	73 75	eqtrd	$⊢ ((φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \land f = 1^{st} (v)) \to ⦋ 2^{nd} (v) / g ⦌ (b \in (g (A Nat C) h), a \in (f (A Nat C) g) ⟼ (x \in {Base}_{A} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (C) 1^{st} (h) (x)) a (x))) = ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)))$
77	15 17 18 76	csbiedf	$⊢ (φ \land (v \in ((A Func C) \times (A Func C)) \land h \in (A Func C))) \to ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (A Nat C) h), a \in (f (A Nat C) g) ⟼ (x \in {Base}_{A} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (C) 1^{st} (h) (x)) a (x))) = ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)))$
78	13 14 77	mpoeq123dva	$⊢ φ \to (v \in ((A Func C) \times (A Func C)), h \in (A Func C) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (A Nat C) h), a \in (f (A Nat C) g) ⟼ (x \in {Base}_{A} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (C) 1^{st} (h) (x)) a (x)))) = (v \in ((B Func D) \times (B Func D)), h \in (B Func D) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x))))$
79	78	opeq2d	$⊢ φ \to ⟨comp (ndx), (v \in ((A Func C) \times (A Func C)), h \in (A Func C) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (A Nat C) h), a \in (f (A Nat C) g) ⟼ (x \in {Base}_{A} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (C) 1^{st} (h) (x)) a (x))))⟩ = ⟨comp (ndx), (v \in ((B Func D) \times (B Func D)), h \in (B Func D) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x))))⟩$
80	10 12 79	tpeq123d	$⊢ φ \to \{⟨{Base}_{ndx}, A Func C⟩, ⟨Hom (ndx), A Nat C⟩, ⟨comp (ndx), (v \in ((A Func C) \times (A Func C)), h \in (A Func C) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (A Nat C) h), a \in (f (A Nat C) g) ⟼ (x \in {Base}_{A} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (C) 1^{st} (h) (x)) a (x))))⟩\} = \{⟨{Base}_{ndx}, B Func D⟩, ⟨Hom (ndx), B Nat D⟩, ⟨comp (ndx), (v \in ((B Func D) \times (B Func D)), h \in (B Func D) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x))))⟩\}$
81		eqid	$⊢ A FuncCat C = A FuncCat C$
82		eqid	$⊢ A Func C = A Func C$
83		eqidd	$⊢ φ \to (v \in ((A Func C) \times (A Func C)), h \in (A Func C) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (A Nat C) h), a \in (f (A Nat C) g) ⟼ (x \in {Base}_{A} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (C) 1^{st} (h) (x)) a (x)))) = (v \in ((A Func C) \times (A Func C)), h \in (A Func C) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (A Nat C) h), a \in (f (A Nat C) g) ⟼ (x \in {Base}_{A} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (C) 1^{st} (h) (x)) a (x))))$
84	81 82 59 34 30 5 7 83	fucval	$⊢ φ \to A FuncCat C = \{⟨{Base}_{ndx}, A Func C⟩, ⟨Hom (ndx), A Nat C⟩, ⟨comp (ndx), (v \in ((A Func C) \times (A Func C)), h \in (A Func C) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (A Nat C) h), a \in (f (A Nat C) g) ⟼ (x \in {Base}_{A} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (C) 1^{st} (h) (x)) a (x))))⟩\}$
85		eqid	$⊢ B FuncCat D = B FuncCat D$
86		eqid	$⊢ B Func D = B Func D$
87		eqid	$⊢ B Nat D = B Nat D$
88		eqid	$⊢ {Base}_{B} = {Base}_{B}$
89		eqidd	$⊢ φ \to (v \in ((B Func D) \times (B Func D)), h \in (B Func D) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x)))) = (v \in ((B Func D) \times (B Func D)), h \in (B Func D) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x))))$
90	85 86 87 88 31 6 8 89	fucval	$⊢ φ \to B FuncCat D = \{⟨{Base}_{ndx}, B Func D⟩, ⟨Hom (ndx), B Nat D⟩, ⟨comp (ndx), (v \in ((B Func D) \times (B Func D)), h \in (B Func D) ⟼ ⦋ 1^{st} (v) / f ⦌ ⦋ 2^{nd} (v) / g ⦌ (b \in (g (B Nat D) h), a \in (f (B Nat D) g) ⟼ (x \in {Base}_{B} ⟼ b (x) (⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ comp (D) 1^{st} (h) (x)) a (x))))⟩\}$
91	80 84 90	3eqtr4d	$⊢ φ \to A FuncCat C = B FuncCat D$

Metamath Proof Explorer

Theorem fucpropd

Proof