imasubc3

Description: An image of a functor injective on objects is a subcategory. Remark 4.2(3) of Adamek p. 48. (Contributed by Zhi Wang, 7-Nov-2025)

	Ref	Expression
Hypotheses	imasubc.s	$⊢ S = F [A]$
	imasubc.h	$⊢ H = Hom (D)$
	imasubc.k	$⊢ K = (x \in S, y \in S ⟼ ⋃_{p \in F^{-1} [\{x\}] \times F^{-1} [\{y\}]} G (p) [H (p)])$
	imassc.f	$⊢ φ \to F (D Func E) G$
	imasubc3.f	$⊢ φ \to Fun F^{-1}$
Assertion	imasubc3	$⊢ φ \to K \in Subcat (E)$

Proof

Step	Hyp	Ref	Expression
1		imasubc.s	$⊢ S = F [A]$
2		imasubc.h	$⊢ H = Hom (D)$
3		imasubc.k	$⊢ K = (x \in S, y \in S ⟼ ⋃_{p \in F^{-1} [\{x\}] \times F^{-1} [\{y\}]} G (p) [H (p)])$
4		imassc.f	$⊢ φ \to F (D Func E) G$
5		imasubc3.f	$⊢ φ \to Fun F^{-1}$
6		eqid	$⊢ {Hom}_{𝑓} (E) = {Hom}_{𝑓} (E)$
7	1 2 3 4 6	imassc	$⊢ φ \to K \subseteq_{cat} {Hom}_{𝑓} (E)$
8	4	adantr	$⊢ (φ \land a \in S) \to F (D Func E) G$
9		eqid	$⊢ Id (E) = Id (E)$
10		simpr	$⊢ (φ \land a \in S) \to a \in S$
11	1 2 3 8 9 10	imaid	$⊢ (φ \land a \in S) \to Id (E) (a) \in (a K a)$
12	4	ad3antrrr	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a K b) \land g \in (b K c))) \to F (D Func E) G$
13		eqid	$⊢ {Base}_{D} = {Base}_{D}$
14		eqid	$⊢ {Base}_{E} = {Base}_{E}$
15		eqid	$⊢ comp (E) = comp (E)$
16	13 14 4	funcf1	$⊢ φ \to F : {Base}_{D} ⟶ {Base}_{E}$
17		df-f1	$⊢ F : {Base}_{D} \underset{1-1}{⟶} {Base}_{E} \leftrightarrow (F : {Base}_{D} ⟶ {Base}_{E} \land Fun F^{-1})$
18	16 5 17	sylanbrc	$⊢ φ \to F : {Base}_{D} \underset{1-1}{⟶} {Base}_{E}$
19	18	ad3antrrr	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a K b) \land g \in (b K c))) \to F : {Base}_{D} \underset{1-1}{⟶} {Base}_{E}$
20		simpllr	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a K b) \land g \in (b K c))) \to a \in S$
21		simplrl	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a K b) \land g \in (b K c))) \to b \in S$
22		simplrr	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a K b) \land g \in (b K c))) \to c \in S$
23		simprl	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a K b) \land g \in (b K c))) \to f \in (a K b)$
24		simprr	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a K b) \land g \in (b K c))) \to g \in (b K c)$
25	1 2 3 12 13 14 15 19 20 21 22 23 24	imaf1co	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a K b) \land g \in (b K c))) \to g (⟨a, b⟩ comp (E) c) f \in (a K c)$
26	25	ralrimivva	$⊢ ((φ \land a \in S) \land (b \in S \land c \in S)) \to \forall f \in (a K b) \forall g \in (b K c) g (⟨a, b⟩ comp (E) c) f \in (a K c)$
27	26	ralrimivva	$⊢ (φ \land a \in S) \to \forall b \in S \forall c \in S \forall f \in (a K b) \forall g \in (b K c) g (⟨a, b⟩ comp (E) c) f \in (a K c)$
28	11 27	jca	$⊢ (φ \land a \in S) \to (Id (E) (a) \in (a K a) \land \forall b \in S \forall c \in S \forall f \in (a K b) \forall g \in (b K c) g (⟨a, b⟩ comp (E) c) f \in (a K c))$
29	28	ralrimiva	$⊢ φ \to \forall a \in S (Id (E) (a) \in (a K a) \land \forall b \in S \forall c \in S \forall f \in (a K b) \forall g \in (b K c) g (⟨a, b⟩ comp (E) c) f \in (a K c))$
30	4	funcrcl3	$⊢ φ \to E \in Cat$
31		relfunc	$⊢ Rel (D Func E)$
32	31	brrelex1i	$⊢ F (D Func E) G \to F \in V$
33	4 32	syl	$⊢ φ \to F \in V$
34	33 33 3	imasubclem2	$⊢ φ \to K Fn (S \times S)$
35	6 9 15 30 34	issubc2	$⊢ φ \to (K \in Subcat (E) \leftrightarrow (K \subseteq_{cat} {Hom}_{𝑓} (E) \land \forall a \in S (Id (E) (a) \in (a K a) \land \forall b \in S \forall c \in S \forall f \in (a K b) \forall g \in (b K c) g (⟨a, b⟩ comp (E) c) f \in (a K c))))$
36	7 29 35	mpbir2and	$⊢ φ \to K \in Subcat (E)$

Metamath Proof Explorer

Theorem imasubc3

Proof