fuccocl

Description: The composition of two natural transformations is a natural transformation. Remark 6.14(a) in Adamek p. 87. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fuccocl.q	$⊢ Q = C FuncCat D$
	fuccocl.n	$⊢ N = C Nat D$
	fuccocl.x	$⊢ \underset{˙}{∙} = comp (Q)$
	fuccocl.r	$⊢ φ \to R \in (F N G)$
	fuccocl.s	$⊢ φ \to S \in (G N H)$
Assertion	fuccocl	$⊢ φ \to S (⟨F, G⟩ \underset{˙}{∙} H) R \in (F N H)$

Proof

Step	Hyp	Ref	Expression
1		fuccocl.q	$⊢ Q = C FuncCat D$
2		fuccocl.n	$⊢ N = C Nat D$
3		fuccocl.x	$⊢ \underset{˙}{∙} = comp (Q)$
4		fuccocl.r	$⊢ φ \to R \in (F N G)$
5		fuccocl.s	$⊢ φ \to S \in (G N H)$
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7		eqid	$⊢ comp (D) = comp (D)$
8	1 2 6 7 3 4 5	fucco	$⊢ φ \to S (⟨F, G⟩ \underset{˙}{∙} H) R = (x \in {Base}_{C} ⟼ S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x))$
9		eqid	$⊢ {Base}_{D} = {Base}_{D}$
10		eqid	$⊢ Hom (D) = Hom (D)$
11	2	natrcl	$⊢ R \in (F N G) \to (F \in (C Func D) \land G \in (C Func D))$
12	4 11	syl	$⊢ φ \to (F \in (C Func D) \land G \in (C Func D))$
13	12	simpld	$⊢ φ \to F \in (C Func D)$
14		funcrcl	$⊢ F \in (C Func D) \to (C \in Cat \land D \in Cat)$
15	13 14	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
16	15	simprd	$⊢ φ \to D \in Cat$
17	16	adantr	$⊢ (φ \land x \in {Base}_{C}) \to D \in Cat$
18		relfunc	$⊢ Rel (C Func D)$
19		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
20	18 13 19	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
21	6 9 20	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
22	21	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (x) \in {Base}_{D}$
23	2	natrcl	$⊢ S \in (G N H) \to (G \in (C Func D) \land H \in (C Func D))$
24	5 23	syl	$⊢ φ \to (G \in (C Func D) \land H \in (C Func D))$
25	24	simpld	$⊢ φ \to G \in (C Func D)$
26		1st2ndbr	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
27	18 25 26	sylancr	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
28	6 9 27	funcf1	$⊢ φ \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
29	28	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G) (x) \in {Base}_{D}$
30	24	simprd	$⊢ φ \to H \in (C Func D)$
31		1st2ndbr	$⊢ (Rel (C Func D) \land H \in (C Func D)) \to 1^{st} (H) (C Func D) 2^{nd} (H)$
32	18 30 31	sylancr	$⊢ φ \to 1^{st} (H) (C Func D) 2^{nd} (H)$
33	6 9 32	funcf1	$⊢ φ \to 1^{st} (H) : {Base}_{C} ⟶ {Base}_{D}$
34	33	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (H) (x) \in {Base}_{D}$
35	2 4	nat1st2nd	$⊢ φ \to R \in (⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩)$
36	35	adantr	$⊢ (φ \land x \in {Base}_{C}) \to R \in (⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩)$
37		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
38	2 36 6 10 37	natcl	$⊢ (φ \land x \in {Base}_{C}) \to R (x) \in (1^{st} (F) (x) Hom (D) 1^{st} (G) (x))$
39	2 5	nat1st2nd	$⊢ φ \to S \in (⟨1^{st} (G), 2^{nd} (G)⟩ N ⟨1^{st} (H), 2^{nd} (H)⟩)$
40	39	adantr	$⊢ (φ \land x \in {Base}_{C}) \to S \in (⟨1^{st} (G), 2^{nd} (G)⟩ N ⟨1^{st} (H), 2^{nd} (H)⟩)$
41	2 40 6 10 37	natcl	$⊢ (φ \land x \in {Base}_{C}) \to S (x) \in (1^{st} (G) (x) Hom (D) 1^{st} (H) (x))$
42	9 10 7 17 22 29 34 38 41	catcocl	$⊢ (φ \land x \in {Base}_{C}) \to S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x) \in (1^{st} (F) (x) Hom (D) 1^{st} (H) (x))$
43	42	ralrimiva	$⊢ φ \to \forall x \in {Base}_{C} S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x) \in (1^{st} (F) (x) Hom (D) 1^{st} (H) (x))$
44		fvex	$⊢ {Base}_{C} \in V$
45		mptelixpg	$⊢ {Base}_{C} \in V \to ((x \in {Base}_{C} ⟼ S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x)) \in \underset{x \in {Base}_{C}}{⨉} (1^{st} (F) (x) Hom (D) 1^{st} (H) (x)) \leftrightarrow \forall x \in {Base}_{C} S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x) \in (1^{st} (F) (x) Hom (D) 1^{st} (H) (x)))$
46	44 45	ax-mp	$⊢ (x \in {Base}_{C} ⟼ S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x)) \in \underset{x \in {Base}_{C}}{⨉} (1^{st} (F) (x) Hom (D) 1^{st} (H) (x)) \leftrightarrow \forall x \in {Base}_{C} S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x) \in (1^{st} (F) (x) Hom (D) 1^{st} (H) (x))$
47	43 46	sylibr	$⊢ φ \to (x \in {Base}_{C} ⟼ S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x)) \in \underset{x \in {Base}_{C}}{⨉} (1^{st} (F) (x) Hom (D) 1^{st} (H) (x))$
48	8 47	eqeltrd	$⊢ φ \to S (⟨F, G⟩ \underset{˙}{∙} H) R \in \underset{x \in {Base}_{C}}{⨉} (1^{st} (F) (x) Hom (D) 1^{st} (H) (x))$
49	16	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to D \in Cat$
50	21	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
51		simpr1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to x \in {Base}_{C}$
52	50 51	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (F) (x) \in {Base}_{D}$
53		simpr2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to y \in {Base}_{C}$
54	50 53	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (F) (y) \in {Base}_{D}$
55	28	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{D}$
56	55 53	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (G) (y) \in {Base}_{D}$
57		eqid	$⊢ Hom (C) = Hom (C)$
58	20	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
59	6 57 10 58 51 53	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (x 2^{nd} (F) y) : x Hom (C) y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)$
60		simpr3	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to f \in (x Hom (C) y)$
61	59 60	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (x 2^{nd} (F) y) (f) \in (1^{st} (F) (x) Hom (D) 1^{st} (F) (y))$
62	35	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to R \in (⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩)$
63	2 62 6 10 53	natcl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to R (y) \in (1^{st} (F) (y) Hom (D) 1^{st} (G) (y))$
64	33	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (H) : {Base}_{C} ⟶ {Base}_{D}$
65	64 53	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (H) (y) \in {Base}_{D}$
66	39	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to S \in (⟨1^{st} (G), 2^{nd} (G)⟩ N ⟨1^{st} (H), 2^{nd} (H)⟩)$
67	2 66 6 10 53	natcl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to S (y) \in (1^{st} (G) (y) Hom (D) 1^{st} (H) (y))$
68	9 10 7 49 52 54 56 61 63 65 67	catass	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (S (y) (⟨1^{st} (F) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (H) (y)) R (y)) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (H) (y)) (x 2^{nd} (F) y) (f) = S (y) (⟨1^{st} (F) (x), 1^{st} (G) (y)⟩ comp (D) 1^{st} (H) (y)) (R (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (G) (y)) (x 2^{nd} (F) y) (f))$
69	2 62 6 57 7 51 53 60	nati	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to R (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (G) (y)) (x 2^{nd} (F) y) (f) = (x 2^{nd} (G) y) (f) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (G) (y)) R (x)$
70	69	oveq2d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to S (y) (⟨1^{st} (F) (x), 1^{st} (G) (y)⟩ comp (D) 1^{st} (H) (y)) (R (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (G) (y)) (x 2^{nd} (F) y) (f)) = S (y) (⟨1^{st} (F) (x), 1^{st} (G) (y)⟩ comp (D) 1^{st} (H) (y)) ((x 2^{nd} (G) y) (f) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (G) (y)) R (x))$
71	55 51	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (G) (x) \in {Base}_{D}$
72	2 62 6 10 51	natcl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to R (x) \in (1^{st} (F) (x) Hom (D) 1^{st} (G) (x))$
73	27	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
74	6 57 10 73 51 53	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (x 2^{nd} (G) y) : x Hom (C) y ⟶ 1^{st} (G) (x) Hom (D) 1^{st} (G) (y)$
75	74 60	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (x 2^{nd} (G) y) (f) \in (1^{st} (G) (x) Hom (D) 1^{st} (G) (y))$
76	9 10 7 49 52 71 56 72 75 65 67	catass	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (S (y) (⟨1^{st} (G) (x), 1^{st} (G) (y)⟩ comp (D) 1^{st} (H) (y)) (x 2^{nd} (G) y) (f)) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (y)) R (x) = S (y) (⟨1^{st} (F) (x), 1^{st} (G) (y)⟩ comp (D) 1^{st} (H) (y)) ((x 2^{nd} (G) y) (f) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (G) (y)) R (x))$
77	2 66 6 57 7 51 53 60	nati	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to S (y) (⟨1^{st} (G) (x), 1^{st} (G) (y)⟩ comp (D) 1^{st} (H) (y)) (x 2^{nd} (G) y) (f) = (x 2^{nd} (H) y) (f) (⟨1^{st} (G) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (H) (y)) S (x)$
78	77	oveq1d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (S (y) (⟨1^{st} (G) (x), 1^{st} (G) (y)⟩ comp (D) 1^{st} (H) (y)) (x 2^{nd} (G) y) (f)) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (y)) R (x) = ((x 2^{nd} (H) y) (f) (⟨1^{st} (G) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (H) (y)) S (x)) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (y)) R (x)$
79	70 76 78	3eqtr2d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to S (y) (⟨1^{st} (F) (x), 1^{st} (G) (y)⟩ comp (D) 1^{st} (H) (y)) (R (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (G) (y)) (x 2^{nd} (F) y) (f)) = ((x 2^{nd} (H) y) (f) (⟨1^{st} (G) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (H) (y)) S (x)) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (y)) R (x)$
80	64 51	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (H) (x) \in {Base}_{D}$
81	2 66 6 10 51	natcl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to S (x) \in (1^{st} (G) (x) Hom (D) 1^{st} (H) (x))$
82	32	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to 1^{st} (H) (C Func D) 2^{nd} (H)$
83	6 57 10 82 51 53	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (x 2^{nd} (H) y) : x Hom (C) y ⟶ 1^{st} (H) (x) Hom (D) 1^{st} (H) (y)$
84	83 60	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (x 2^{nd} (H) y) (f) \in (1^{st} (H) (x) Hom (D) 1^{st} (H) (y))$
85	9 10 7 49 52 71 80 72 81 65 84	catass	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to ((x 2^{nd} (H) y) (f) (⟨1^{st} (G) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (H) (y)) S (x)) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (y)) R (x) = (x 2^{nd} (H) y) (f) (⟨1^{st} (F) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (H) (y)) (S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x))$
86	68 79 85	3eqtrd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (S (y) (⟨1^{st} (F) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (H) (y)) R (y)) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (H) (y)) (x 2^{nd} (F) y) (f) = (x 2^{nd} (H) y) (f) (⟨1^{st} (F) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (H) (y)) (S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x))$
87	4	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to R \in (F N G)$
88	5	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to S \in (G N H)$
89	1 2 6 7 3 87 88 53	fuccoval	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (S (⟨F, G⟩ \underset{˙}{∙} H) R) (y) = S (y) (⟨1^{st} (F) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (H) (y)) R (y)$
90	89	oveq1d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (S (⟨F, G⟩ \underset{˙}{∙} H) R) (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (H) (y)) (x 2^{nd} (F) y) (f) = (S (y) (⟨1^{st} (F) (y), 1^{st} (G) (y)⟩ comp (D) 1^{st} (H) (y)) R (y)) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (H) (y)) (x 2^{nd} (F) y) (f)$
91	1 2 6 7 3 87 88 51	fuccoval	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (S (⟨F, G⟩ \underset{˙}{∙} H) R) (x) = S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x)$
92	91	oveq2d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (x 2^{nd} (H) y) (f) (⟨1^{st} (F) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (H) (y)) (S (⟨F, G⟩ \underset{˙}{∙} H) R) (x) = (x 2^{nd} (H) y) (f) (⟨1^{st} (F) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (H) (y)) (S (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (H) (x)) R (x))$
93	86 90 92	3eqtr4d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land f \in (x Hom (C) y))) \to (S (⟨F, G⟩ \underset{˙}{∙} H) R) (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (H) (y)) (x 2^{nd} (F) y) (f) = (x 2^{nd} (H) y) (f) (⟨1^{st} (F) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (H) (y)) (S (⟨F, G⟩ \underset{˙}{∙} H) R) (x)$
94	93	ralrimivvva	$⊢ φ \to \forall x \in {Base}_{C} \forall y \in {Base}_{C} \forall f \in (x Hom (C) y) (S (⟨F, G⟩ \underset{˙}{∙} H) R) (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (H) (y)) (x 2^{nd} (F) y) (f) = (x 2^{nd} (H) y) (f) (⟨1^{st} (F) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (H) (y)) (S (⟨F, G⟩ \underset{˙}{∙} H) R) (x)$
95	2 6 57 10 7 13 30	isnat2	$⊢ φ \to (S (⟨F, G⟩ \underset{˙}{∙} H) R \in (F N H) \leftrightarrow (S (⟨F, G⟩ \underset{˙}{∙} H) R \in \underset{x \in {Base}_{C}}{⨉} (1^{st} (F) (x) Hom (D) 1^{st} (H) (x)) \land \forall x \in {Base}_{C} \forall y \in {Base}_{C} \forall f \in (x Hom (C) y) (S (⟨F, G⟩ \underset{˙}{∙} H) R) (y) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (H) (y)) (x 2^{nd} (F) y) (f) = (x 2^{nd} (H) y) (f) (⟨1^{st} (F) (x), 1^{st} (H) (x)⟩ comp (D) 1^{st} (H) (y)) (S (⟨F, G⟩ \underset{˙}{∙} H) R) (x)))$
96	48 94 95	mpbir2and	$⊢ φ \to S (⟨F, G⟩ \underset{˙}{∙} H) R \in (F N H)$

Metamath Proof Explorer

Theorem fuccocl

Proof