isfunc

Description: Value of the set of functors between two categories. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	isfunc.b	$⊢ B = {Base}_{D}$
	isfunc.c	$⊢ C = {Base}_{E}$
	isfunc.h	$⊢ H = Hom (D)$
	isfunc.j	$⊢ J = Hom (E)$
	isfunc.1	$⊢ \underset{˙}{1} = Id (D)$
	isfunc.i	$⊢ I = Id (E)$
	isfunc.x	$⊢ \underset{˙}{\cdot} = comp (D)$
	isfunc.o	$⊢ O = comp (E)$
	isfunc.d	$⊢ φ \to D \in Cat$
	isfunc.e	$⊢ φ \to E \in Cat$
Assertion	isfunc	$⊢ φ \to (F (D Func E) G \leftrightarrow (F : B ⟶ C \land G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x G x) (\underset{˙}{1} (x)) = I (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m))))$

Proof

Step	Hyp	Ref	Expression
1		isfunc.b	$⊢ B = {Base}_{D}$
2		isfunc.c	$⊢ C = {Base}_{E}$
3		isfunc.h	$⊢ H = Hom (D)$
4		isfunc.j	$⊢ J = Hom (E)$
5		isfunc.1	$⊢ \underset{˙}{1} = Id (D)$
6		isfunc.i	$⊢ I = Id (E)$
7		isfunc.x	$⊢ \underset{˙}{\cdot} = comp (D)$
8		isfunc.o	$⊢ O = comp (E)$
9		isfunc.d	$⊢ φ \to D \in Cat$
10		isfunc.e	$⊢ φ \to E \in Cat$
11		fvexd	$⊢ (d = D \land e = E) \to {Base}_{d} \in V$
12		simpl	$⊢ (d = D \land e = E) \to d = D$
13	12	fveq2d	$⊢ (d = D \land e = E) \to {Base}_{d} = {Base}_{D}$
14	13 1	eqtr4di	$⊢ (d = D \land e = E) \to {Base}_{d} = B$
15		simpr	$⊢ ((d = D \land e = E) \land b = B) \to b = B$
16		simplr	$⊢ ((d = D \land e = E) \land b = B) \to e = E$
17	16	fveq2d	$⊢ ((d = D \land e = E) \land b = B) \to {Base}_{e} = {Base}_{E}$
18	17 2	eqtr4di	$⊢ ((d = D \land e = E) \land b = B) \to {Base}_{e} = C$
19	15 18	feq23d	$⊢ ((d = D \land e = E) \land b = B) \to (f : b ⟶ {Base}_{e} \leftrightarrow f : B ⟶ C)$
20	2	fvexi	$⊢ C \in V$
21	1	fvexi	$⊢ B \in V$
22	20 21	elmap	$⊢ f \in (C^{B}) \leftrightarrow f : B ⟶ C$
23	19 22	bitr4di	$⊢ ((d = D \land e = E) \land b = B) \to (f : b ⟶ {Base}_{e} \leftrightarrow f \in (C^{B}))$
24	15	sqxpeqd	$⊢ ((d = D \land e = E) \land b = B) \to b \times b = B \times B$
25	24	ixpeq1d	$⊢ ((d = D \land e = E) \land b = B) \to \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (e) f (2^{nd} (z)))}^{Hom (d) (z)}) = \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) Hom (e) f (2^{nd} (z)))}^{Hom (d) (z)})$
26	16	fveq2d	$⊢ ((d = D \land e = E) \land b = B) \to Hom (e) = Hom (E)$
27	26 4	eqtr4di	$⊢ ((d = D \land e = E) \land b = B) \to Hom (e) = J$
28	27	oveqd	$⊢ ((d = D \land e = E) \land b = B) \to f (1^{st} (z)) Hom (e) f (2^{nd} (z)) = f (1^{st} (z)) J f (2^{nd} (z))$
29		simpll	$⊢ ((d = D \land e = E) \land b = B) \to d = D$
30	29	fveq2d	$⊢ ((d = D \land e = E) \land b = B) \to Hom (d) = Hom (D)$
31	30 3	eqtr4di	$⊢ ((d = D \land e = E) \land b = B) \to Hom (d) = H$
32	31	fveq1d	$⊢ ((d = D \land e = E) \land b = B) \to Hom (d) (z) = H (z)$
33	28 32	oveq12d	$⊢ ((d = D \land e = E) \land b = B) \to {(f (1^{st} (z)) Hom (e) f (2^{nd} (z)))}^{Hom (d) (z)} = {(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)}$
34	33	ixpeq2dv	$⊢ ((d = D \land e = E) \land b = B) \to \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) Hom (e) f (2^{nd} (z)))}^{Hom (d) (z)}) = \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})$
35	25 34	eqtrd	$⊢ ((d = D \land e = E) \land b = B) \to \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (e) f (2^{nd} (z)))}^{Hom (d) (z)}) = \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})$
36	35	eleq2d	$⊢ ((d = D \land e = E) \land b = B) \to (g \in \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (e) f (2^{nd} (z)))}^{Hom (d) (z)}) \leftrightarrow g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)}))$
37	29	fveq2d	$⊢ ((d = D \land e = E) \land b = B) \to Id (d) = Id (D)$
38	37 5	eqtr4di	$⊢ ((d = D \land e = E) \land b = B) \to Id (d) = \underset{˙}{1}$
39	38	fveq1d	$⊢ ((d = D \land e = E) \land b = B) \to Id (d) (x) = \underset{˙}{1} (x)$
40	39	fveq2d	$⊢ ((d = D \land e = E) \land b = B) \to (x g x) (Id (d) (x)) = (x g x) (\underset{˙}{1} (x))$
41	16	fveq2d	$⊢ ((d = D \land e = E) \land b = B) \to Id (e) = Id (E)$
42	41 6	eqtr4di	$⊢ ((d = D \land e = E) \land b = B) \to Id (e) = I$
43	42	fveq1d	$⊢ ((d = D \land e = E) \land b = B) \to Id (e) (f (x)) = I (f (x))$
44	40 43	eqeq12d	$⊢ ((d = D \land e = E) \land b = B) \to ((x g x) (Id (d) (x)) = Id (e) (f (x)) \leftrightarrow (x g x) (\underset{˙}{1} (x)) = I (f (x)))$
45	31	oveqd	$⊢ ((d = D \land e = E) \land b = B) \to x Hom (d) y = x H y$
46	31	oveqd	$⊢ ((d = D \land e = E) \land b = B) \to y Hom (d) z = y H z$
47	29	fveq2d	$⊢ ((d = D \land e = E) \land b = B) \to comp (d) = comp (D)$
48	47 7	eqtr4di	$⊢ ((d = D \land e = E) \land b = B) \to comp (d) = \underset{˙}{\cdot}$
49	48	oveqd	$⊢ ((d = D \land e = E) \land b = B) \to ⟨x, y⟩ comp (d) z = ⟨x, y⟩ \underset{˙}{\cdot} z$
50	49	oveqd	$⊢ ((d = D \land e = E) \land b = B) \to n (⟨x, y⟩ comp (d) z) m = n (⟨x, y⟩ \underset{˙}{\cdot} z) m$
51	50	fveq2d	$⊢ ((d = D \land e = E) \land b = B) \to (x g z) (n (⟨x, y⟩ comp (d) z) m) = (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m)$
52	16	fveq2d	$⊢ ((d = D \land e = E) \land b = B) \to comp (e) = comp (E)$
53	52 8	eqtr4di	$⊢ ((d = D \land e = E) \land b = B) \to comp (e) = O$
54	53	oveqd	$⊢ ((d = D \land e = E) \land b = B) \to ⟨f (x), f (y)⟩ comp (e) f (z) = ⟨f (x), f (y)⟩ O f (z)$
55	54	oveqd	$⊢ ((d = D \land e = E) \land b = B) \to (y g z) (n) (⟨f (x), f (y)⟩ comp (e) f (z)) (x g y) (m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)$
56	51 55	eqeq12d	$⊢ ((d = D \land e = E) \land b = B) \to ((x g z) (n (⟨x, y⟩ comp (d) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (e) f (z)) (x g y) (m) \leftrightarrow (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m))$
57	46 56	raleqbidv	$⊢ ((d = D \land e = E) \land b = B) \to (\forall n \in (y Hom (d) z) (x g z) (n (⟨x, y⟩ comp (d) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (e) f (z)) (x g y) (m) \leftrightarrow \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m))$
58	45 57	raleqbidv	$⊢ ((d = D \land e = E) \land b = B) \to (\forall m \in (x Hom (d) y) \forall n \in (y Hom (d) z) (x g z) (n (⟨x, y⟩ comp (d) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (e) f (z)) (x g y) (m) \leftrightarrow \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m))$
59	15 58	raleqbidv	$⊢ ((d = D \land e = E) \land b = B) \to (\forall z \in b \forall m \in (x Hom (d) y) \forall n \in (y Hom (d) z) (x g z) (n (⟨x, y⟩ comp (d) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (e) f (z)) (x g y) (m) \leftrightarrow \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m))$
60	15 59	raleqbidv	$⊢ ((d = D \land e = E) \land b = B) \to (\forall y \in b \forall z \in b \forall m \in (x Hom (d) y) \forall n \in (y Hom (d) z) (x g z) (n (⟨x, y⟩ comp (d) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (e) f (z)) (x g y) (m) \leftrightarrow \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m))$
61	44 60	anbi12d	$⊢ ((d = D \land e = E) \land b = B) \to (((x g x) (Id (d) (x)) = Id (e) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (d) y) \forall n \in (y Hom (d) z) (x g z) (n (⟨x, y⟩ comp (d) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (e) f (z)) (x g y) (m)) \leftrightarrow ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))$
62	15 61	raleqbidv	$⊢ ((d = D \land e = E) \land b = B) \to (\forall x \in b ((x g x) (Id (d) (x)) = Id (e) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (d) y) \forall n \in (y Hom (d) z) (x g z) (n (⟨x, y⟩ comp (d) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (e) f (z)) (x g y) (m)) \leftrightarrow \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))$
63	23 36 62	3anbi123d	$⊢ ((d = D \land e = E) \land b = B) \to ((f : b ⟶ {Base}_{e} \land g \in \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (e) f (2^{nd} (z)))}^{Hom (d) (z)}) \land \forall x \in b ((x g x) (Id (d) (x)) = Id (e) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (d) y) \forall n \in (y Hom (d) z) (x g z) (n (⟨x, y⟩ comp (d) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (e) f (z)) (x g y) (m))) \leftrightarrow (f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m))))$
64		df-3an	$⊢ (f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m))) \leftrightarrow ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))$
65	63 64	bitrdi	$⊢ ((d = D \land e = E) \land b = B) \to ((f : b ⟶ {Base}_{e} \land g \in \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (e) f (2^{nd} (z)))}^{Hom (d) (z)}) \land \forall x \in b ((x g x) (Id (d) (x)) = Id (e) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (d) y) \forall n \in (y Hom (d) z) (x g z) (n (⟨x, y⟩ comp (d) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (e) f (z)) (x g y) (m))) \leftrightarrow ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m))))$
66	11 14 65	sbcied2	$⊢ (d = D \land e = E) \to (\underset{˙}{[} {Base}_{d} / b \underset{˙}{]} (f : b ⟶ {Base}_{e} \land g \in \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (e) f (2^{nd} (z)))}^{Hom (d) (z)}) \land \forall x \in b ((x g x) (Id (d) (x)) = Id (e) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (d) y) \forall n \in (y Hom (d) z) (x g z) (n (⟨x, y⟩ comp (d) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (e) f (z)) (x g y) (m))) \leftrightarrow ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m))))$
67	66	opabbidv	$⊢ (d = D \land e = E) \to \{⟨f, g⟩ \| \underset{˙}{[} {Base}_{d} / b \underset{˙}{]} (f : b ⟶ {Base}_{e} \land g \in \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (e) f (2^{nd} (z)))}^{Hom (d) (z)}) \land \forall x \in b ((x g x) (Id (d) (x)) = Id (e) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (d) y) \forall n \in (y Hom (d) z) (x g z) (n (⟨x, y⟩ comp (d) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (e) f (z)) (x g y) (m)))\} = \{⟨f, g⟩ \| ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))\}$
68		df-func	$⊢ Func = (d \in Cat, e \in Cat ⟼ \{⟨f, g⟩ \| \underset{˙}{[} {Base}_{d} / b \underset{˙}{]} (f : b ⟶ {Base}_{e} \land g \in \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (e) f (2^{nd} (z)))}^{Hom (d) (z)}) \land \forall x \in b ((x g x) (Id (d) (x)) = Id (e) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (d) y) \forall n \in (y Hom (d) z) (x g z) (n (⟨x, y⟩ comp (d) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (e) f (z)) (x g y) (m)))\})$
69		ovex	$⊢ C^{B} \in V$
70		snex	$⊢ \{f\} \in V$
71		ovex	$⊢ {(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)} \in V$
72	71	rgenw	$⊢ \forall z \in (B \times B) {(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)} \in V$
73		ixpexg	$⊢ \forall z \in (B \times B) {(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)} \in V \to \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)}) \in V$
74	72 73	ax-mp	$⊢ \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)}) \in V$
75	70 74	xpex	$⊢ \{f\} \times \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)}) \in V$
76	69 75	iunex	$⊢ ⋃_{f \in C^{B}} (\{f\} \times \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \in V$
77		simpl	$⊢ ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m))) \to (f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)}))$
78	77	anim2i	$⊢ (d = ⟨f, g⟩ \land ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))) \to (d = ⟨f, g⟩ \land (f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})))$
79	78	2eximi	$⊢ \exists f \exists g (d = ⟨f, g⟩ \land ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))) \to \exists f \exists g (d = ⟨f, g⟩ \land (f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})))$
80		elopab	$⊢ d \in \{⟨f, g⟩ \| ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))\} \leftrightarrow \exists f \exists g (d = ⟨f, g⟩ \land ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m))))$
81		eliunxp	$⊢ d \in ⋃_{f \in C^{B}} (\{f\} \times \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \leftrightarrow \exists f \exists g (d = ⟨f, g⟩ \land (f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})))$
82	79 80 81	3imtr4i	$⊢ d \in \{⟨f, g⟩ \| ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))\} \to d \in ⋃_{f \in C^{B}} (\{f\} \times \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)}))$
83	82	ssriv	$⊢ \{⟨f, g⟩ \| ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))\} \subseteq ⋃_{f \in C^{B}} (\{f\} \times \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)}))$
84	76 83	ssexi	$⊢ \{⟨f, g⟩ \| ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))\} \in V$
85	67 68 84	ovmpoa	$⊢ (D \in Cat \land E \in Cat) \to D Func E = \{⟨f, g⟩ \| ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))\}$
86	9 10 85	syl2anc	$⊢ φ \to D Func E = \{⟨f, g⟩ \| ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))\}$
87	86	breqd	$⊢ φ \to (F (D Func E) G \leftrightarrow F \{⟨f, g⟩ \| ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))\} G)$
88		brabv	$⊢ F \{⟨f, g⟩ \| ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))\} G \to (F \in V \land G \in V)$
89		elex	$⊢ F \in (C^{B}) \to F \in V$
90		elex	$⊢ G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \to G \in V$
91	89 90	anim12i	$⊢ (F \in (C^{B}) \land G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)})) \to (F \in V \land G \in V)$
92	91	3adant3	$⊢ (F \in (C^{B}) \land G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x G x) (\underset{˙}{1} (x)) = I (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m))) \to (F \in V \land G \in V)$
93		simpl	$⊢ (f = F \land g = G) \to f = F$
94	93	eleq1d	$⊢ (f = F \land g = G) \to (f \in (C^{B}) \leftrightarrow F \in (C^{B}))$
95		simpr	$⊢ (f = F \land g = G) \to g = G$
96	93	fveq1d	$⊢ (f = F \land g = G) \to f (1^{st} (z)) = F (1^{st} (z))$
97	93	fveq1d	$⊢ (f = F \land g = G) \to f (2^{nd} (z)) = F (2^{nd} (z))$
98	96 97	oveq12d	$⊢ (f = F \land g = G) \to f (1^{st} (z)) J f (2^{nd} (z)) = F (1^{st} (z)) J F (2^{nd} (z))$
99	98	oveq1d	$⊢ (f = F \land g = G) \to {(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)} = {(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}$
100	99	ixpeq2dv	$⊢ (f = F \land g = G) \to \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)}) = \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)})$
101	95 100	eleq12d	$⊢ (f = F \land g = G) \to (g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)}) \leftrightarrow G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}))$
102	95	oveqd	$⊢ (f = F \land g = G) \to x g x = x G x$
103	102	fveq1d	$⊢ (f = F \land g = G) \to (x g x) (\underset{˙}{1} (x)) = (x G x) (\underset{˙}{1} (x))$
104	93	fveq1d	$⊢ (f = F \land g = G) \to f (x) = F (x)$
105	104	fveq2d	$⊢ (f = F \land g = G) \to I (f (x)) = I (F (x))$
106	103 105	eqeq12d	$⊢ (f = F \land g = G) \to ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \leftrightarrow (x G x) (\underset{˙}{1} (x)) = I (F (x)))$
107	95	oveqd	$⊢ (f = F \land g = G) \to x g z = x G z$
108	107	fveq1d	$⊢ (f = F \land g = G) \to (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m)$
109	93	fveq1d	$⊢ (f = F \land g = G) \to f (y) = F (y)$
110	104 109	opeq12d	$⊢ (f = F \land g = G) \to ⟨f (x), f (y)⟩ = ⟨F (x), F (y)⟩$
111	93	fveq1d	$⊢ (f = F \land g = G) \to f (z) = F (z)$
112	110 111	oveq12d	$⊢ (f = F \land g = G) \to ⟨f (x), f (y)⟩ O f (z) = ⟨F (x), F (y)⟩ O F (z)$
113	95	oveqd	$⊢ (f = F \land g = G) \to y g z = y G z$
114	113	fveq1d	$⊢ (f = F \land g = G) \to (y g z) (n) = (y G z) (n)$
115	95	oveqd	$⊢ (f = F \land g = G) \to x g y = x G y$
116	115	fveq1d	$⊢ (f = F \land g = G) \to (x g y) (m) = (x G y) (m)$
117	112 114 116	oveq123d	$⊢ (f = F \land g = G) \to (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m)$
118	108 117	eqeq12d	$⊢ (f = F \land g = G) \to ((x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m) \leftrightarrow (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m))$
119	118	2ralbidv	$⊢ (f = F \land g = G) \to (\forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m) \leftrightarrow \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m))$
120	119	2ralbidv	$⊢ (f = F \land g = G) \to (\forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m) \leftrightarrow \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m))$
121	106 120	anbi12d	$⊢ (f = F \land g = G) \to (((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)) \leftrightarrow ((x G x) (\underset{˙}{1} (x)) = I (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m)))$
122	121	ralbidv	$⊢ (f = F \land g = G) \to (\forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)) \leftrightarrow \forall x \in B ((x G x) (\underset{˙}{1} (x)) = I (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m)))$
123	94 101 122	3anbi123d	$⊢ (f = F \land g = G) \to ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m))) \leftrightarrow (F \in (C^{B}) \land G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x G x) (\underset{˙}{1} (x)) = I (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m))))$
124	64 123	bitr3id	$⊢ (f = F \land g = G) \to (((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m))) \leftrightarrow (F \in (C^{B}) \land G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x G x) (\underset{˙}{1} (x)) = I (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m))))$
125		eqid	$⊢ \{⟨f, g⟩ \| ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))\} = \{⟨f, g⟩ \| ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))\}$
126	124 125	brabga	$⊢ (F \in V \land G \in V) \to (F \{⟨f, g⟩ \| ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))\} G \leftrightarrow (F \in (C^{B}) \land G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x G x) (\underset{˙}{1} (x)) = I (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m))))$
127	88 92 126	pm5.21nii	$⊢ F \{⟨f, g⟩ \| ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))\} G \leftrightarrow (F \in (C^{B}) \land G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x G x) (\underset{˙}{1} (x)) = I (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m)))$
128	20 21	elmap	$⊢ F \in (C^{B}) \leftrightarrow F : B ⟶ C$
129	128	3anbi1i	$⊢ (F \in (C^{B}) \land G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x G x) (\underset{˙}{1} (x)) = I (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m))) \leftrightarrow (F : B ⟶ C \land G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x G x) (\underset{˙}{1} (x)) = I (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m)))$
130	127 129	bitri	$⊢ F \{⟨f, g⟩ \| ((f \in (C^{B}) \land g \in \underset{z \in B \times B}{⨉} ({(f (1^{st} (z)) J f (2^{nd} (z)))}^{H (z)})) \land \forall x \in B ((x g x) (\underset{˙}{1} (x)) = I (f (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x g z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y g z) (n) (⟨f (x), f (y)⟩ O f (z)) (x g y) (m)))\} G \leftrightarrow (F : B ⟶ C \land G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x G x) (\underset{˙}{1} (x)) = I (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m)))$
131	87 130	bitrdi	$⊢ φ \to (F (D Func E) G \leftrightarrow (F : B ⟶ C \land G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \land \forall x \in B ((x G x) (\underset{˙}{1} (x)) = I (F (x)) \land \forall y \in B \forall z \in B \forall m \in (x H y) \forall n \in (y H z) (x G z) (n (⟨x, y⟩ \underset{˙}{\cdot} z) m) = (y G z) (n) (⟨F (x), F (y)⟩ O F (z)) (x G y) (m))))$

Metamath Proof Explorer

Theorem isfunc

Proof