natpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same natural transformations. (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	natpropd	$⊢ φ \to A Nat C = B Nat 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	adantr	$⊢ (φ \land f \in (A Func C)) \to A Func C = B Func D$
11		nfv	$⊢ Ⅎ r (φ \land (f \in (A Func C) \land g \in (A Func C)))$
12		nfcsb1v	$⊢ \underline{Ⅎ} r ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\}$
13	12	a1i	$⊢ (φ \land (f \in (A Func C) \land g \in (A Func C))) \to \underline{Ⅎ} r ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\}$
14		fvexd	$⊢ (φ \land (f \in (A Func C) \land g \in (A Func C))) \to 1^{st} (f) \in V$
15		nfv	$⊢ Ⅎ s ((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f))$
16		nfcsb1v	$⊢ \underline{Ⅎ} s ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\}$
17	16	a1i	$⊢ ((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \to \underline{Ⅎ} s ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\}$
18		fvexd	$⊢ ((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \to 1^{st} (g) \in V$
19		eqid	$⊢ {Base}_{C} = {Base}_{C}$
20		eqid	$⊢ Hom (C) = Hom (C)$
21		eqid	$⊢ Hom (D) = Hom (D)$
22	3	ad4antr	$⊢ ((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land x \in {Base}_{A}) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
23		eqid	$⊢ {Base}_{A} = {Base}_{A}$
24		simplr	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to r = 1^{st} (f)$
25		relfunc	$⊢ Rel (A Func C)$
26		simpllr	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to (f \in (A Func C) \land g \in (A Func C))$
27	26	simpld	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to f \in (A Func C)$
28		1st2ndbr	$⊢ (Rel (A Func C) \land f \in (A Func C)) \to 1^{st} (f) (A Func C) 2^{nd} (f)$
29	25 27 28	sylancr	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to 1^{st} (f) (A Func C) 2^{nd} (f)$
30	24 29	eqbrtrd	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to r (A Func C) 2^{nd} (f)$
31	23 19 30	funcf1	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to r : {Base}_{A} ⟶ {Base}_{C}$
32	31	ffvelcdmda	$⊢ ((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land x \in {Base}_{A}) \to r (x) \in {Base}_{C}$
33		simpr	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to s = 1^{st} (g)$
34	26	simprd	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to g \in (A Func C)$
35		1st2ndbr	$⊢ (Rel (A Func C) \land g \in (A Func C)) \to 1^{st} (g) (A Func C) 2^{nd} (g)$
36	25 34 35	sylancr	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to 1^{st} (g) (A Func C) 2^{nd} (g)$
37	33 36	eqbrtrd	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to s (A Func C) 2^{nd} (g)$
38	23 19 37	funcf1	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to s : {Base}_{A} ⟶ {Base}_{C}$
39	38	ffvelcdmda	$⊢ ((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land x \in {Base}_{A}) \to s (x) \in {Base}_{C}$
40	19 20 21 22 32 39	homfeqval	$⊢ ((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land x \in {Base}_{A}) \to r (x) Hom (C) s (x) = r (x) Hom (D) s (x)$
41	40	ixpeq2dva	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to \underset{x \in {Base}_{A}}{⨉} (r (x) Hom (C) s (x)) = \underset{x \in {Base}_{A}}{⨉} (r (x) Hom (D) s (x))$
42	1	homfeqbas	$⊢ φ \to {Base}_{A} = {Base}_{B}$
43	42	ad3antrrr	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to {Base}_{A} = {Base}_{B}$
44	43	ixpeq1d	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to \underset{x \in {Base}_{A}}{⨉} (r (x) Hom (D) s (x)) = \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x))$
45	41 44	eqtrd	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to \underset{x \in {Base}_{A}}{⨉} (r (x) Hom (C) s (x)) = \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x))$
46		fveq2	$⊢ x = z \to r (x) = r (z)$
47		fveq2	$⊢ x = z \to s (x) = s (z)$
48	46 47	oveq12d	$⊢ x = z \to r (x) Hom (C) s (x) = r (z) Hom (C) s (z)$
49	48	cbvixpv	$⊢ \underset{x \in {Base}_{A}}{⨉} (r (x) Hom (C) s (x)) = \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))$
50	49	eleq2i	$⊢ a \in \underset{x \in {Base}_{A}}{⨉} (r (x) Hom (C) s (x)) \leftrightarrow a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))$
51	43	adantr	$⊢ ((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \to {Base}_{A} = {Base}_{B}$
52	51	adantr	$⊢ (((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \to {Base}_{A} = {Base}_{B}$
53		eqid	$⊢ Hom (A) = Hom (A)$
54		eqid	$⊢ Hom (B) = Hom (B)$
55	1	ad6antr	$⊢ ((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
56		simplr	$⊢ ((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to x \in {Base}_{A}$
57		simpr	$⊢ ((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to y \in {Base}_{A}$
58	23 53 54 55 56 57	homfeqval	$⊢ ((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to x Hom (A) y = x Hom (B) y$
59		eqid	$⊢ comp (C) = comp (C)$
60		eqid	$⊢ comp (D) = comp (D)$
61	3	ad7antr	$⊢ (((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land h \in (x Hom (A) y)) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
62	4	ad7antr	$⊢ (((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land h \in (x Hom (A) y)) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
63	32	ad5ant13	$⊢ (((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land h \in (x Hom (A) y)) \to r (x) \in {Base}_{C}$
64	31	ad2antrr	$⊢ (((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \to r : {Base}_{A} ⟶ {Base}_{C}$
65	64	ffvelcdmda	$⊢ ((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to r (y) \in {Base}_{C}$
66	65	adantr	$⊢ (((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land h \in (x Hom (A) y)) \to r (y) \in {Base}_{C}$
67	38	ad2antrr	$⊢ (((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \to s : {Base}_{A} ⟶ {Base}_{C}$
68	67	ffvelcdmda	$⊢ ((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to s (y) \in {Base}_{C}$
69	68	adantr	$⊢ (((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land h \in (x Hom (A) y)) \to s (y) \in {Base}_{C}$
70	30	ad3antrrr	$⊢ ((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to r (A Func C) 2^{nd} (f)$
71	23 53 20 70 56 57	funcf2	$⊢ ((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to (x 2^{nd} (f) y) : x Hom (A) y ⟶ r (x) Hom (C) r (y)$
72	71	ffvelcdmda	$⊢ (((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land h \in (x Hom (A) y)) \to (x 2^{nd} (f) y) (h) \in (r (x) Hom (C) r (y))$
73		fveq2	$⊢ z = y \to r (z) = r (y)$
74		fveq2	$⊢ z = y \to s (z) = s (y)$
75	73 74	oveq12d	$⊢ z = y \to r (z) Hom (C) s (z) = r (y) Hom (C) s (y)$
76	75	fvixp	$⊢ (a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z)) \land y \in {Base}_{A}) \to a (y) \in (r (y) Hom (C) s (y))$
77	76	ad5ant24	$⊢ (((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land h \in (x Hom (A) y)) \to a (y) \in (r (y) Hom (C) s (y))$
78	19 20 59 60 61 62 63 66 69 72 77	comfeqval	$⊢ (((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land h \in (x Hom (A) y)) \to a (y) (⟨r (x), r (y)⟩ comp (C) s (y)) (x 2^{nd} (f) y) (h) = a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h)$
79	39	ad5ant13	$⊢ (((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land h \in (x Hom (A) y)) \to s (x) \in {Base}_{C}$
80		fveq2	$⊢ z = x \to r (z) = r (x)$
81		fveq2	$⊢ z = x \to s (z) = s (x)$
82	80 81	oveq12d	$⊢ z = x \to r (z) Hom (C) s (z) = r (x) Hom (C) s (x)$
83	82	fvixp	$⊢ (a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z)) \land x \in {Base}_{A}) \to a (x) \in (r (x) Hom (C) s (x))$
84	83	ad5ant23	$⊢ (((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land h \in (x Hom (A) y)) \to a (x) \in (r (x) Hom (C) s (x))$
85	37	ad3antrrr	$⊢ ((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to s (A Func C) 2^{nd} (g)$
86	23 53 20 85 56 57	funcf2	$⊢ ((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to (x 2^{nd} (g) y) : x Hom (A) y ⟶ s (x) Hom (C) s (y)$
87	86	ffvelcdmda	$⊢ (((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land h \in (x Hom (A) y)) \to (x 2^{nd} (g) y) (h) \in (s (x) Hom (C) s (y))$
88	19 20 59 60 61 62 63 79 69 84 87	comfeqval	$⊢ (((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land h \in (x Hom (A) y)) \to (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (C) s (y)) a (x) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)$
89	78 88	eqeq12d	$⊢ (((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land h \in (x Hom (A) y)) \to (a (y) (⟨r (x), r (y)⟩ comp (C) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (C) s (y)) a (x) \leftrightarrow a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x))$
90	58 89	raleqbidva	$⊢ ((((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to (\forall h \in (x Hom (A) y) a (y) (⟨r (x), r (y)⟩ comp (C) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (C) s (y)) a (x) \leftrightarrow \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x))$
91	52 90	raleqbidva	$⊢ (((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \land x \in {Base}_{A}) \to (\forall y \in {Base}_{A} \forall h \in (x Hom (A) y) a (y) (⟨r (x), r (y)⟩ comp (C) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (C) s (y)) a (x) \leftrightarrow \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x))$
92	51 91	raleqbidva	$⊢ ((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{z \in {Base}_{A}}{⨉} (r (z) Hom (C) s (z))) \to (\forall x \in {Base}_{A} \forall y \in {Base}_{A} \forall h \in (x Hom (A) y) a (y) (⟨r (x), r (y)⟩ comp (C) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (C) s (y)) a (x) \leftrightarrow \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x))$
93	50 92	sylan2b	$⊢ ((((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \land a \in \underset{x \in {Base}_{A}}{⨉} (r (x) Hom (C) s (x))) \to (\forall x \in {Base}_{A} \forall y \in {Base}_{A} \forall h \in (x Hom (A) y) a (y) (⟨r (x), r (y)⟩ comp (C) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (C) s (y)) a (x) \leftrightarrow \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x))$
94	45 93	rabeqbidva	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to \{a \in \underset{x \in {Base}_{A}}{⨉} (r (x) Hom (C) s (x)) \| \forall x \in {Base}_{A} \forall y \in {Base}_{A} \forall h \in (x Hom (A) y) a (y) (⟨r (x), r (y)⟩ comp (C) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (C) s (y)) a (x)\} = \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\}$
95		csbeq1a	$⊢ s = 1^{st} (g) \to \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\} = ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\}$
96	95	adantl	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\} = ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\}$
97	94 96	eqtrd	$⊢ (((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \land s = 1^{st} (g)) \to \{a \in \underset{x \in {Base}_{A}}{⨉} (r (x) Hom (C) s (x)) \| \forall x \in {Base}_{A} \forall y \in {Base}_{A} \forall h \in (x Hom (A) y) a (y) (⟨r (x), r (y)⟩ comp (C) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (C) s (y)) a (x)\} = ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\}$
98	15 17 18 97	csbiedf	$⊢ ((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \to ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{A}}{⨉} (r (x) Hom (C) s (x)) \| \forall x \in {Base}_{A} \forall y \in {Base}_{A} \forall h \in (x Hom (A) y) a (y) (⟨r (x), r (y)⟩ comp (C) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (C) s (y)) a (x)\} = ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\}$
99		csbeq1a	$⊢ r = 1^{st} (f) \to ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\} = ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\}$
100	99	adantl	$⊢ ((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \to ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\} = ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\}$
101	98 100	eqtrd	$⊢ ((φ \land (f \in (A Func C) \land g \in (A Func C))) \land r = 1^{st} (f)) \to ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{A}}{⨉} (r (x) Hom (C) s (x)) \| \forall x \in {Base}_{A} \forall y \in {Base}_{A} \forall h \in (x Hom (A) y) a (y) (⟨r (x), r (y)⟩ comp (C) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (C) s (y)) a (x)\} = ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\}$
102	11 13 14 101	csbiedf	$⊢ (φ \land (f \in (A Func C) \land g \in (A Func C))) \to ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{A}}{⨉} (r (x) Hom (C) s (x)) \| \forall x \in {Base}_{A} \forall y \in {Base}_{A} \forall h \in (x Hom (A) y) a (y) (⟨r (x), r (y)⟩ comp (C) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (C) s (y)) a (x)\} = ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\}$
103	9 10 102	mpoeq123dva	$⊢ φ \to (f \in (A Func C), g \in (A Func C) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{A}}{⨉} (r (x) Hom (C) s (x)) \| \forall x \in {Base}_{A} \forall y \in {Base}_{A} \forall h \in (x Hom (A) y) a (y) (⟨r (x), r (y)⟩ comp (C) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (C) s (y)) a (x)\}) = (f \in (B Func D), g \in (B Func D) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\})$
104		eqid	$⊢ A Nat C = A Nat C$
105	104 23 53 20 59	natfval	$⊢ A Nat C = (f \in (A Func C), g \in (A Func C) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{A}}{⨉} (r (x) Hom (C) s (x)) \| \forall x \in {Base}_{A} \forall y \in {Base}_{A} \forall h \in (x Hom (A) y) a (y) (⟨r (x), r (y)⟩ comp (C) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (C) s (y)) a (x)\})$
106		eqid	$⊢ B Nat D = B Nat D$
107		eqid	$⊢ {Base}_{B} = {Base}_{B}$
108	106 107 54 21 60	natfval	$⊢ B Nat D = (f \in (B Func D), g \in (B Func D) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{B}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{B} \forall y \in {Base}_{B} \forall h \in (x Hom (B) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\})$
109	103 105 108	3eqtr4g	$⊢ φ \to A Nat C = B Nat D$

Metamath Proof Explorer

Theorem natpropd

Proof