funcres

Description: A functor restricted to a subcategory is a functor. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	funcres.f	$⊢ φ \to F \in (C Func D)$
	funcres.h	$⊢ φ \to H \in Subcat (C)$
Assertion	funcres	$⊢ φ \to F ↾_{f} H \in ((C ↾_{cat} H) Func D)$

Proof

Step	Hyp	Ref	Expression
1		funcres.f	$⊢ φ \to F \in (C Func D)$
2		funcres.h	$⊢ φ \to H \in Subcat (C)$
3	1 2	resfval	$⊢ φ \to F ↾_{f} H = ⟨{1^{st} (F) ↾}_{dom dom H}, (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})⟩$
4	3	fveq2d	$⊢ φ \to 2^{nd} (F ↾_{f} H) = 2^{nd} (⟨{1^{st} (F) ↾}_{dom dom H}, (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})⟩)$
5		fvex	$⊢ 1^{st} (F) \in V$
6	5	resex	$⊢ {1^{st} (F) ↾}_{dom dom H} \in V$
7		dmexg	$⊢ H \in Subcat (C) \to dom H \in V$
8		mptexg	$⊢ dom H \in V \to (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)}) \in V$
9	2 7 8	3syl	$⊢ φ \to (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)}) \in V$
10		op2ndg	$⊢ ({1^{st} (F) ↾}_{dom dom H} \in V \land (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)}) \in V) \to 2^{nd} (⟨{1^{st} (F) ↾}_{dom dom H}, (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})⟩) = (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})$
11	6 9 10	sylancr	$⊢ φ \to 2^{nd} (⟨{1^{st} (F) ↾}_{dom dom H}, (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})⟩) = (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})$
12	4 11	eqtrd	$⊢ φ \to 2^{nd} (F ↾_{f} H) = (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})$
13	12	opeq2d	$⊢ φ \to ⟨{1^{st} (F) ↾}_{dom dom H}, 2^{nd} (F ↾_{f} H)⟩ = ⟨{1^{st} (F) ↾}_{dom dom H}, (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})⟩$
14	3 13	eqtr4d	$⊢ φ \to F ↾_{f} H = ⟨{1^{st} (F) ↾}_{dom dom H}, 2^{nd} (F ↾_{f} H)⟩$
15		eqid	$⊢ {Base}_{(C ↾_{cat} H)} = {Base}_{(C ↾_{cat} H)}$
16		eqid	$⊢ {Base}_{D} = {Base}_{D}$
17		eqid	$⊢ Hom (C ↾_{cat} H) = Hom (C ↾_{cat} H)$
18		eqid	$⊢ Hom (D) = Hom (D)$
19		eqid	$⊢ Id (C ↾_{cat} H) = Id (C ↾_{cat} H)$
20		eqid	$⊢ Id (D) = Id (D)$
21		eqid	$⊢ comp (C ↾_{cat} H) = comp (C ↾_{cat} H)$
22		eqid	$⊢ comp (D) = comp (D)$
23		eqid	$⊢ C ↾_{cat} H = C ↾_{cat} H$
24	23 2	subccat	$⊢ φ \to C ↾_{cat} H \in Cat$
25		funcrcl	$⊢ F \in (C Func D) \to (C \in Cat \land D \in Cat)$
26	1 25	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
27	26	simprd	$⊢ φ \to D \in Cat$
28		eqid	$⊢ {Base}_{C} = {Base}_{C}$
29		relfunc	$⊢ Rel (C Func D)$
30		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
31	29 1 30	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
32	28 16 31	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
33		eqidd	$⊢ φ \to dom dom H = dom dom H$
34	2 33	subcfn	$⊢ φ \to H Fn (dom dom H \times dom dom H)$
35	2 34 28	subcss1	$⊢ φ \to dom dom H \subseteq {Base}_{C}$
36	32 35	fssresd	$⊢ φ \to ({1^{st} (F) ↾}_{dom dom H}) : dom dom H ⟶ {Base}_{D}$
37	26	simpld	$⊢ φ \to C \in Cat$
38	23 28 37 34 35	rescbas	$⊢ φ \to dom dom H = {Base}_{(C ↾_{cat} H)}$
39	38	feq2d	$⊢ φ \to (({1^{st} (F) ↾}_{dom dom H}) : dom dom H ⟶ {Base}_{D} \leftrightarrow ({1^{st} (F) ↾}_{dom dom H}) : {Base}_{(C ↾_{cat} H)} ⟶ {Base}_{D})$
40	36 39	mpbid	$⊢ φ \to ({1^{st} (F) ↾}_{dom dom H}) : {Base}_{(C ↾_{cat} H)} ⟶ {Base}_{D}$
41		fvex	$⊢ 2^{nd} (F) (z) \in V$
42	41	resex	$⊢ {2^{nd} (F) (z) ↾}_{H (z)} \in V$
43		eqid	$⊢ (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)}) = (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)})$
44	42 43	fnmpti	$⊢ (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)}) Fn dom H$
45	12	eqcomd	$⊢ φ \to (z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)}) = 2^{nd} (F ↾_{f} H)$
46		fndm	$⊢ H Fn (dom dom H \times dom dom H) \to dom H = dom dom H \times dom dom H$
47	34 46	syl	$⊢ φ \to dom H = dom dom H \times dom dom H$
48	38	sqxpeqd	$⊢ φ \to dom dom H \times dom dom H = {Base}_{(C ↾_{cat} H)} \times {Base}_{(C ↾_{cat} H)}$
49	47 48	eqtrd	$⊢ φ \to dom H = {Base}_{(C ↾_{cat} H)} \times {Base}_{(C ↾_{cat} H)}$
50	45 49	fneq12d	$⊢ φ \to ((z \in dom H ⟼ {2^{nd} (F) (z) ↾}_{H (z)}) Fn dom H \leftrightarrow 2^{nd} (F ↾_{f} H) Fn ({Base}_{(C ↾_{cat} H)} \times {Base}_{(C ↾_{cat} H)}))$
51	44 50	mpbii	$⊢ φ \to 2^{nd} (F ↾_{f} H) Fn ({Base}_{(C ↾_{cat} H)} \times {Base}_{(C ↾_{cat} H)})$
52		eqid	$⊢ Hom (C) = Hom (C)$
53	31	adantr	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
54	35	adantr	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to dom dom H \subseteq {Base}_{C}$
55		simprl	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to x \in {Base}_{(C ↾_{cat} H)}$
56	38	adantr	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to dom dom H = {Base}_{(C ↾_{cat} H)}$
57	55 56	eleqtrrd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to x \in dom dom H$
58	54 57	sseldd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to x \in {Base}_{C}$
59		simprr	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to y \in {Base}_{(C ↾_{cat} H)}$
60	59 56	eleqtrrd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to y \in dom dom H$
61	54 60	sseldd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to y \in {Base}_{C}$
62	28 52 18 53 58 61	funcf2	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to (x 2^{nd} (F) y) : x Hom (C) y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)$
63	2	adantr	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to H \in Subcat (C)$
64	34	adantr	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to H Fn (dom dom H \times dom dom H)$
65	63 64 52 57 60	subcss2	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to x H y \subseteq x Hom (C) y$
66	62 65	fssresd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to ({(x 2^{nd} (F) y) ↾}_{(x H y)}) : x H y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)$
67	1	adantr	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to F \in (C Func D)$
68	67 63 64 57 60	resf2nd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to x 2^{nd} (F ↾_{f} H) y = {(x 2^{nd} (F) y) ↾}_{(x H y)}$
69	68	feq1d	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to ((x 2^{nd} (F ↾_{f} H) y) : x H y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y) \leftrightarrow ({(x 2^{nd} (F) y) ↾}_{(x H y)}) : x H y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y))$
70	66 69	mpbird	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to (x 2^{nd} (F ↾_{f} H) y) : x H y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)$
71	23 28 37 34 35	reschom	$⊢ φ \to H = Hom (C ↾_{cat} H)$
72	71	adantr	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to H = Hom (C ↾_{cat} H)$
73	72	oveqd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to x H y = x Hom (C ↾_{cat} H) y$
74	57	fvresd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to ({1^{st} (F) ↾}_{dom dom H}) (x) = 1^{st} (F) (x)$
75	60	fvresd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to ({1^{st} (F) ↾}_{dom dom H}) (y) = 1^{st} (F) (y)$
76	74 75	oveq12d	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to ({1^{st} (F) ↾}_{dom dom H}) (x) Hom (D) ({1^{st} (F) ↾}_{dom dom H}) (y) = 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)$
77	76	eqcomd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to 1^{st} (F) (x) Hom (D) 1^{st} (F) (y) = ({1^{st} (F) ↾}_{dom dom H}) (x) Hom (D) ({1^{st} (F) ↾}_{dom dom H}) (y)$
78	73 77	feq23d	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to ((x 2^{nd} (F ↾_{f} H) y) : x H y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y) \leftrightarrow (x 2^{nd} (F ↾_{f} H) y) : x Hom (C ↾_{cat} H) y ⟶ ({1^{st} (F) ↾}_{dom dom H}) (x) Hom (D) ({1^{st} (F) ↾}_{dom dom H}) (y))$
79	70 78	mpbid	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)})) \to (x 2^{nd} (F ↾_{f} H) y) : x Hom (C ↾_{cat} H) y ⟶ ({1^{st} (F) ↾}_{dom dom H}) (x) Hom (D) ({1^{st} (F) ↾}_{dom dom H}) (y)$
80	1	adantr	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to F \in (C Func D)$
81	2	adantr	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to H \in Subcat (C)$
82	34	adantr	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to H Fn (dom dom H \times dom dom H)$
83	38	eleq2d	$⊢ φ \to (x \in dom dom H \leftrightarrow x \in {Base}_{(C ↾_{cat} H)})$
84	83	biimpar	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to x \in dom dom H$
85	80 81 82 84 84	resf2nd	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to x 2^{nd} (F ↾_{f} H) x = {(x 2^{nd} (F) x) ↾}_{(x H x)}$
86		eqid	$⊢ Id (C) = Id (C)$
87	23 81 82 86 84	subcid	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to Id (C) (x) = Id (C ↾_{cat} H) (x)$
88	87	eqcomd	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to Id (C ↾_{cat} H) (x) = Id (C) (x)$
89	85 88	fveq12d	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to (x 2^{nd} (F ↾_{f} H) x) (Id (C ↾_{cat} H) (x)) = ({(x 2^{nd} (F) x) ↾}_{(x H x)}) (Id (C) (x))$
90	31	adantr	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
91	38 35	eqsstrrd	$⊢ φ \to {Base}_{(C ↾_{cat} H)} \subseteq {Base}_{C}$
92	91	sselda	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to x \in {Base}_{C}$
93	28 86 20 90 92	funcid	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to (x 2^{nd} (F) x) (Id (C) (x)) = Id (D) (1^{st} (F) (x))$
94	81 82 84 86	subcidcl	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to Id (C) (x) \in (x H x)$
95	94	fvresd	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to ({(x 2^{nd} (F) x) ↾}_{(x H x)}) (Id (C) (x)) = (x 2^{nd} (F) x) (Id (C) (x))$
96	84	fvresd	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to ({1^{st} (F) ↾}_{dom dom H}) (x) = 1^{st} (F) (x)$
97	96	fveq2d	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to Id (D) (({1^{st} (F) ↾}_{dom dom H}) (x)) = Id (D) (1^{st} (F) (x))$
98	93 95 97	3eqtr4d	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to ({(x 2^{nd} (F) x) ↾}_{(x H x)}) (Id (C) (x)) = Id (D) (({1^{st} (F) ↾}_{dom dom H}) (x))$
99	89 98	eqtrd	$⊢ (φ \land x \in {Base}_{(C ↾_{cat} H)}) \to (x 2^{nd} (F ↾_{f} H) x) (Id (C ↾_{cat} H) (x)) = Id (D) (({1^{st} (F) ↾}_{dom dom H}) (x))$
100	2	3ad2ant1	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to H \in Subcat (C)$
101	34	3ad2ant1	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to H Fn (dom dom H \times dom dom H)$
102		simp21	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to x \in {Base}_{(C ↾_{cat} H)}$
103	38	3ad2ant1	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to dom dom H = {Base}_{(C ↾_{cat} H)}$
104	102 103	eleqtrrd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to x \in dom dom H$
105		eqid	$⊢ comp (C) = comp (C)$
106		simp22	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to y \in {Base}_{(C ↾_{cat} H)}$
107	106 103	eleqtrrd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to y \in dom dom H$
108		simp23	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to z \in {Base}_{(C ↾_{cat} H)}$
109	108 103	eleqtrrd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to z \in dom dom H$
110		simp3l	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to f \in (x Hom (C ↾_{cat} H) y)$
111	71	3ad2ant1	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to H = Hom (C ↾_{cat} H)$
112	111	oveqd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to x H y = x Hom (C ↾_{cat} H) y$
113	110 112	eleqtrrd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to f \in (x H y)$
114		simp3r	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to g \in (y Hom (C ↾_{cat} H) z)$
115	111	oveqd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to y H z = y Hom (C ↾_{cat} H) z$
116	114 115	eleqtrrd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to g \in (y H z)$
117	100 101 104 105 107 109 113 116	subccocl	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to g (⟨x, y⟩ comp (C) z) f \in (x H z)$
118	117	fvresd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to ({(x 2^{nd} (F) z) ↾}_{(x H z)}) (g (⟨x, y⟩ comp (C) z) f) = (x 2^{nd} (F) z) (g (⟨x, y⟩ comp (C) z) f)$
119	31	3ad2ant1	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
120	35	3ad2ant1	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to dom dom H \subseteq {Base}_{C}$
121	120 104	sseldd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to x \in {Base}_{C}$
122	120 107	sseldd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to y \in {Base}_{C}$
123	120 109	sseldd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to z \in {Base}_{C}$
124	100 101 52 104 107	subcss2	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to x H y \subseteq x Hom (C) y$
125	124 113	sseldd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to f \in (x Hom (C) y)$
126	100 101 52 107 109	subcss2	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to y H z \subseteq y Hom (C) z$
127	126 116	sseldd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to g \in (y Hom (C) z)$
128	28 52 105 22 119 121 122 123 125 127	funcco	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to (x 2^{nd} (F) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (F) z) (g) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (z)) (x 2^{nd} (F) y) (f)$
129	118 128	eqtrd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to ({(x 2^{nd} (F) z) ↾}_{(x H z)}) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (F) z) (g) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (z)) (x 2^{nd} (F) y) (f)$
130	1	3ad2ant1	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to F \in (C Func D)$
131	130 100 101 104 109	resf2nd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to x 2^{nd} (F ↾_{f} H) z = {(x 2^{nd} (F) z) ↾}_{(x H z)}$
132	23 28 37 34 35 105	rescco	$⊢ φ \to comp (C) = comp (C ↾_{cat} H)$
133	132	3ad2ant1	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to comp (C) = comp (C ↾_{cat} H)$
134	133	eqcomd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to comp (C ↾_{cat} H) = comp (C)$
135	134	oveqd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to ⟨x, y⟩ comp (C ↾_{cat} H) z = ⟨x, y⟩ comp (C) z$
136	135	oveqd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to g (⟨x, y⟩ comp (C ↾_{cat} H) z) f = g (⟨x, y⟩ comp (C) z) f$
137	131 136	fveq12d	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to (x 2^{nd} (F ↾_{f} H) z) (g (⟨x, y⟩ comp (C ↾_{cat} H) z) f) = ({(x 2^{nd} (F) z) ↾}_{(x H z)}) (g (⟨x, y⟩ comp (C) z) f)$
138	104	fvresd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to ({1^{st} (F) ↾}_{dom dom H}) (x) = 1^{st} (F) (x)$
139	107	fvresd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to ({1^{st} (F) ↾}_{dom dom H}) (y) = 1^{st} (F) (y)$
140	138 139	opeq12d	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to ⟨({1^{st} (F) ↾}_{dom dom H}) (x), ({1^{st} (F) ↾}_{dom dom H}) (y)⟩ = ⟨1^{st} (F) (x), 1^{st} (F) (y)⟩$
141	109	fvresd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to ({1^{st} (F) ↾}_{dom dom H}) (z) = 1^{st} (F) (z)$
142	140 141	oveq12d	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to ⟨({1^{st} (F) ↾}_{dom dom H}) (x), ({1^{st} (F) ↾}_{dom dom H}) (y)⟩ comp (D) ({1^{st} (F) ↾}_{dom dom H}) (z) = ⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (z)$
143	130 100 101 107 109	resf2nd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to y 2^{nd} (F ↾_{f} H) z = {(y 2^{nd} (F) z) ↾}_{(y H z)}$
144	143	fveq1d	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to (y 2^{nd} (F ↾_{f} H) z) (g) = ({(y 2^{nd} (F) z) ↾}_{(y H z)}) (g)$
145	116	fvresd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to ({(y 2^{nd} (F) z) ↾}_{(y H z)}) (g) = (y 2^{nd} (F) z) (g)$
146	144 145	eqtrd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to (y 2^{nd} (F ↾_{f} H) z) (g) = (y 2^{nd} (F) z) (g)$
147	130 100 101 104 107	resf2nd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to x 2^{nd} (F ↾_{f} H) y = {(x 2^{nd} (F) y) ↾}_{(x H y)}$
148	147	fveq1d	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to (x 2^{nd} (F ↾_{f} H) y) (f) = ({(x 2^{nd} (F) y) ↾}_{(x H y)}) (f)$
149	113	fvresd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to ({(x 2^{nd} (F) y) ↾}_{(x H y)}) (f) = (x 2^{nd} (F) y) (f)$
150	148 149	eqtrd	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to (x 2^{nd} (F ↾_{f} H) y) (f) = (x 2^{nd} (F) y) (f)$
151	142 146 150	oveq123d	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to (y 2^{nd} (F ↾_{f} H) z) (g) (⟨({1^{st} (F) ↾}_{dom dom H}) (x), ({1^{st} (F) ↾}_{dom dom H}) (y)⟩ comp (D) ({1^{st} (F) ↾}_{dom dom H}) (z)) (x 2^{nd} (F ↾_{f} H) y) (f) = (y 2^{nd} (F) z) (g) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (z)) (x 2^{nd} (F) y) (f)$
152	129 137 151	3eqtr4d	$⊢ (φ \land (x \in {Base}_{(C ↾_{cat} H)} \land y \in {Base}_{(C ↾_{cat} H)} \land z \in {Base}_{(C ↾_{cat} H)}) \land (f \in (x Hom (C ↾_{cat} H) y) \land g \in (y Hom (C ↾_{cat} H) z))) \to (x 2^{nd} (F ↾_{f} H) z) (g (⟨x, y⟩ comp (C ↾_{cat} H) z) f) = (y 2^{nd} (F ↾_{f} H) z) (g) (⟨({1^{st} (F) ↾}_{dom dom H}) (x), ({1^{st} (F) ↾}_{dom dom H}) (y)⟩ comp (D) ({1^{st} (F) ↾}_{dom dom H}) (z)) (x 2^{nd} (F ↾_{f} H) y) (f)$
153	15 16 17 18 19 20 21 22 24 27 40 51 79 99 152	isfuncd	$⊢ φ \to ({1^{st} (F) ↾}_{dom dom H}) ((C ↾_{cat} H) Func D) 2^{nd} (F ↾_{f} H)$
154		df-br	$⊢ ({1^{st} (F) ↾}_{dom dom H}) ((C ↾_{cat} H) Func D) 2^{nd} (F ↾_{f} H) \leftrightarrow ⟨{1^{st} (F) ↾}_{dom dom H}, 2^{nd} (F ↾_{f} H)⟩ \in ((C ↾_{cat} H) Func D)$
155	153 154	sylib	$⊢ φ \to ⟨{1^{st} (F) ↾}_{dom dom H}, 2^{nd} (F ↾_{f} H)⟩ \in ((C ↾_{cat} H) Func D)$
156	14 155	eqeltrd	$⊢ φ \to F ↾_{f} H \in ((C ↾_{cat} H) Func D)$

Metamath Proof Explorer

Theorem funcres

Proof