iinfssc

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

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

Proof

Step	Hyp	Ref	Expression
1		iinfssc.1	$⊢ φ \to A \neq \emptyset$
2		iinfssc.2	$⊢ (φ \land x \in A) \to H \subseteq_{cat} J$
3		iinfssc.3	$⊢ φ \to K = (y \in ⋂_{x \in A} dom H ⟼ ⋂_{x \in A} H (y))$
4		eqidd	$⊢ (φ \land x \in A) \to dom dom H = dom dom H$
5	2 4	sscfn1	$⊢ (φ \land x \in A) \to H Fn (dom dom H \times dom dom H)$
6		eqidd	$⊢ (φ \land x \in A) \to dom dom J = dom dom J$
7	2 6	sscfn2	$⊢ (φ \land x \in A) \to J Fn (dom dom J \times dom dom J)$
8	5 7 2	ssc1	$⊢ (φ \land x \in A) \to dom dom H \subseteq dom dom J$
9	8	ralrimiva	$⊢ φ \to \forall x \in A dom dom H \subseteq dom dom J$
10		r19.2z	$⊢ (A \neq \emptyset \land \forall x \in A dom dom H \subseteq dom dom J) \to \exists x \in A dom dom H \subseteq dom dom J$
11	1 9 10	syl2anc	$⊢ φ \to \exists x \in A dom dom H \subseteq dom dom J$
12		iinss	$⊢ \exists x \in A dom dom H \subseteq dom dom J \to ⋂_{x \in A} dom dom H \subseteq dom dom J$
13	11 12	syl	$⊢ φ \to ⋂_{x \in A} dom dom H \subseteq dom dom J$
14		nfv	$⊢ Ⅎ x φ$
15	1 2 3 4 14	iinfssclem1	$⊢ φ \to K = (z \in ⋂_{x \in A} dom dom H, w \in ⋂_{x \in A} dom dom H ⟼ ⋂_{x \in A} (z H w))$
16		ovex	$⊢ z H w \in V$
17	16	rgenw	$⊢ \forall x \in A z H w \in V$
18		iinexg	$⊢ (A \neq \emptyset \land \forall x \in A z H w \in V) \to ⋂_{x \in A} (z H w) \in V$
19	1 17 18	sylancl	$⊢ φ \to ⋂_{x \in A} (z H w) \in V$
20	19	adantr	$⊢ (φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \to ⋂_{x \in A} (z H w) \in V$
21	15 20	ovmpt4d	$⊢ (φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \to z K w = ⋂_{x \in A} (z H w)$
22	1	adantr	$⊢ (φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \to A \neq \emptyset$
23		nfii1	$⊢ \underline{Ⅎ} x ⋂_{x \in A} dom dom H$
24	23	nfcri	$⊢ Ⅎ x z \in ⋂_{x \in A} dom dom H$
25	23	nfcri	$⊢ Ⅎ x w \in ⋂_{x \in A} dom dom H$
26	24 25	nfan	$⊢ Ⅎ x (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)$
27	14 26	nfan	$⊢ Ⅎ x (φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H))$
28	5	adantlr	$⊢ ((φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \land x \in A) \to H Fn (dom dom H \times dom dom H)$
29	2	adantlr	$⊢ ((φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \land x \in A) \to H \subseteq_{cat} J$
30		iinss2	$⊢ x \in A \to ⋂_{x \in A} dom dom H \subseteq dom dom H$
31	30	adantl	$⊢ ((φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \land x \in A) \to ⋂_{x \in A} dom dom H \subseteq dom dom H$
32		simplrl	$⊢ ((φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \land x \in A) \to z \in ⋂_{x \in A} dom dom H$
33	31 32	sseldd	$⊢ ((φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \land x \in A) \to z \in dom dom H$
34		simplrr	$⊢ ((φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \land x \in A) \to w \in ⋂_{x \in A} dom dom H$
35	31 34	sseldd	$⊢ ((φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \land x \in A) \to w \in dom dom H$
36	28 29 33 35	ssc2	$⊢ ((φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \land x \in A) \to z H w \subseteq z J w$
37	27 36	ralrimia	$⊢ (φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \to \forall x \in A z H w \subseteq z J w$
38	22 37	jca	$⊢ (φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \to (A \neq \emptyset \land \forall x \in A z H w \subseteq z J w)$
39		r19.2z	$⊢ (A \neq \emptyset \land \forall x \in A z H w \subseteq z J w) \to \exists x \in A z H w \subseteq z J w$
40		iinss	$⊢ \exists x \in A z H w \subseteq z J w \to ⋂_{x \in A} (z H w) \subseteq z J w$
41	38 39 40	3syl	$⊢ (φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \to ⋂_{x \in A} (z H w) \subseteq z J w$
42	21 41	eqsstrd	$⊢ (φ \land (z \in ⋂_{x \in A} dom dom H \land w \in ⋂_{x \in A} dom dom H)) \to z K w \subseteq z J w$
43	42	ralrimivva	$⊢ φ \to \forall z \in ⋂_{x \in A} dom dom H \forall w \in ⋂_{x \in A} dom dom H z K w \subseteq z J w$
44	1 2 3 4 14	iinfssclem2	$⊢ φ \to K Fn (⋂_{x \in A} dom dom H \times ⋂_{x \in A} dom dom H)$
45		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
46	1 45	sylib	$⊢ φ \to \exists x x \in A$
47	46 7	exlimddv	$⊢ φ \to J Fn (dom dom J \times dom dom J)$
48		sscrel	$⊢ Rel \subseteq_{cat}$
49	48	brrelex2i	$⊢ H \subseteq_{cat} J \to J \in V$
50	2 49	syl	$⊢ (φ \land x \in A) \to J \in V$
51	46 50	exlimddv	$⊢ φ \to J \in V$
52	51	dmexd	$⊢ φ \to dom J \in V$
53	52	dmexd	$⊢ φ \to dom dom J \in V$
54	44 47 53	isssc	$⊢ φ \to (K \subseteq_{cat} J \leftrightarrow (⋂_{x \in A} dom dom H \subseteq dom dom J \land \forall z \in ⋂_{x \in A} dom dom H \forall w \in ⋂_{x \in A} dom dom H z K w \subseteq z J w))$
55	13 43 54	mpbir2and	$⊢ φ \to K \subseteq_{cat} J$

Metamath Proof Explorer

Theorem iinfssc

Proof