funcpropd

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

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

Proof

Step	Hyp	Ref	Expression
1		funcpropd.1	$⊢ φ \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
2		funcpropd.2	$⊢ φ \to {comp}_{𝑓} (A) = {comp}_{𝑓} (B)$
3		funcpropd.3	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
4		funcpropd.4	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
5		funcpropd.a	$⊢ φ \to A \in V$
6		funcpropd.b	$⊢ φ \to B \in V$
7		funcpropd.c	$⊢ φ \to C \in V$
8		funcpropd.d	$⊢ φ \to D \in V$
9		relfunc	$⊢ Rel (A Func C)$
10		relfunc	$⊢ Rel (B Func D)$
11	1 2 5 6	catpropd	$⊢ φ \to (A \in Cat \leftrightarrow B \in Cat)$
12	3 4 7 8	catpropd	$⊢ φ \to (C \in Cat \leftrightarrow D \in Cat)$
13	11 12	anbi12d	$⊢ φ \to ((A \in Cat \land C \in Cat) \leftrightarrow (B \in Cat \land D \in Cat))$
14		2fveq3	$⊢ z = w \to f (1^{st} (z)) = f (1^{st} (w))$
15		2fveq3	$⊢ z = w \to f (2^{nd} (z)) = f (2^{nd} (w))$
16	14 15	oveq12d	$⊢ z = w \to f (1^{st} (z)) Hom (C) f (2^{nd} (z)) = f (1^{st} (w)) Hom (C) f (2^{nd} (w))$
17		fveq2	$⊢ z = w \to Hom (A) (z) = Hom (A) (w)$
18	16 17	oveq12d	$⊢ z = w \to {(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)} = {(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}$
19	18	cbvixpv	$⊢ \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)}) = \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)})$
20	19	eleq2i	$⊢ g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)}) \leftrightarrow g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)})$
21	20	anbi2i	$⊢ (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)})) \leftrightarrow (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))$
22	1	ad2antrr	$⊢ ((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
23	2	ad2antrr	$⊢ ((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \to {comp}_{𝑓} (A) = {comp}_{𝑓} (B)$
24	5	ad2antrr	$⊢ ((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \to A \in V$
25	6	ad2antrr	$⊢ ((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \to B \in V$
26	22 23 24 25	cidpropd	$⊢ ((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \to Id (A) = Id (B)$
27	26	fveq1d	$⊢ ((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \to Id (A) (x) = Id (B) (x)$
28	27	fveq2d	$⊢ ((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \to (x g x) (Id (A) (x)) = (x g x) (Id (B) (x))$
29	3 4 7 8	cidpropd	$⊢ φ \to Id (C) = Id (D)$
30	29	ad2antrr	$⊢ ((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \to Id (C) = Id (D)$
31	30	fveq1d	$⊢ ((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \to Id (C) (f (x)) = Id (D) (f (x))$
32	28 31	eqeq12d	$⊢ ((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \to ((x g x) (Id (A) (x)) = Id (C) (f (x)) \leftrightarrow (x g x) (Id (B) (x)) = Id (D) (f (x)))$
33		eqid	$⊢ {Base}_{A} = {Base}_{A}$
34		eqid	$⊢ Hom (A) = Hom (A)$
35		eqid	$⊢ comp (A) = comp (A)$
36		eqid	$⊢ comp (B) = comp (B)$
37	1	ad6antr	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
38	2	ad6antr	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to {comp}_{𝑓} (A) = {comp}_{𝑓} (B)$
39		simp-5r	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to x \in {Base}_{A}$
40		simp-4r	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to y \in {Base}_{A}$
41		simpllr	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to z \in {Base}_{A}$
42		simplr	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to m \in (x Hom (A) y)$
43		simpr	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to n \in (y Hom (A) z)$
44	33 34 35 36 37 38 39 40 41 42 43	comfeqval	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to n (⟨x, y⟩ comp (A) z) m = n (⟨x, y⟩ comp (B) z) m$
45	44	fveq2d	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to (x g z) (n (⟨x, y⟩ comp (A) z) m) = (x g z) (n (⟨x, y⟩ comp (B) z) m)$
46		eqid	$⊢ {Base}_{C} = {Base}_{C}$
47		eqid	$⊢ Hom (C) = Hom (C)$
48		eqid	$⊢ comp (C) = comp (C)$
49		eqid	$⊢ comp (D) = comp (D)$
50	3	ad6antr	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
51	4	ad6antr	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
52		simprl	$⊢ (φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \to f : {Base}_{A} ⟶ {Base}_{C}$
53	52	ad5antr	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to f : {Base}_{A} ⟶ {Base}_{C}$
54	53 39	ffvelcdmd	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to f (x) \in {Base}_{C}$
55	53 40	ffvelcdmd	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to f (y) \in {Base}_{C}$
56	53 41	ffvelcdmd	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to f (z) \in {Base}_{C}$
57		df-ov	$⊢ x g y = g (⟨x, y⟩)$
58		simprr	$⊢ (φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \to g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)})$
59	58	ad3antrrr	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)})$
60	59	adantr	$⊢ (((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \to g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)})$
61		opelxpi	$⊢ (x \in {Base}_{A} \land y \in {Base}_{A}) \to ⟨x, y⟩ \in ({Base}_{A} \times {Base}_{A})$
62	61	ad5ant23	$⊢ (((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \to ⟨x, y⟩ \in ({Base}_{A} \times {Base}_{A})$
63		vex	$⊢ x \in V$
64		vex	$⊢ y \in V$
65	63 64	op1std	$⊢ w = ⟨x, y⟩ \to 1^{st} (w) = x$
66	65	fveq2d	$⊢ w = ⟨x, y⟩ \to f (1^{st} (w)) = f (x)$
67	63 64	op2ndd	$⊢ w = ⟨x, y⟩ \to 2^{nd} (w) = y$
68	67	fveq2d	$⊢ w = ⟨x, y⟩ \to f (2^{nd} (w)) = f (y)$
69	66 68	oveq12d	$⊢ w = ⟨x, y⟩ \to f (1^{st} (w)) Hom (C) f (2^{nd} (w)) = f (x) Hom (C) f (y)$
70		fveq2	$⊢ w = ⟨x, y⟩ \to Hom (A) (w) = Hom (A) (⟨x, y⟩)$
71		df-ov	$⊢ x Hom (A) y = Hom (A) (⟨x, y⟩)$
72	70 71	eqtr4di	$⊢ w = ⟨x, y⟩ \to Hom (A) (w) = x Hom (A) y$
73	69 72	oveq12d	$⊢ w = ⟨x, y⟩ \to {(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)} = {(f (x) Hom (C) f (y))}^{(x Hom (A) y)}$
74	73	fvixp	$⊢ (g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}) \land ⟨x, y⟩ \in ({Base}_{A} \times {Base}_{A})) \to g (⟨x, y⟩) \in ({(f (x) Hom (C) f (y))}^{(x Hom (A) y)})$
75	60 62 74	syl2anc	$⊢ (((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \to g (⟨x, y⟩) \in ({(f (x) Hom (C) f (y))}^{(x Hom (A) y)})$
76	57 75	eqeltrid	$⊢ (((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \to x g y \in ({(f (x) Hom (C) f (y))}^{(x Hom (A) y)})$
77		elmapi	$⊢ x g y \in ({(f (x) Hom (C) f (y))}^{(x Hom (A) y)}) \to (x g y) : x Hom (A) y ⟶ f (x) Hom (C) f (y)$
78	76 77	syl	$⊢ (((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \to (x g y) : x Hom (A) y ⟶ f (x) Hom (C) f (y)$
79	78	adantr	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to (x g y) : x Hom (A) y ⟶ f (x) Hom (C) f (y)$
80	79 42	ffvelcdmd	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to (x g y) (m) \in (f (x) Hom (C) f (y))$
81		df-ov	$⊢ y g z = g (⟨y, z⟩)$
82		opelxpi	$⊢ (y \in {Base}_{A} \land z \in {Base}_{A}) \to ⟨y, z⟩ \in ({Base}_{A} \times {Base}_{A})$
83	82	adantll	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to ⟨y, z⟩ \in ({Base}_{A} \times {Base}_{A})$
84		vex	$⊢ z \in V$
85	64 84	op1std	$⊢ w = ⟨y, z⟩ \to 1^{st} (w) = y$
86	85	fveq2d	$⊢ w = ⟨y, z⟩ \to f (1^{st} (w)) = f (y)$
87	64 84	op2ndd	$⊢ w = ⟨y, z⟩ \to 2^{nd} (w) = z$
88	87	fveq2d	$⊢ w = ⟨y, z⟩ \to f (2^{nd} (w)) = f (z)$
89	86 88	oveq12d	$⊢ w = ⟨y, z⟩ \to f (1^{st} (w)) Hom (C) f (2^{nd} (w)) = f (y) Hom (C) f (z)$
90		fveq2	$⊢ w = ⟨y, z⟩ \to Hom (A) (w) = Hom (A) (⟨y, z⟩)$
91		df-ov	$⊢ y Hom (A) z = Hom (A) (⟨y, z⟩)$
92	90 91	eqtr4di	$⊢ w = ⟨y, z⟩ \to Hom (A) (w) = y Hom (A) z$
93	89 92	oveq12d	$⊢ w = ⟨y, z⟩ \to {(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)} = {(f (y) Hom (C) f (z))}^{(y Hom (A) z)}$
94	93	fvixp	$⊢ (g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}) \land ⟨y, z⟩ \in ({Base}_{A} \times {Base}_{A})) \to g (⟨y, z⟩) \in ({(f (y) Hom (C) f (z))}^{(y Hom (A) z)})$
95	59 83 94	syl2anc	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to g (⟨y, z⟩) \in ({(f (y) Hom (C) f (z))}^{(y Hom (A) z)})$
96	81 95	eqeltrid	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to y g z \in ({(f (y) Hom (C) f (z))}^{(y Hom (A) z)})$
97		elmapi	$⊢ y g z \in ({(f (y) Hom (C) f (z))}^{(y Hom (A) z)}) \to (y g z) : y Hom (A) z ⟶ f (y) Hom (C) f (z)$
98	96 97	syl	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to (y g z) : y Hom (A) z ⟶ f (y) Hom (C) f (z)$
99	98	adantr	$⊢ (((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \to (y g z) : y Hom (A) z ⟶ f (y) Hom (C) f (z)$
100	99	ffvelcdmda	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to (y g z) (n) \in (f (y) Hom (C) f (z))$
101	46 47 48 49 50 51 54 55 56 80 100	comfeqval	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m)$
102	45 101	eqeq12d	$⊢ ((((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \land n \in (y Hom (A) z)) \to ((x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m) \leftrightarrow (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))$
103	102	ralbidva	$⊢ (((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \land m \in (x Hom (A) y)) \to (\forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m) \leftrightarrow \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))$
104	103	ralbidva	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to (\forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m) \leftrightarrow \forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))$
105		eqid	$⊢ Hom (B) = Hom (B)$
106	22	ad2antrr	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
107		simpllr	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to x \in {Base}_{A}$
108		simplr	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to y \in {Base}_{A}$
109	33 34 105 106 107 108	homfeqval	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to x Hom (A) y = x Hom (B) y$
110		simpr	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to z \in {Base}_{A}$
111	33 34 105 106 108 110	homfeqval	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to y Hom (A) z = y Hom (B) z$
112	111	raleqdv	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to (\forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m) \leftrightarrow \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))$
113	109 112	raleqbidv	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to (\forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m) \leftrightarrow \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))$
114	104 113	bitrd	$⊢ ((((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \land z \in {Base}_{A}) \to (\forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m) \leftrightarrow \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))$
115	114	ralbidva	$⊢ (((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \land y \in {Base}_{A}) \to (\forall z \in {Base}_{A} \forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m) \leftrightarrow \forall z \in {Base}_{A} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))$
116	115	ralbidva	$⊢ ((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \to (\forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m) \leftrightarrow \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))$
117	32 116	anbi12d	$⊢ ((φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \land x \in {Base}_{A}) \to (((x g x) (Id (A) (x)) = Id (C) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m)) \leftrightarrow ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m)))$
118	117	ralbidva	$⊢ (φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{w \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (w)) Hom (C) f (2^{nd} (w)))}^{Hom (A) (w)}))) \to (\forall x \in {Base}_{A} ((x g x) (Id (A) (x)) = Id (C) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m)) \leftrightarrow \forall x \in {Base}_{A} ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m)))$
119	21 118	sylan2b	$⊢ (φ \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)}))) \to (\forall x \in {Base}_{A} ((x g x) (Id (A) (x)) = Id (C) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m)) \leftrightarrow \forall x \in {Base}_{A} ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m)))$
120	119	pm5.32da	$⊢ φ \to (((f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)})) \land \forall x \in {Base}_{A} ((x g x) (Id (A) (x)) = Id (C) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m))) \leftrightarrow ((f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)})) \land \forall x \in {Base}_{A} ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))))$
121		eqid	$⊢ Hom (D) = Hom (D)$
122	3	ad2antrr	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
123		simplr	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to f : {Base}_{A} ⟶ {Base}_{C}$
124		xp1st	$⊢ z \in ({Base}_{A} \times {Base}_{A}) \to 1^{st} (z) \in {Base}_{A}$
125	124	adantl	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to 1^{st} (z) \in {Base}_{A}$
126	123 125	ffvelcdmd	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to f (1^{st} (z)) \in {Base}_{C}$
127		xp2nd	$⊢ z \in ({Base}_{A} \times {Base}_{A}) \to 2^{nd} (z) \in {Base}_{A}$
128	127	adantl	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to 2^{nd} (z) \in {Base}_{A}$
129	123 128	ffvelcdmd	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to f (2^{nd} (z)) \in {Base}_{C}$
130	46 47 121 122 126 129	homfeqval	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to f (1^{st} (z)) Hom (C) f (2^{nd} (z)) = f (1^{st} (z)) Hom (D) f (2^{nd} (z))$
131	1	ad2antrr	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
132	33 34 105 131 125 128	homfeqval	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to 1^{st} (z) Hom (A) 2^{nd} (z) = 1^{st} (z) Hom (B) 2^{nd} (z)$
133		df-ov	$⊢ 1^{st} (z) Hom (A) 2^{nd} (z) = Hom (A) (⟨1^{st} (z), 2^{nd} (z)⟩)$
134		df-ov	$⊢ 1^{st} (z) Hom (B) 2^{nd} (z) = Hom (B) (⟨1^{st} (z), 2^{nd} (z)⟩)$
135	132 133 134	3eqtr3g	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to Hom (A) (⟨1^{st} (z), 2^{nd} (z)⟩) = Hom (B) (⟨1^{st} (z), 2^{nd} (z)⟩)$
136		1st2nd2	$⊢ z \in ({Base}_{A} \times {Base}_{A}) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
137	136	adantl	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
138	137	fveq2d	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to Hom (A) (z) = Hom (A) (⟨1^{st} (z), 2^{nd} (z)⟩)$
139	137	fveq2d	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to Hom (B) (z) = Hom (B) (⟨1^{st} (z), 2^{nd} (z)⟩)$
140	135 138 139	3eqtr4d	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to Hom (A) (z) = Hom (B) (z)$
141	130 140	oveq12d	$⊢ ((φ \land f : {Base}_{A} ⟶ {Base}_{C}) \land z \in ({Base}_{A} \times {Base}_{A})) \to {(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)} = {(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)}$
142	141	ixpeq2dva	$⊢ (φ \land f : {Base}_{A} ⟶ {Base}_{C}) \to \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)}) = \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)})$
143	1	homfeqbas	$⊢ φ \to {Base}_{A} = {Base}_{B}$
144	143	sqxpeqd	$⊢ φ \to {Base}_{A} \times {Base}_{A} = {Base}_{B} \times {Base}_{B}$
145	144	adantr	$⊢ (φ \land f : {Base}_{A} ⟶ {Base}_{C}) \to {Base}_{A} \times {Base}_{A} = {Base}_{B} \times {Base}_{B}$
146	145	ixpeq1d	$⊢ (φ \land f : {Base}_{A} ⟶ {Base}_{C}) \to \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)}) = \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)})$
147	142 146	eqtrd	$⊢ (φ \land f : {Base}_{A} ⟶ {Base}_{C}) \to \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)}) = \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)})$
148	147	eleq2d	$⊢ (φ \land f : {Base}_{A} ⟶ {Base}_{C}) \to (g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)}) \leftrightarrow g \in \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)}))$
149	148	pm5.32da	$⊢ φ \to ((f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)})) \leftrightarrow (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)})))$
150	3	homfeqbas	$⊢ φ \to {Base}_{C} = {Base}_{D}$
151	143 150	feq23d	$⊢ φ \to (f : {Base}_{A} ⟶ {Base}_{C} \leftrightarrow f : {Base}_{B} ⟶ {Base}_{D})$
152	151	anbi1d	$⊢ φ \to ((f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)})) \leftrightarrow (f : {Base}_{B} ⟶ {Base}_{D} \land g \in \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)})))$
153	149 152	bitrd	$⊢ φ \to ((f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)})) \leftrightarrow (f : {Base}_{B} ⟶ {Base}_{D} \land g \in \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)})))$
154	143	adantr	$⊢ (φ \land x \in {Base}_{A}) \to {Base}_{A} = {Base}_{B}$
155	154	raleqdv	$⊢ (φ \land x \in {Base}_{A}) \to (\forall z \in {Base}_{A} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m) \leftrightarrow \forall z \in {Base}_{B} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))$
156	154 155	raleqbidv	$⊢ (φ \land x \in {Base}_{A}) \to (\forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m) \leftrightarrow \forall y \in {Base}_{B} \forall z \in {Base}_{B} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))$
157	156	anbi2d	$⊢ (φ \land x \in {Base}_{A}) \to (((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m)) \leftrightarrow ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{B} \forall z \in {Base}_{B} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m)))$
158	143 157	raleqbidva	$⊢ φ \to (\forall x \in {Base}_{A} ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m)) \leftrightarrow \forall x \in {Base}_{B} ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{B} \forall z \in {Base}_{B} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m)))$
159	153 158	anbi12d	$⊢ φ \to (((f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)})) \land \forall x \in {Base}_{A} ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))) \leftrightarrow ((f : {Base}_{B} ⟶ {Base}_{D} \land g \in \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)})) \land \forall x \in {Base}_{B} ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{B} \forall z \in {Base}_{B} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))))$
160	120 159	bitrd	$⊢ φ \to (((f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)})) \land \forall x \in {Base}_{A} ((x g x) (Id (A) (x)) = Id (C) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m))) \leftrightarrow ((f : {Base}_{B} ⟶ {Base}_{D} \land g \in \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)})) \land \forall x \in {Base}_{B} ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{B} \forall z \in {Base}_{B} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))))$
161		df-3an	$⊢ (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)}) \land \forall x \in {Base}_{A} ((x g x) (Id (A) (x)) = Id (C) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m))) \leftrightarrow ((f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)})) \land \forall x \in {Base}_{A} ((x g x) (Id (A) (x)) = Id (C) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m)))$
162		df-3an	$⊢ (f : {Base}_{B} ⟶ {Base}_{D} \land g \in \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)}) \land \forall x \in {Base}_{B} ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{B} \forall z \in {Base}_{B} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))) \leftrightarrow ((f : {Base}_{B} ⟶ {Base}_{D} \land g \in \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)})) \land \forall x \in {Base}_{B} ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{B} \forall z \in {Base}_{B} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m)))$
163	160 161 162	3bitr4g	$⊢ φ \to ((f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)}) \land \forall x \in {Base}_{A} ((x g x) (Id (A) (x)) = Id (C) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m))) \leftrightarrow (f : {Base}_{B} ⟶ {Base}_{D} \land g \in \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)}) \land \forall x \in {Base}_{B} ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{B} \forall z \in {Base}_{B} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))))$
164	13 163	anbi12d	$⊢ φ \to (((A \in Cat \land C \in Cat) \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)}) \land \forall x \in {Base}_{A} ((x g x) (Id (A) (x)) = Id (C) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m)))) \leftrightarrow ((B \in Cat \land D \in Cat) \land (f : {Base}_{B} ⟶ {Base}_{D} \land g \in \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)}) \land \forall x \in {Base}_{B} ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{B} \forall z \in {Base}_{B} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m)))))$
165		df-br	$⊢ f (A Func C) g \leftrightarrow ⟨f, g⟩ \in (A Func C)$
166		funcrcl	$⊢ ⟨f, g⟩ \in (A Func C) \to (A \in Cat \land C \in Cat)$
167	165 166	sylbi	$⊢ f (A Func C) g \to (A \in Cat \land C \in Cat)$
168		eqid	$⊢ Id (A) = Id (A)$
169		eqid	$⊢ Id (C) = Id (C)$
170		simpl	$⊢ (A \in Cat \land C \in Cat) \to A \in Cat$
171		simpr	$⊢ (A \in Cat \land C \in Cat) \to C \in Cat$
172	33 46 34 47 168 169 35 48 170 171	isfunc	$⊢ (A \in Cat \land C \in Cat) \to (f (A Func C) g \leftrightarrow (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)}) \land \forall x \in {Base}_{A} ((x g x) (Id (A) (x)) = Id (C) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m))))$
173	167 172	biadanii	$⊢ f (A Func C) g \leftrightarrow ((A \in Cat \land C \in Cat) \land (f : {Base}_{A} ⟶ {Base}_{C} \land g \in \underset{z \in {Base}_{A} \times {Base}_{A}}{⨉} ({(f (1^{st} (z)) Hom (C) f (2^{nd} (z)))}^{Hom (A) (z)}) \land \forall x \in {Base}_{A} ((x g x) (Id (A) (x)) = Id (C) (f (x)) \land \forall y \in {Base}_{A} \forall z \in {Base}_{A} \forall m \in (x Hom (A) y) \forall n \in (y Hom (A) z) (x g z) (n (⟨x, y⟩ comp (A) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (C) f (z)) (x g y) (m))))$
174		df-br	$⊢ f (B Func D) g \leftrightarrow ⟨f, g⟩ \in (B Func D)$
175		funcrcl	$⊢ ⟨f, g⟩ \in (B Func D) \to (B \in Cat \land D \in Cat)$
176	174 175	sylbi	$⊢ f (B Func D) g \to (B \in Cat \land D \in Cat)$
177		eqid	$⊢ {Base}_{B} = {Base}_{B}$
178		eqid	$⊢ {Base}_{D} = {Base}_{D}$
179		eqid	$⊢ Id (B) = Id (B)$
180		eqid	$⊢ Id (D) = Id (D)$
181		simpl	$⊢ (B \in Cat \land D \in Cat) \to B \in Cat$
182		simpr	$⊢ (B \in Cat \land D \in Cat) \to D \in Cat$
183	177 178 105 121 179 180 36 49 181 182	isfunc	$⊢ (B \in Cat \land D \in Cat) \to (f (B Func D) g \leftrightarrow (f : {Base}_{B} ⟶ {Base}_{D} \land g \in \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)}) \land \forall x \in {Base}_{B} ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{B} \forall z \in {Base}_{B} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))))$
184	176 183	biadanii	$⊢ f (B Func D) g \leftrightarrow ((B \in Cat \land D \in Cat) \land (f : {Base}_{B} ⟶ {Base}_{D} \land g \in \underset{z \in {Base}_{B} \times {Base}_{B}}{⨉} ({(f (1^{st} (z)) Hom (D) f (2^{nd} (z)))}^{Hom (B) (z)}) \land \forall x \in {Base}_{B} ((x g x) (Id (B) (x)) = Id (D) (f (x)) \land \forall y \in {Base}_{B} \forall z \in {Base}_{B} \forall m \in (x Hom (B) y) \forall n \in (y Hom (B) z) (x g z) (n (⟨x, y⟩ comp (B) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (D) f (z)) (x g y) (m))))$
185	164 173 184	3bitr4g	$⊢ φ \to (f (A Func C) g \leftrightarrow f (B Func D) g)$
186	9 10 185	eqbrrdiv	$⊢ φ \to A Func C = B Func D$

Metamath Proof Explorer

Theorem funcpropd

Proof