iinfsubc

Description: Indexed intersection of subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025)

	Ref	Expression
Hypotheses	iinfsubc.1	$⊢ φ \to A \neq \emptyset$
	iinfsubc.2	$⊢ (φ \land x \in A) \to H \in Subcat (C)$
	iinfsubc.3	$⊢ φ \to K = (y \in ⋂_{x \in A} dom H ⟼ ⋂_{x \in A} H (y))$
Assertion	iinfsubc	$⊢ φ \to K \in Subcat (C)$

Proof

Step	Hyp	Ref	Expression
1		iinfsubc.1	$⊢ φ \to A \neq \emptyset$
2		iinfsubc.2	$⊢ (φ \land x \in A) \to H \in Subcat (C)$
3		iinfsubc.3	$⊢ φ \to K = (y \in ⋂_{x \in A} dom H ⟼ ⋂_{x \in A} H (y))$
4		eqid	$⊢ {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
5	2 4	subcssc	$⊢ (φ \land x \in A) \to H \subseteq_{cat} {Hom}_{𝑓} (C)$
6	1 5 3	iinfssc	$⊢ φ \to K \subseteq_{cat} {Hom}_{𝑓} (C)$
7	2	adantr	$⊢ ((φ \land x \in A) \land a \in dom dom H) \to H \in Subcat (C)$
8		eqidd	$⊢ (φ \land x \in A) \to dom dom H = dom dom H$
9	2 8	subcfn	$⊢ (φ \land x \in A) \to H Fn (dom dom H \times dom dom H)$
10	9	adantr	$⊢ ((φ \land x \in A) \land a \in dom dom H) \to H Fn (dom dom H \times dom dom H)$
11		simpr	$⊢ ((φ \land x \in A) \land a \in dom dom H) \to a \in dom dom H$
12		eqid	$⊢ Id (C) = Id (C)$
13	7 10 11 12	subcidcl	$⊢ ((φ \land x \in A) \land a \in dom dom H) \to Id (C) (a) \in (a H a)$
14	13	ex	$⊢ (φ \land x \in A) \to (a \in dom dom H \to Id (C) (a) \in (a H a))$
15	14	ralimdva	$⊢ φ \to (\forall x \in A a \in dom dom H \to \forall x \in A Id (C) (a) \in (a H a))$
16		eliin	$⊢ a \in V \to (a \in ⋂_{x \in A} dom dom H \leftrightarrow \forall x \in A a \in dom dom H)$
17	16	elv	$⊢ a \in ⋂_{x \in A} dom dom H \leftrightarrow \forall x \in A a \in dom dom H$
18		fvex	$⊢ Id (C) (a) \in V$
19		eliin	$⊢ Id (C) (a) \in V \to (Id (C) (a) \in ⋂_{x \in A} (a H a) \leftrightarrow \forall x \in A Id (C) (a) \in (a H a))$
20	18 19	ax-mp	$⊢ Id (C) (a) \in ⋂_{x \in A} (a H a) \leftrightarrow \forall x \in A Id (C) (a) \in (a H a)$
21	15 17 20	3imtr4g	$⊢ φ \to (a \in ⋂_{x \in A} dom dom H \to Id (C) (a) \in ⋂_{x \in A} (a H a))$
22	21	imp	$⊢ (φ \land a \in ⋂_{x \in A} dom dom H) \to Id (C) (a) \in ⋂_{x \in A} (a H a)$
23	1	adantr	$⊢ (φ \land a \in ⋂_{x \in A} dom dom H) \to A \neq \emptyset$
24	5	adantlr	$⊢ ((φ \land a \in ⋂_{x \in A} dom dom H) \land x \in A) \to H \subseteq_{cat} {Hom}_{𝑓} (C)$
25	3	adantr	$⊢ (φ \land a \in ⋂_{x \in A} dom dom H) \to K = (y \in ⋂_{x \in A} dom H ⟼ ⋂_{x \in A} H (y))$
26		eqidd	$⊢ ((φ \land a \in ⋂_{x \in A} dom dom H) \land x \in A) \to dom dom H = dom dom H$
27		nfv	$⊢ Ⅎ x φ$
28		nfii1	$⊢ \underline{Ⅎ} x ⋂_{x \in A} dom dom H$
29	28	nfcri	$⊢ Ⅎ x a \in ⋂_{x \in A} dom dom H$
30	27 29	nfan	$⊢ Ⅎ x (φ \land a \in ⋂_{x \in A} dom dom H)$
31		simpr	$⊢ (φ \land a \in ⋂_{x \in A} dom dom H) \to a \in ⋂_{x \in A} dom dom H$
32	23 24 25 26 30 31 31	iinfssclem3	$⊢ (φ \land a \in ⋂_{x \in A} dom dom H) \to a K a = ⋂_{x \in A} (a H a)$
33	22 32	eleqtrrd	$⊢ (φ \land a \in ⋂_{x \in A} dom dom H) \to Id (C) (a) \in (a K a)$
34		simprl	$⊢ (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in (a K b) \land g \in (b K c))) \to f \in (a K b)$
35	1	ad2antrr	$⊢ ((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \to A \neq \emptyset$
36	24	adantlr	$⊢ (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land x \in A) \to H \subseteq_{cat} {Hom}_{𝑓} (C)$
37	3	ad2antrr	$⊢ ((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \to K = (y \in ⋂_{x \in A} dom H ⟼ ⋂_{x \in A} H (y))$
38		eqidd	$⊢ (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land x \in A) \to dom dom H = dom dom H$
39	28	nfcri	$⊢ Ⅎ x b \in ⋂_{x \in A} dom dom H$
40	28	nfcri	$⊢ Ⅎ x c \in ⋂_{x \in A} dom dom H$
41	39 40	nfan	$⊢ Ⅎ x (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)$
42	30 41	nfan	$⊢ Ⅎ x ((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H))$
43	31	adantr	$⊢ ((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \to a \in ⋂_{x \in A} dom dom H$
44		simprl	$⊢ ((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \to b \in ⋂_{x \in A} dom dom H$
45	35 36 37 38 42 43 44	iinfssclem3	$⊢ ((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \to a K b = ⋂_{x \in A} (a H b)$
46	45	adantr	$⊢ (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in (a K b) \land g \in (b K c))) \to a K b = ⋂_{x \in A} (a H b)$
47	34 46	eleqtrd	$⊢ (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in (a K b) \land g \in (b K c))) \to f \in ⋂_{x \in A} (a H b)$
48		simprr	$⊢ (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in (a K b) \land g \in (b K c))) \to g \in (b K c)$
49		simprr	$⊢ ((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \to c \in ⋂_{x \in A} dom dom H$
50	35 36 37 38 42 44 49	iinfssclem3	$⊢ ((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \to b K c = ⋂_{x \in A} (b H c)$
51	50	adantr	$⊢ (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in (a K b) \land g \in (b K c))) \to b K c = ⋂_{x \in A} (b H c)$
52	48 51	eleqtrd	$⊢ (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in (a K b) \land g \in (b K c))) \to g \in ⋂_{x \in A} (b H c)$
53	47 52	jca	$⊢ (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in (a K b) \land g \in (b K c))) \to (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))$
54		nfii1	$⊢ \underline{Ⅎ} x ⋂_{x \in A} (a H b)$
55	54	nfcri	$⊢ Ⅎ x f \in ⋂_{x \in A} (a H b)$
56		nfii1	$⊢ \underline{Ⅎ} x ⋂_{x \in A} (b H c)$
57	56	nfcri	$⊢ Ⅎ x g \in ⋂_{x \in A} (b H c)$
58	55 57	nfan	$⊢ Ⅎ x (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))$
59	42 58	nfan	$⊢ Ⅎ x (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c)))$
60	2	ad5ant15	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to H \in Subcat (C)$
61	9	ad5ant15	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to H Fn (dom dom H \times dom dom H)$
62		iinss2	$⊢ x \in A \to ⋂_{x \in A} dom dom H \subseteq dom dom H$
63	62	adantl	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to ⋂_{x \in A} dom dom H \subseteq dom dom H$
64	43	ad2antrr	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to a \in ⋂_{x \in A} dom dom H$
65	63 64	sseldd	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to a \in dom dom H$
66		eqid	$⊢ comp (C) = comp (C)$
67	44	ad2antrr	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to b \in ⋂_{x \in A} dom dom H$
68	63 67	sseldd	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to b \in dom dom H$
69	49	ad2antrr	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to c \in ⋂_{x \in A} dom dom H$
70	63 69	sseldd	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to c \in dom dom H$
71		iinss2	$⊢ x \in A \to ⋂_{x \in A} (a H b) \subseteq a H b$
72	71	adantl	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to ⋂_{x \in A} (a H b) \subseteq a H b$
73		simplrl	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to f \in ⋂_{x \in A} (a H b)$
74	72 73	sseldd	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to f \in (a H b)$
75		iinss2	$⊢ x \in A \to ⋂_{x \in A} (b H c) \subseteq b H c$
76	75	adantl	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to ⋂_{x \in A} (b H c) \subseteq b H c$
77		simplrr	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to g \in ⋂_{x \in A} (b H c)$
78	76 77	sseldd	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to g \in (b H c)$
79	60 61 65 66 68 70 74 78	subccocl	$⊢ ((((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \land x \in A) \to g (⟨a, b⟩ comp (C) c) f \in (a H c)$
80	59 79	ralrimia	$⊢ (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \to \forall x \in A g (⟨a, b⟩ comp (C) c) f \in (a H c)$
81		ovex	$⊢ g (⟨a, b⟩ comp (C) c) f \in V$
82		eliin	$⊢ g (⟨a, b⟩ comp (C) c) f \in V \to (g (⟨a, b⟩ comp (C) c) f \in ⋂_{x \in A} (a H c) \leftrightarrow \forall x \in A g (⟨a, b⟩ comp (C) c) f \in (a H c))$
83	81 82	ax-mp	$⊢ g (⟨a, b⟩ comp (C) c) f \in ⋂_{x \in A} (a H c) \leftrightarrow \forall x \in A g (⟨a, b⟩ comp (C) c) f \in (a H c)$
84	80 83	sylibr	$⊢ (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in ⋂_{x \in A} (a H b) \land g \in ⋂_{x \in A} (b H c))) \to g (⟨a, b⟩ comp (C) c) f \in ⋂_{x \in A} (a H c)$
85	53 84	syldan	$⊢ (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in (a K b) \land g \in (b K c))) \to g (⟨a, b⟩ comp (C) c) f \in ⋂_{x \in A} (a H c)$
86	35 36 37 38 42 43 49	iinfssclem3	$⊢ ((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \to a K c = ⋂_{x \in A} (a H c)$
87	86	adantr	$⊢ (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in (a K b) \land g \in (b K c))) \to a K c = ⋂_{x \in A} (a H c)$
88	85 87	eleqtrrd	$⊢ (((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \land (f \in (a K b) \land g \in (b K c))) \to g (⟨a, b⟩ comp (C) c) f \in (a K c)$
89	88	ralrimivva	$⊢ ((φ \land a \in ⋂_{x \in A} dom dom H) \land (b \in ⋂_{x \in A} dom dom H \land c \in ⋂_{x \in A} dom dom H)) \to \forall f \in (a K b) \forall g \in (b K c) g (⟨a, b⟩ comp (C) c) f \in (a K c)$
90	89	ralrimivva	$⊢ (φ \land a \in ⋂_{x \in A} dom dom H) \to \forall b \in ⋂_{x \in A} dom dom H \forall c \in ⋂_{x \in A} dom dom H \forall f \in (a K b) \forall g \in (b K c) g (⟨a, b⟩ comp (C) c) f \in (a K c)$
91	33 90	jca	$⊢ (φ \land a \in ⋂_{x \in A} dom dom H) \to (Id (C) (a) \in (a K a) \land \forall b \in ⋂_{x \in A} dom dom H \forall c \in ⋂_{x \in A} dom dom H \forall f \in (a K b) \forall g \in (b K c) g (⟨a, b⟩ comp (C) c) f \in (a K c))$
92	91	ralrimiva	$⊢ φ \to \forall a \in ⋂_{x \in A} dom dom H (Id (C) (a) \in (a K a) \land \forall b \in ⋂_{x \in A} dom dom H \forall c \in ⋂_{x \in A} dom dom H \forall f \in (a K b) \forall g \in (b K c) g (⟨a, b⟩ comp (C) c) f \in (a K c))$
93		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
94	1 93	sylib	$⊢ φ \to \exists x x \in A$
95		subcrcl	$⊢ H \in Subcat (C) \to C \in Cat$
96	2 95	syl	$⊢ (φ \land x \in A) \to C \in Cat$
97	94 96	exlimddv	$⊢ φ \to C \in Cat$
98	1 5 3 8 27	iinfssclem2	$⊢ φ \to K Fn (⋂_{x \in A} dom dom H \times ⋂_{x \in A} dom dom H)$
99	4 12 66 97 98	issubc2	$⊢ φ \to (K \in Subcat (C) \leftrightarrow (K \subseteq_{cat} {Hom}_{𝑓} (C) \land \forall a \in ⋂_{x \in A} dom dom H (Id (C) (a) \in (a K a) \land \forall b \in ⋂_{x \in A} dom dom H \forall c \in ⋂_{x \in A} dom dom H \forall f \in (a K b) \forall g \in (b K c) g (⟨a, b⟩ comp (C) c) f \in (a K c))))$
100	6 92 99	mpbir2and	$⊢ φ \to K \in Subcat (C)$

Metamath Proof Explorer

Theorem iinfsubc

Proof