funcres2c

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

	Ref	Expression
Hypotheses	funcres2c.a	$⊢ A = {Base}_{C}$
	funcres2c.e	$⊢ E = D ↾_{𝑠} S$
	funcres2c.d	$⊢ φ \to D \in Cat$
	funcres2c.r	$⊢ φ \to S \in V$
	funcres2c.1	$⊢ φ \to F : A ⟶ S$
Assertion	funcres2c	$⊢ φ \to (F (C Func D) G \leftrightarrow F (C Func E) G)$

Proof

Step	Hyp	Ref	Expression
1		funcres2c.a	$⊢ A = {Base}_{C}$
2		funcres2c.e	$⊢ E = D ↾_{𝑠} S$
3		funcres2c.d	$⊢ φ \to D \in Cat$
4		funcres2c.r	$⊢ φ \to S \in V$
5		funcres2c.1	$⊢ φ \to F : A ⟶ S$
6		orc	$⊢ F (C Func D) G \to (F (C Func D) G \lor F (C Func E) G)$
7	6	a1i	$⊢ φ \to (F (C Func D) G \to (F (C Func D) G \lor F (C Func E) G))$
8		olc	$⊢ F (C Func E) G \to (F (C Func D) G \lor F (C Func E) G)$
9	8	a1i	$⊢ φ \to (F (C Func E) G \to (F (C Func D) G \lor F (C Func E) G))$
10		eqid	$⊢ Hom (C) = Hom (C)$
11		eqid	$⊢ {Base}_{D} = {Base}_{D}$
12		eqid	$⊢ {Hom}_{𝑓} (D) = {Hom}_{𝑓} (D)$
13		inss2	$⊢ S \cap {Base}_{D} \subseteq {Base}_{D}$
14	13	a1i	$⊢ φ \to S \cap {Base}_{D} \subseteq {Base}_{D}$
15	11 12 3 14	fullsubc	$⊢ φ \to {{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))} \in Subcat (D)$
16	15	adantr	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to {{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))} \in Subcat (D)$
17	12 11	homffn	$⊢ {Hom}_{𝑓} (D) Fn ({Base}_{D} \times {Base}_{D})$
18		xpss12	$⊢ (S \cap {Base}_{D} \subseteq {Base}_{D} \land S \cap {Base}_{D} \subseteq {Base}_{D}) \to (S \cap {Base}_{D}) \times (S \cap {Base}_{D}) \subseteq {Base}_{D} \times {Base}_{D}$
19	13 13 18	mp2an	$⊢ (S \cap {Base}_{D}) \times (S \cap {Base}_{D}) \subseteq {Base}_{D} \times {Base}_{D}$
20		fnssres	$⊢ ({Hom}_{𝑓} (D) Fn ({Base}_{D} \times {Base}_{D}) \land (S \cap {Base}_{D}) \times (S \cap {Base}_{D}) \subseteq {Base}_{D} \times {Base}_{D}) \to ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}) Fn ((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))$
21	17 19 20	mp2an	$⊢ ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}) Fn ((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))$
22	21	a1i	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}) Fn ((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))$
23	5	adantr	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to F : A ⟶ S$
24	23	ffnd	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to F Fn A$
25	23	frnd	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to ran F \subseteq S$
26		simpr	$⊢ (φ \land F (C Func D) G) \to F (C Func D) G$
27	1 11 26	funcf1	$⊢ (φ \land F (C Func D) G) \to F : A ⟶ {Base}_{D}$
28	27	frnd	$⊢ (φ \land F (C Func D) G) \to ran F \subseteq {Base}_{D}$
29		eqid	$⊢ {Base}_{E} = {Base}_{E}$
30		simpr	$⊢ (φ \land F (C Func E) G) \to F (C Func E) G$
31	1 29 30	funcf1	$⊢ (φ \land F (C Func E) G) \to F : A ⟶ {Base}_{E}$
32	31	frnd	$⊢ (φ \land F (C Func E) G) \to ran F \subseteq {Base}_{E}$
33	2 11	ressbasss	$⊢ {Base}_{E} \subseteq {Base}_{D}$
34	32 33	sstrdi	$⊢ (φ \land F (C Func E) G) \to ran F \subseteq {Base}_{D}$
35	28 34	jaodan	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to ran F \subseteq {Base}_{D}$
36	25 35	ssind	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to ran F \subseteq S \cap {Base}_{D}$
37		df-f	$⊢ F : A ⟶ S \cap {Base}_{D} \leftrightarrow (F Fn A \land ran F \subseteq S \cap {Base}_{D})$
38	24 36 37	sylanbrc	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to F : A ⟶ S \cap {Base}_{D}$
39		eqid	$⊢ Hom (D) = Hom (D)$
40		simpr	$⊢ ((φ \land (x \in A \land y \in A)) \land F (C Func D) G) \to F (C Func D) G$
41		simplrl	$⊢ ((φ \land (x \in A \land y \in A)) \land F (C Func D) G) \to x \in A$
42		simplrr	$⊢ ((φ \land (x \in A \land y \in A)) \land F (C Func D) G) \to y \in A$
43	1 10 39 40 41 42	funcf2	$⊢ ((φ \land (x \in A \land y \in A)) \land F (C Func D) G) \to (x G y) : x Hom (C) y ⟶ F (x) Hom (D) F (y)$
44		eqid	$⊢ Hom (E) = Hom (E)$
45		simpr	$⊢ ((φ \land (x \in A \land y \in A)) \land F (C Func E) G) \to F (C Func E) G$
46		simplrl	$⊢ ((φ \land (x \in A \land y \in A)) \land F (C Func E) G) \to x \in A$
47		simplrr	$⊢ ((φ \land (x \in A \land y \in A)) \land F (C Func E) G) \to y \in A$
48	1 10 44 45 46 47	funcf2	$⊢ ((φ \land (x \in A \land y \in A)) \land F (C Func E) G) \to (x G y) : x Hom (C) y ⟶ F (x) Hom (E) F (y)$
49	2 39	resshom	$⊢ S \in V \to Hom (D) = Hom (E)$
50	4 49	syl	$⊢ φ \to Hom (D) = Hom (E)$
51	50	ad2antrr	$⊢ ((φ \land (x \in A \land y \in A)) \land F (C Func E) G) \to Hom (D) = Hom (E)$
52	51	oveqd	$⊢ ((φ \land (x \in A \land y \in A)) \land F (C Func E) G) \to F (x) Hom (D) F (y) = F (x) Hom (E) F (y)$
53	52	feq3d	$⊢ ((φ \land (x \in A \land y \in A)) \land F (C Func E) G) \to ((x G y) : x Hom (C) y ⟶ F (x) Hom (D) F (y) \leftrightarrow (x G y) : x Hom (C) y ⟶ F (x) Hom (E) F (y))$
54	48 53	mpbird	$⊢ ((φ \land (x \in A \land y \in A)) \land F (C Func E) G) \to (x G y) : x Hom (C) y ⟶ F (x) Hom (D) F (y)$
55	43 54	jaodan	$⊢ ((φ \land (x \in A \land y \in A)) \land (F (C Func D) G \lor F (C Func E) G)) \to (x G y) : x Hom (C) y ⟶ F (x) Hom (D) F (y)$
56	55	an32s	$⊢ ((φ \land (F (C Func D) G \lor F (C Func E) G)) \land (x \in A \land y \in A)) \to (x G y) : x Hom (C) y ⟶ F (x) Hom (D) F (y)$
57	38	adantr	$⊢ ((φ \land (F (C Func D) G \lor F (C Func E) G)) \land (x \in A \land y \in A)) \to F : A ⟶ S \cap {Base}_{D}$
58		simprl	$⊢ ((φ \land (F (C Func D) G \lor F (C Func E) G)) \land (x \in A \land y \in A)) \to x \in A$
59	57 58	ffvelcdmd	$⊢ ((φ \land (F (C Func D) G \lor F (C Func E) G)) \land (x \in A \land y \in A)) \to F (x) \in (S \cap {Base}_{D})$
60		simprr	$⊢ ((φ \land (F (C Func D) G \lor F (C Func E) G)) \land (x \in A \land y \in A)) \to y \in A$
61	57 60	ffvelcdmd	$⊢ ((φ \land (F (C Func D) G \lor F (C Func E) G)) \land (x \in A \land y \in A)) \to F (y) \in (S \cap {Base}_{D})$
62	59 61	ovresd	$⊢ ((φ \land (F (C Func D) G \lor F (C Func E) G)) \land (x \in A \land y \in A)) \to F (x) ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}) F (y) = F (x) {Hom}_{𝑓} (D) F (y)$
63	59	elin2d	$⊢ ((φ \land (F (C Func D) G \lor F (C Func E) G)) \land (x \in A \land y \in A)) \to F (x) \in {Base}_{D}$
64	61	elin2d	$⊢ ((φ \land (F (C Func D) G \lor F (C Func E) G)) \land (x \in A \land y \in A)) \to F (y) \in {Base}_{D}$
65	12 11 39 63 64	homfval	$⊢ ((φ \land (F (C Func D) G \lor F (C Func E) G)) \land (x \in A \land y \in A)) \to F (x) {Hom}_{𝑓} (D) F (y) = F (x) Hom (D) F (y)$
66	62 65	eqtrd	$⊢ ((φ \land (F (C Func D) G \lor F (C Func E) G)) \land (x \in A \land y \in A)) \to F (x) ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}) F (y) = F (x) Hom (D) F (y)$
67	66	feq3d	$⊢ ((φ \land (F (C Func D) G \lor F (C Func E) G)) \land (x \in A \land y \in A)) \to ((x G y) : x Hom (C) y ⟶ F (x) ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}) F (y) \leftrightarrow (x G y) : x Hom (C) y ⟶ F (x) Hom (D) F (y))$
68	56 67	mpbird	$⊢ ((φ \land (F (C Func D) G \lor F (C Func E) G)) \land (x \in A \land y \in A)) \to (x G y) : x Hom (C) y ⟶ F (x) ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}) F (y)$
69	1 10 16 22 38 68	funcres2b	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to (F (C Func D) G \leftrightarrow F (C Func (D ↾_{cat} ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}))) G)$
70		eqidd	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
71		eqidd	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (C)$
72	11	ressinbas	$⊢ S \in V \to D ↾_{𝑠} S = D ↾_{𝑠} (S \cap {Base}_{D})$
73	4 72	syl	$⊢ φ \to D ↾_{𝑠} S = D ↾_{𝑠} (S \cap {Base}_{D})$
74	2 73	eqtrid	$⊢ φ \to E = D ↾_{𝑠} (S \cap {Base}_{D})$
75	74	fveq2d	$⊢ φ \to {Hom}_{𝑓} (E) = {Hom}_{𝑓} (D ↾_{𝑠} (S \cap {Base}_{D}))$
76		eqid	$⊢ D ↾_{𝑠} (S \cap {Base}_{D}) = D ↾_{𝑠} (S \cap {Base}_{D})$
77		eqid	$⊢ D ↾_{cat} ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}) = D ↾_{cat} ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))})$
78	11 12 3 14 76 77	fullresc	$⊢ φ \to ({Hom}_{𝑓} (D ↾_{𝑠} (S \cap {Base}_{D})) = {Hom}_{𝑓} (D ↾_{cat} ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))})) \land {comp}_{𝑓} (D ↾_{𝑠} (S \cap {Base}_{D})) = {comp}_{𝑓} (D ↾_{cat} ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))})))$
79	78	simpld	$⊢ φ \to {Hom}_{𝑓} (D ↾_{𝑠} (S \cap {Base}_{D})) = {Hom}_{𝑓} (D ↾_{cat} ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}))$
80	75 79	eqtrd	$⊢ φ \to {Hom}_{𝑓} (E) = {Hom}_{𝑓} (D ↾_{cat} ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}))$
81	80	adantr	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to {Hom}_{𝑓} (E) = {Hom}_{𝑓} (D ↾_{cat} ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}))$
82	74	fveq2d	$⊢ φ \to {comp}_{𝑓} (E) = {comp}_{𝑓} (D ↾_{𝑠} (S \cap {Base}_{D}))$
83	78	simprd	$⊢ φ \to {comp}_{𝑓} (D ↾_{𝑠} (S \cap {Base}_{D})) = {comp}_{𝑓} (D ↾_{cat} ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}))$
84	82 83	eqtrd	$⊢ φ \to {comp}_{𝑓} (E) = {comp}_{𝑓} (D ↾_{cat} ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}))$
85	84	adantr	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to {comp}_{𝑓} (E) = {comp}_{𝑓} (D ↾_{cat} ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}))$
86		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
87		funcrcl	$⊢ ⟨F, G⟩ \in (C Func D) \to (C \in Cat \land D \in Cat)$
88	86 87	sylbi	$⊢ F (C Func D) G \to (C \in Cat \land D \in Cat)$
89	88	simpld	$⊢ F (C Func D) G \to C \in Cat$
90		df-br	$⊢ F (C Func E) G \leftrightarrow ⟨F, G⟩ \in (C Func E)$
91		funcrcl	$⊢ ⟨F, G⟩ \in (C Func E) \to (C \in Cat \land E \in Cat)$
92	90 91	sylbi	$⊢ F (C Func E) G \to (C \in Cat \land E \in Cat)$
93	92	simpld	$⊢ F (C Func E) G \to C \in Cat$
94	89 93	jaoi	$⊢ (F (C Func D) G \lor F (C Func E) G) \to C \in Cat$
95	94	elexd	$⊢ (F (C Func D) G \lor F (C Func E) G) \to C \in V$
96	95	adantl	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to C \in V$
97	2	ovexi	$⊢ E \in V$
98	97	a1i	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to E \in V$
99		ovexd	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to D ↾_{cat} ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}) \in V$
100	70 71 81 85 96 96 98 99	funcpropd	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to C Func E = C Func (D ↾_{cat} ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}))$
101	100	breqd	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to (F (C Func E) G \leftrightarrow F (C Func (D ↾_{cat} ({{Hom}_{𝑓} (D) ↾}_{((S \cap {Base}_{D}) \times (S \cap {Base}_{D}))}))) G)$
102	69 101	bitr4d	$⊢ (φ \land (F (C Func D) G \lor F (C Func E) G)) \to (F (C Func D) G \leftrightarrow F (C Func E) G)$
103	102	ex	$⊢ φ \to ((F (C Func D) G \lor F (C Func E) G) \to (F (C Func D) G \leftrightarrow F (C Func E) G))$
104	7 9 103	pm5.21ndd	$⊢ φ \to (F (C Func D) G \leftrightarrow F (C Func E) G)$

Metamath Proof Explorer

Theorem funcres2c

Proof