funcres2b

Description: Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	funcres2b.a	$⊢ A = {Base}_{C}$
	funcres2b.h	$⊢ H = Hom (C)$
	funcres2b.r	$⊢ φ \to R \in Subcat (D)$
	funcres2b.s	$⊢ φ \to R Fn (S \times S)$
	funcres2b.1	$⊢ φ \to F : A ⟶ S$
	funcres2b.2	$⊢ (φ \land (x \in A \land y \in A)) \to (x G y) : Y ⟶ F (x) R F (y)$
Assertion	funcres2b	$⊢ φ \to (F (C Func D) G \leftrightarrow F (C Func (D ↾_{cat} R)) G)$

Proof

Step	Hyp	Ref	Expression
1		funcres2b.a	$⊢ A = {Base}_{C}$
2		funcres2b.h	$⊢ H = Hom (C)$
3		funcres2b.r	$⊢ φ \to R \in Subcat (D)$
4		funcres2b.s	$⊢ φ \to R Fn (S \times S)$
5		funcres2b.1	$⊢ φ \to F : A ⟶ S$
6		funcres2b.2	$⊢ (φ \land (x \in A \land y \in A)) \to (x G y) : Y ⟶ F (x) R F (y)$
7		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
8		funcrcl	$⊢ ⟨F, G⟩ \in (C Func D) \to (C \in Cat \land D \in Cat)$
9	7 8	sylbi	$⊢ F (C Func D) G \to (C \in Cat \land D \in Cat)$
10	9	simpld	$⊢ F (C Func D) G \to C \in Cat$
11	10	a1i	$⊢ φ \to (F (C Func D) G \to C \in Cat)$
12		df-br	$⊢ F (C Func (D ↾_{cat} R)) G \leftrightarrow ⟨F, G⟩ \in (C Func (D ↾_{cat} R))$
13		funcrcl	$⊢ ⟨F, G⟩ \in (C Func (D ↾_{cat} R)) \to (C \in Cat \land D ↾_{cat} R \in Cat)$
14	12 13	sylbi	$⊢ F (C Func (D ↾_{cat} R)) G \to (C \in Cat \land D ↾_{cat} R \in Cat)$
15	14	simpld	$⊢ F (C Func (D ↾_{cat} R)) G \to C \in Cat$
16	15	a1i	$⊢ φ \to (F (C Func (D ↾_{cat} R)) G \to C \in Cat)$
17		eqid	$⊢ {Base}_{D} = {Base}_{D}$
18	3 4 17	subcss1	$⊢ φ \to S \subseteq {Base}_{D}$
19	5 18	fssd	$⊢ φ \to F : A ⟶ {Base}_{D}$
20		eqid	$⊢ D ↾_{cat} R = D ↾_{cat} R$
21		subcrcl	$⊢ R \in Subcat (D) \to D \in Cat$
22	3 21	syl	$⊢ φ \to D \in Cat$
23	20 17 22 4 18	rescbas	$⊢ φ \to S = {Base}_{(D ↾_{cat} R)}$
24	23	feq3d	$⊢ φ \to (F : A ⟶ S \leftrightarrow F : A ⟶ {Base}_{(D ↾_{cat} R)})$
25	5 24	mpbid	$⊢ φ \to F : A ⟶ {Base}_{(D ↾_{cat} R)}$
26	19 25	2thd	$⊢ φ \to (F : A ⟶ {Base}_{D} \leftrightarrow F : A ⟶ {Base}_{(D ↾_{cat} R)})$
27	26	adantr	$⊢ (φ \land C \in Cat) \to (F : A ⟶ {Base}_{D} \leftrightarrow F : A ⟶ {Base}_{(D ↾_{cat} R)})$
28	6	adantlr	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to (x G y) : Y ⟶ F (x) R F (y)$
29	28	frnd	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to ran (x G y) \subseteq F (x) R F (y)$
30	3	ad2antrr	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to R \in Subcat (D)$
31	4	ad2antrr	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to R Fn (S \times S)$
32		eqid	$⊢ Hom (D) = Hom (D)$
33	5	ad2antrr	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to F : A ⟶ S$
34		simprl	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to x \in A$
35	33 34	ffvelrnd	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to F (x) \in S$
36		simprr	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to y \in A$
37	33 36	ffvelrnd	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to F (y) \in S$
38	30 31 32 35 37	subcss2	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to F (x) R F (y) \subseteq F (x) Hom (D) F (y)$
39	29 38	sstrd	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to ran (x G y) \subseteq F (x) Hom (D) F (y)$
40	39 29	2thd	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to (ran (x G y) \subseteq F (x) Hom (D) F (y) \leftrightarrow ran (x G y) \subseteq F (x) R F (y))$
41	40	anbi2d	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to (((x G y) Fn (x H y) \land ran (x G y) \subseteq F (x) Hom (D) F (y)) \leftrightarrow ((x G y) Fn (x H y) \land ran (x G y) \subseteq F (x) R F (y)))$
42		df-f	$⊢ (x G y) : x H y ⟶ F (x) Hom (D) F (y) \leftrightarrow ((x G y) Fn (x H y) \land ran (x G y) \subseteq F (x) Hom (D) F (y))$
43		df-f	$⊢ (x G y) : x H y ⟶ F (x) R F (y) \leftrightarrow ((x G y) Fn (x H y) \land ran (x G y) \subseteq F (x) R F (y))$
44	41 42 43	3bitr4g	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to ((x G y) : x H y ⟶ F (x) Hom (D) F (y) \leftrightarrow (x G y) : x H y ⟶ F (x) R F (y))$
45	20 17 22 4 18	reschom	$⊢ φ \to R = Hom (D ↾_{cat} R)$
46	45	ad2antrr	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to R = Hom (D ↾_{cat} R)$
47	46	oveqd	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to F (x) R F (y) = F (x) Hom (D ↾_{cat} R) F (y)$
48	47	feq3d	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to ((x G y) : x H y ⟶ F (x) R F (y) \leftrightarrow (x G y) : x H y ⟶ F (x) Hom (D ↾_{cat} R) F (y))$
49	44 48	bitrd	$⊢ ((φ \land C \in Cat) \land (x \in A \land y \in A)) \to ((x G y) : x H y ⟶ F (x) Hom (D) F (y) \leftrightarrow (x G y) : x H y ⟶ F (x) Hom (D ↾_{cat} R) F (y))$
50	49	ralrimivva	$⊢ (φ \land C \in Cat) \to \forall x \in A \forall y \in A ((x G y) : x H y ⟶ F (x) Hom (D) F (y) \leftrightarrow (x G y) : x H y ⟶ F (x) Hom (D ↾_{cat} R) F (y))$
51		fveq2	$⊢ z = ⟨x, y⟩ \to G (z) = G (⟨x, y⟩)$
52		df-ov	$⊢ x G y = G (⟨x, y⟩)$
53	51 52	eqtr4di	$⊢ z = ⟨x, y⟩ \to G (z) = x G y$
54		vex	$⊢ x \in V$
55		vex	$⊢ y \in V$
56	54 55	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
57	56	fveq2d	$⊢ z = ⟨x, y⟩ \to F (1^{st} (z)) = F (x)$
58	54 55	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
59	58	fveq2d	$⊢ z = ⟨x, y⟩ \to F (2^{nd} (z)) = F (y)$
60	57 59	oveq12d	$⊢ z = ⟨x, y⟩ \to F (1^{st} (z)) Hom (D) F (2^{nd} (z)) = F (x) Hom (D) F (y)$
61		fveq2	$⊢ z = ⟨x, y⟩ \to H (z) = H (⟨x, y⟩)$
62		df-ov	$⊢ x H y = H (⟨x, y⟩)$
63	61 62	eqtr4di	$⊢ z = ⟨x, y⟩ \to H (z) = x H y$
64	60 63	oveq12d	$⊢ z = ⟨x, y⟩ \to {(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)} = {(F (x) Hom (D) F (y))}^{(x H y)}$
65	53 64	eleq12d	$⊢ z = ⟨x, y⟩ \to (G (z) \in ({(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow x G y \in ({(F (x) Hom (D) F (y))}^{(x H y)}))$
66		ovex	$⊢ F (x) Hom (D) F (y) \in V$
67		ovex	$⊢ x H y \in V$
68	66 67	elmap	$⊢ x G y \in ({(F (x) Hom (D) F (y))}^{(x H y)}) \leftrightarrow (x G y) : x H y ⟶ F (x) Hom (D) F (y)$
69	65 68	bitrdi	$⊢ z = ⟨x, y⟩ \to (G (z) \in ({(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow (x G y) : x H y ⟶ F (x) Hom (D) F (y))$
70	57 59	oveq12d	$⊢ z = ⟨x, y⟩ \to F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)) = F (x) Hom (D ↾_{cat} R) F (y)$
71	70 63	oveq12d	$⊢ z = ⟨x, y⟩ \to {(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)} = {(F (x) Hom (D ↾_{cat} R) F (y))}^{(x H y)}$
72	53 71	eleq12d	$⊢ z = ⟨x, y⟩ \to (G (z) \in ({(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow x G y \in ({(F (x) Hom (D ↾_{cat} R) F (y))}^{(x H y)}))$
73		ovex	$⊢ F (x) Hom (D ↾_{cat} R) F (y) \in V$
74	73 67	elmap	$⊢ x G y \in ({(F (x) Hom (D ↾_{cat} R) F (y))}^{(x H y)}) \leftrightarrow (x G y) : x H y ⟶ F (x) Hom (D ↾_{cat} R) F (y)$
75	72 74	bitrdi	$⊢ z = ⟨x, y⟩ \to (G (z) \in ({(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow (x G y) : x H y ⟶ F (x) Hom (D ↾_{cat} R) F (y))$
76	69 75	bibi12d	$⊢ z = ⟨x, y⟩ \to ((G (z) \in ({(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow G (z) \in ({(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)})) \leftrightarrow ((x G y) : x H y ⟶ F (x) Hom (D) F (y) \leftrightarrow (x G y) : x H y ⟶ F (x) Hom (D ↾_{cat} R) F (y)))$
77	76	ralxp	$⊢ \forall z \in (A \times A) (G (z) \in ({(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow G (z) \in ({(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)})) \leftrightarrow \forall x \in A \forall y \in A ((x G y) : x H y ⟶ F (x) Hom (D) F (y) \leftrightarrow (x G y) : x H y ⟶ F (x) Hom (D ↾_{cat} R) F (y))$
78	50 77	sylibr	$⊢ (φ \land C \in Cat) \to \forall z \in (A \times A) (G (z) \in ({(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow G (z) \in ({(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)}))$
79		ralbi	$⊢ \forall z \in (A \times A) (G (z) \in ({(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow G (z) \in ({(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)})) \to (\forall z \in (A \times A) G (z) \in ({(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow \forall z \in (A \times A) G (z) \in ({(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)}))$
80	78 79	syl	$⊢ (φ \land C \in Cat) \to (\forall z \in (A \times A) G (z) \in ({(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow \forall z \in (A \times A) G (z) \in ({(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)}))$
81	80	3anbi3d	$⊢ (φ \land C \in Cat) \to ((G \in V \land G Fn (A \times A) \land \forall z \in (A \times A) G (z) \in ({(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)})) \leftrightarrow (G \in V \land G Fn (A \times A) \land \forall z \in (A \times A) G (z) \in ({(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)})))$
82		elixp2	$⊢ G \in \underset{z \in A \times A}{⨉} ({(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow (G \in V \land G Fn (A \times A) \land \forall z \in (A \times A) G (z) \in ({(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)}))$
83		elixp2	$⊢ G \in \underset{z \in A \times A}{⨉} ({(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow (G \in V \land G Fn (A \times A) \land \forall z \in (A \times A) G (z) \in ({(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)}))$
84	81 82 83	3bitr4g	$⊢ (φ \land C \in Cat) \to (G \in \underset{z \in A \times A}{⨉} ({(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)}) \leftrightarrow G \in \underset{z \in A \times A}{⨉} ({(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)}))$
85	3	ad2antrr	$⊢ ((φ \land C \in Cat) \land x \in A) \to R \in Subcat (D)$
86	4	ad2antrr	$⊢ ((φ \land C \in Cat) \land x \in A) \to R Fn (S \times S)$
87		eqid	$⊢ Id (D) = Id (D)$
88	5	adantr	$⊢ (φ \land C \in Cat) \to F : A ⟶ S$
89	88	ffvelrnda	$⊢ ((φ \land C \in Cat) \land x \in A) \to F (x) \in S$
90	20 85 86 87 89	subcid	$⊢ ((φ \land C \in Cat) \land x \in A) \to Id (D) (F (x)) = Id (D ↾_{cat} R) (F (x))$
91	90	eqeq2d	$⊢ ((φ \land C \in Cat) \land x \in A) \to ((x G x) (Id (C) (x)) = Id (D) (F (x)) \leftrightarrow (x G x) (Id (C) (x)) = Id (D ↾_{cat} R) (F (x)))$
92		eqid	$⊢ comp (D) = comp (D)$
93	20 17 22 4 18 92	rescco	$⊢ φ \to comp (D) = comp (D ↾_{cat} R)$
94	93	ad2antrr	$⊢ ((φ \land C \in Cat) \land x \in A) \to comp (D) = comp (D ↾_{cat} R)$
95	94	oveqd	$⊢ ((φ \land C \in Cat) \land x \in A) \to ⟨F (x), F (y)⟩ comp (D) F (z) = ⟨F (x), F (y)⟩ comp (D ↾_{cat} R) F (z)$
96	95	oveqd	$⊢ ((φ \land C \in Cat) \land x \in A) \to (y G z) (g) (⟨F (x), F (y)⟩ comp (D) F (z)) (x G y) (f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D ↾_{cat} R) F (z)) (x G y) (f)$
97	96	eqeq2d	$⊢ ((φ \land C \in Cat) \land x \in A) \to ((x G z) (g (⟨x, y⟩ comp (C) z) f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D) F (z)) (x G y) (f) \leftrightarrow (x G z) (g (⟨x, y⟩ comp (C) z) f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D ↾_{cat} R) F (z)) (x G y) (f))$
98	97	2ralbidv	$⊢ ((φ \land C \in Cat) \land x \in A) \to (\forall f \in (x H y) \forall g \in (y H z) (x G z) (g (⟨x, y⟩ comp (C) z) f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D) F (z)) (x G y) (f) \leftrightarrow \forall f \in (x H y) \forall g \in (y H z) (x G z) (g (⟨x, y⟩ comp (C) z) f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D ↾_{cat} R) F (z)) (x G y) (f))$
99	98	2ralbidv	$⊢ ((φ \land C \in Cat) \land x \in A) \to (\forall y \in A \forall z \in A \forall f \in (x H y) \forall g \in (y H z) (x G z) (g (⟨x, y⟩ comp (C) z) f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D) F (z)) (x G y) (f) \leftrightarrow \forall y \in A \forall z \in A \forall f \in (x H y) \forall g \in (y H z) (x G z) (g (⟨x, y⟩ comp (C) z) f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D ↾_{cat} R) F (z)) (x G y) (f))$
100	91 99	anbi12d	$⊢ ((φ \land C \in Cat) \land x \in A) \to (((x G x) (Id (C) (x)) = Id (D) (F (x)) \land \forall y \in A \forall z \in A \forall f \in (x H y) \forall g \in (y H z) (x G z) (g (⟨x, y⟩ comp (C) z) f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D) F (z)) (x G y) (f)) \leftrightarrow ((x G x) (Id (C) (x)) = Id (D ↾_{cat} R) (F (x)) \land \forall y \in A \forall z \in A \forall f \in (x H y) \forall g \in (y H z) (x G z) (g (⟨x, y⟩ comp (C) z) f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D ↾_{cat} R) F (z)) (x G y) (f)))$
101	100	ralbidva	$⊢ (φ \land C \in Cat) \to (\forall x \in A ((x G x) (Id (C) (x)) = Id (D) (F (x)) \land \forall y \in A \forall z \in A \forall f \in (x H y) \forall g \in (y H z) (x G z) (g (⟨x, y⟩ comp (C) z) f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D) F (z)) (x G y) (f)) \leftrightarrow \forall x \in A ((x G x) (Id (C) (x)) = Id (D ↾_{cat} R) (F (x)) \land \forall y \in A \forall z \in A \forall f \in (x H y) \forall g \in (y H z) (x G z) (g (⟨x, y⟩ comp (C) z) f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D ↾_{cat} R) F (z)) (x G y) (f)))$
102	27 84 101	3anbi123d	$⊢ (φ \land C \in Cat) \to ((F : A ⟶ {Base}_{D} \land G \in \underset{z \in A \times A}{⨉} ({(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)}) \land \forall x \in A ((x G x) (Id (C) (x)) = Id (D) (F (x)) \land \forall y \in A \forall z \in A \forall f \in (x H y) \forall g \in (y H z) (x G z) (g (⟨x, y⟩ comp (C) z) f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D) F (z)) (x G y) (f))) \leftrightarrow (F : A ⟶ {Base}_{(D ↾_{cat} R)} \land G \in \underset{z \in A \times A}{⨉} ({(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)}) \land \forall x \in A ((x G x) (Id (C) (x)) = Id (D ↾_{cat} R) (F (x)) \land \forall y \in A \forall z \in A \forall f \in (x H y) \forall g \in (y H z) (x G z) (g (⟨x, y⟩ comp (C) z) f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D ↾_{cat} R) F (z)) (x G y) (f))))$
103		eqid	$⊢ Id (C) = Id (C)$
104		eqid	$⊢ comp (C) = comp (C)$
105		simpr	$⊢ (φ \land C \in Cat) \to C \in Cat$
106	22	adantr	$⊢ (φ \land C \in Cat) \to D \in Cat$
107	1 17 2 32 103 87 104 92 105 106	isfunc	$⊢ (φ \land C \in Cat) \to (F (C Func D) G \leftrightarrow (F : A ⟶ {Base}_{D} \land G \in \underset{z \in A \times A}{⨉} ({(F (1^{st} (z)) Hom (D) F (2^{nd} (z)))}^{H (z)}) \land \forall x \in A ((x G x) (Id (C) (x)) = Id (D) (F (x)) \land \forall y \in A \forall z \in A \forall f \in (x H y) \forall g \in (y H z) (x G z) (g (⟨x, y⟩ comp (C) z) f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D) F (z)) (x G y) (f))))$
108		eqid	$⊢ {Base}_{(D ↾_{cat} R)} = {Base}_{(D ↾_{cat} R)}$
109		eqid	$⊢ Hom (D ↾_{cat} R) = Hom (D ↾_{cat} R)$
110		eqid	$⊢ Id (D ↾_{cat} R) = Id (D ↾_{cat} R)$
111		eqid	$⊢ comp (D ↾_{cat} R) = comp (D ↾_{cat} R)$
112	20 3	subccat	$⊢ φ \to D ↾_{cat} R \in Cat$
113	112	adantr	$⊢ (φ \land C \in Cat) \to D ↾_{cat} R \in Cat$
114	1 108 2 109 103 110 104 111 105 113	isfunc	$⊢ (φ \land C \in Cat) \to (F (C Func (D ↾_{cat} R)) G \leftrightarrow (F : A ⟶ {Base}_{(D ↾_{cat} R)} \land G \in \underset{z \in A \times A}{⨉} ({(F (1^{st} (z)) Hom (D ↾_{cat} R) F (2^{nd} (z)))}^{H (z)}) \land \forall x \in A ((x G x) (Id (C) (x)) = Id (D ↾_{cat} R) (F (x)) \land \forall y \in A \forall z \in A \forall f \in (x H y) \forall g \in (y H z) (x G z) (g (⟨x, y⟩ comp (C) z) f) = (y G z) (g) (⟨F (x), F (y)⟩ comp (D ↾_{cat} R) F (z)) (x G y) (f))))$
115	102 107 114	3bitr4d	$⊢ (φ \land C \in Cat) \to (F (C Func D) G \leftrightarrow F (C Func (D ↾_{cat} R)) G)$
116	115	ex	$⊢ φ \to (C \in Cat \to (F (C Func D) G \leftrightarrow F (C Func (D ↾_{cat} R)) G))$
117	11 16 116	pm5.21ndd	$⊢ φ \to (F (C Func D) G \leftrightarrow F (C Func (D ↾_{cat} R)) G)$

Metamath Proof Explorer

Theorem funcres2b

Proof