iinfconstbas

Description: The discrete category is the indexed intersection of all subcategories with the same base. (Contributed by Zhi Wang, 1-Nov-2025)

	Ref	Expression
Hypotheses	discsubc.j	$⊢ J = (x \in S, y \in S ⟼ if (x = y, \{I (x)\}, \emptyset))$
	discsubc.b	$⊢ B = {Base}_{C}$
	discsubc.i	$⊢ I = Id (C)$
	discsubc.s	$⊢ φ \to S \subseteq B$
	discsubc.c	$⊢ φ \to C \in Cat$
	iinfconstbas.a	$⊢ φ \to A = Subcat (C) \cap \{j \| j Fn (S \times S)\}$
Assertion	iinfconstbas	$⊢ φ \to J = (z \in ⋂_{h \in A} dom h ⟼ ⋂_{h \in A} h (z))$

Proof

Step	Hyp	Ref	Expression
1		discsubc.j	$⊢ J = (x \in S, y \in S ⟼ if (x = y, \{I (x)\}, \emptyset))$
2		discsubc.b	$⊢ B = {Base}_{C}$
3		discsubc.i	$⊢ I = Id (C)$
4		discsubc.s	$⊢ φ \to S \subseteq B$
5		discsubc.c	$⊢ φ \to C \in Cat$
6		iinfconstbas.a	$⊢ φ \to A = Subcat (C) \cap \{j \| j Fn (S \times S)\}$
7	1 2 3 4 5 6	iinfconstbaslem	$⊢ φ \to J \in A$
8	7	ne0d	$⊢ φ \to A \neq \emptyset$
9		iinconst	$⊢ A \neq \emptyset \to ⋂_{h \in A} S = S$
10	8 9	syl	$⊢ φ \to ⋂_{h \in A} S = S$
11	10	eqcomd	$⊢ φ \to S = ⋂_{h \in A} S$
12	11	adantr	$⊢ (φ \land x \in S) \to S = ⋂_{h \in A} S$
13	7	adantr	$⊢ (φ \land (x \in S \land y \in S)) \to J \in A$
14		simpr	$⊢ ((φ \land (x \in S \land y \in S)) \land h = J) \to h = J$
15	14	oveqd	$⊢ ((φ \land (x \in S \land y \in S)) \land h = J) \to x h y = x J y$
16		snex	$⊢ \{I (x)\} \in V$
17		0ex	$⊢ \emptyset \in V$
18	16 17	ifex	$⊢ if (x = y, \{I (x)\}, \emptyset) \in V$
19	1	ovmpt4g	$⊢ (x \in S \land y \in S \land if (x = y, \{I (x)\}, \emptyset) \in V) \to x J y = if (x = y, \{I (x)\}, \emptyset)$
20	18 19	mp3an3	$⊢ (x \in S \land y \in S) \to x J y = if (x = y, \{I (x)\}, \emptyset)$
21	20	ad2antlr	$⊢ ((φ \land (x \in S \land y \in S)) \land h = J) \to x J y = if (x = y, \{I (x)\}, \emptyset)$
22	15 21	eqtrd	$⊢ ((φ \land (x \in S \land y \in S)) \land h = J) \to x h y = if (x = y, \{I (x)\}, \emptyset)$
23		sseq1	$⊢ \{I (x)\} = if (x = y, \{I (x)\}, \emptyset) \to (\{I (x)\} \subseteq x h y \leftrightarrow if (x = y, \{I (x)\}, \emptyset) \subseteq x h y)$
24		sseq1	$⊢ \emptyset = if (x = y, \{I (x)\}, \emptyset) \to (\emptyset \subseteq x h y \leftrightarrow if (x = y, \{I (x)\}, \emptyset) \subseteq x h y)$
25		simpr	$⊢ (φ \land h \in A) \to h \in A$
26	6	adantr	$⊢ (φ \land h \in A) \to A = Subcat (C) \cap \{j \| j Fn (S \times S)\}$
27	25 26	eleqtrd	$⊢ (φ \land h \in A) \to h \in (Subcat (C) \cap \{j \| j Fn (S \times S)\})$
28	27	elin1d	$⊢ (φ \land h \in A) \to h \in Subcat (C)$
29	28	adantlr	$⊢ ((φ \land (x \in S \land y \in S)) \land h \in A) \to h \in Subcat (C)$
30	27	elin2d	$⊢ (φ \land h \in A) \to h \in \{j \| j Fn (S \times S)\}$
31		vex	$⊢ h \in V$
32		fneq1	$⊢ j = h \to (j Fn (S \times S) \leftrightarrow h Fn (S \times S))$
33	31 32	elab	$⊢ h \in \{j \| j Fn (S \times S)\} \leftrightarrow h Fn (S \times S)$
34	30 33	sylib	$⊢ (φ \land h \in A) \to h Fn (S \times S)$
35	34	adantlr	$⊢ ((φ \land (x \in S \land y \in S)) \land h \in A) \to h Fn (S \times S)$
36		simplrl	$⊢ ((φ \land (x \in S \land y \in S)) \land h \in A) \to x \in S$
37	29 35 36 3	subcidcl	$⊢ ((φ \land (x \in S \land y \in S)) \land h \in A) \to I (x) \in (x h x)$
38	37	adantr	$⊢ (((φ \land (x \in S \land y \in S)) \land h \in A) \land x = y) \to I (x) \in (x h x)$
39		simpr	$⊢ (((φ \land (x \in S \land y \in S)) \land h \in A) \land x = y) \to x = y$
40	39	oveq2d	$⊢ (((φ \land (x \in S \land y \in S)) \land h \in A) \land x = y) \to x h x = x h y$
41	38 40	eleqtrd	$⊢ (((φ \land (x \in S \land y \in S)) \land h \in A) \land x = y) \to I (x) \in (x h y)$
42	41	snssd	$⊢ (((φ \land (x \in S \land y \in S)) \land h \in A) \land x = y) \to \{I (x)\} \subseteq x h y$
43		0ss	$⊢ \emptyset \subseteq x h y$
44	43	a1i	$⊢ (((φ \land (x \in S \land y \in S)) \land h \in A) \land \neg x = y) \to \emptyset \subseteq x h y$
45	23 24 42 44	ifbothda	$⊢ ((φ \land (x \in S \land y \in S)) \land h \in A) \to if (x = y, \{I (x)\}, \emptyset) \subseteq x h y$
46	13 22 45	iinglb	$⊢ (φ \land (x \in S \land y \in S)) \to ⋂_{h \in A} (x h y) = if (x = y, \{I (x)\}, \emptyset)$
47	46	eqcomd	$⊢ (φ \land (x \in S \land y \in S)) \to if (x = y, \{I (x)\}, \emptyset) = ⋂_{h \in A} (x h y)$
48	11 12 47	mpoeq123dva	$⊢ φ \to (x \in S, y \in S ⟼ if (x = y, \{I (x)\}, \emptyset)) = (x \in ⋂_{h \in A} S, y \in ⋂_{h \in A} S ⟼ ⋂_{h \in A} (x h y))$
49	1 48	eqtrid	$⊢ φ \to J = (x \in ⋂_{h \in A} S, y \in ⋂_{h \in A} S ⟼ ⋂_{h \in A} (x h y))$
50		eqid	$⊢ {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
51	28 50	subcssc	$⊢ (φ \land h \in A) \to h \subseteq_{cat} {Hom}_{𝑓} (C)$
52		eqidd	$⊢ φ \to (z \in ⋂_{h \in A} dom h ⟼ ⋂_{h \in A} h (z)) = (z \in ⋂_{h \in A} dom h ⟼ ⋂_{h \in A} h (z))$
53		dmdm	$⊢ h Fn (S \times S) \to S = dom dom h$
54	34 53	syl	$⊢ (φ \land h \in A) \to S = dom dom h$
55		nfv	$⊢ Ⅎ h φ$
56	8 51 52 54 55	iinfssclem1	$⊢ φ \to (z \in ⋂_{h \in A} dom h ⟼ ⋂_{h \in A} h (z)) = (x \in ⋂_{h \in A} S, y \in ⋂_{h \in A} S ⟼ ⋂_{h \in A} (x h y))$
57	49 56	eqtr4d	$⊢ φ \to J = (z \in ⋂_{h \in A} dom h ⟼ ⋂_{h \in A} h (z))$

Metamath Proof Explorer

Theorem iinfconstbas

Proof