isfuncd

Description: Deduce that an operation is a functor of categories. (Contributed by Mario Carneiro, 4-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$
	isfuncd.1	$⊢ φ \to F : B ⟶ C$
	isfuncd.2	$⊢ φ \to G Fn (B \times B)$
	isfuncd.3	$⊢ (φ \land (x \in B \land y \in B)) \to (x G y) : x H y ⟶ F (x) J F (y)$
	isfuncd.4	$⊢ (φ \land x \in B) \to (x G x) (\underset{˙}{1} (x)) = I (F (x))$
	isfuncd.5	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \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)$
Assertion	isfuncd	$⊢ φ \to F (D Func E) G$

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		isfuncd.1	$⊢ φ \to F : B ⟶ C$
12		isfuncd.2	$⊢ φ \to G Fn (B \times B)$
13		isfuncd.3	$⊢ (φ \land (x \in B \land y \in B)) \to (x G y) : x H y ⟶ F (x) J F (y)$
14		isfuncd.4	$⊢ (φ \land x \in B) \to (x G x) (\underset{˙}{1} (x)) = I (F (x))$
15		isfuncd.5	$⊢ (φ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \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)$
16	1	fvexi	$⊢ B \in V$
17	16 16	xpex	$⊢ B \times B \in V$
18		fnex	$⊢ (G Fn (B \times B) \land B \times B \in V) \to G \in V$
19	12 17 18	sylancl	$⊢ φ \to G \in V$
20		ovex	$⊢ F (x) J F (y) \in V$
21		ovex	$⊢ x H y \in V$
22	20 21	elmap	$⊢ x G y \in ({(F (x) J F (y))}^{(x H y)}) \leftrightarrow (x G y) : x H y ⟶ F (x) J F (y)$
23	13 22	sylibr	$⊢ (φ \land (x \in B \land y \in B)) \to x G y \in ({(F (x) J F (y))}^{(x H y)})$
24	23	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B x G y \in ({(F (x) J F (y))}^{(x H y)})$
25		fveq2	$⊢ z = ⟨x, y⟩ \to G (z) = G (⟨x, y⟩)$
26		df-ov	$⊢ x G y = G (⟨x, y⟩)$
27	25 26	eqtr4di	$⊢ z = ⟨x, y⟩ \to G (z) = x G y$
28		vex	$⊢ x \in V$
29		vex	$⊢ y \in V$
30	28 29	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
31	30	fveq2d	$⊢ z = ⟨x, y⟩ \to F (1^{st} (z)) = F (x)$
32	28 29	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
33	32	fveq2d	$⊢ z = ⟨x, y⟩ \to F (2^{nd} (z)) = F (y)$
34	31 33	oveq12d	$⊢ z = ⟨x, y⟩ \to F (1^{st} (z)) J F (2^{nd} (z)) = F (x) J F (y)$
35		fveq2	$⊢ z = ⟨x, y⟩ \to H (z) = H (⟨x, y⟩)$
36		df-ov	$⊢ x H y = H (⟨x, y⟩)$
37	35 36	eqtr4di	$⊢ z = ⟨x, y⟩ \to H (z) = x H y$
38	34 37	oveq12d	$⊢ z = ⟨x, y⟩ \to {(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)} = {(F (x) J F (y))}^{(x H y)}$
39	27 38	eleq12d	$⊢ z = ⟨x, y⟩ \to (G (z) \in ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \leftrightarrow x G y \in ({(F (x) J F (y))}^{(x H y)}))$
40	39	ralxp	$⊢ \forall z \in (B \times B) G (z) \in ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \leftrightarrow \forall x \in B \forall y \in B x G y \in ({(F (x) J F (y))}^{(x H y)})$
41	24 40	sylibr	$⊢ φ \to \forall z \in (B \times B) G (z) \in ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)})$
42		elixp2	$⊢ G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}) \leftrightarrow (G \in V \land G Fn (B \times B) \land \forall z \in (B \times B) G (z) \in ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)}))$
43	19 12 41 42	syl3anbrc	$⊢ φ \to G \in \underset{z \in B \times B}{⨉} ({(F (1^{st} (z)) J F (2^{nd} (z)))}^{H (z)})$
44	15	3expia	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to ((m \in (x H y) \land n \in (y H z)) \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))$
45	44	3exp2	$⊢ φ \to (x \in B \to (y \in B \to (z \in B \to ((m \in (x H y) \land n \in (y H z)) \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)))))$
46	45	imp43	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to ((m \in (x H y) \land n \in (y H z)) \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))$
47	46	ralrimivv	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \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)$
48	47	ralrimivva	$⊢ (φ \land x \in B) \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)$
49	14 48	jca	$⊢ (φ \land x \in B) \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))$
50	49	ralrimiva	$⊢ φ \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))$
51	1 2 3 4 5 6 7 8 9 10	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))))$
52	11 43 50 51	mpbir3and	$⊢ φ \to F (D Func E) G$

Metamath Proof Explorer

Theorem isfuncd

Proof