Theorem iinfconstbaslem

Description: Lemma for iinfconstbas . (Contributed by Zhi Wang, 1-Nov-2025)

	Ref	Expression
Hypotheses	discsubc.j	$$⊢J=\left(x\in S,y\in S⟼if\left(x=y,\left\{I\left(x\right)\right\},\varnothing \right)\right)$$
	discsubc.b	$$⊢B={\mathrm{Base}}_C$$
	discsubc.i	$$⊢I=\mathrm{Id}\left(C\right)$$
	discsubc.s	$$⊢\phi \to S\subseteq B$$
	discsubc.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	iinfconstbas.a	$$⊢\phi \to A=\mathrm{Subcat}\left(C\right)\cap \left\{j|jFn\left(S\times S\right)\right\}$$
Assertion	iinfconstbaslem	$$⊢\phi \to J\in A$$

Proof

Step	Hyp	Ref	Expression
1		discsubc.j	$$⊢J=\left(x\in S,y\in S⟼if\left(x=y,\left\{I\left(x\right)\right\},\varnothing \right)\right)$$
2		discsubc.b	$$⊢B={\mathrm{Base}}_C$$
3		discsubc.i	$$⊢I=\mathrm{Id}\left(C\right)$$
4		discsubc.s	$$⊢\phi \to S\subseteq B$$
5		discsubc.c	$$⊢\phi \to C\in \mathrm{Cat}$$
6		iinfconstbas.a	$$⊢\phi \to A=\mathrm{Subcat}\left(C\right)\cap \left\{j|jFn\left(S\times S\right)\right\}$$
7	1 2 3 4 5	discsubc	$$⊢\phi \to J\in \mathrm{Subcat}\left(C\right)$$
8	1	discsubclem	$$⊢JFn\left(S\times S\right)$$
9	8	a1i	$$⊢\phi \to JFn\left(S\times S\right)$$
10		fneq1	$$⊢j=J\to \left(jFn\left(S\times S\right)\leftrightarrow JFn\left(S\times S\right)\right)$$
11	7 9 10	elabd	$$⊢\phi \to J\in \left\{j|jFn\left(S\times S\right)\right\}$$
12	7 11	elind	$$⊢\phi \to J\in \left(\mathrm{Subcat}\left(C\right)\cap \left\{j|jFn\left(S\times S\right)\right\}\right)$$
13	12 6	eleqtrrd	$$⊢\phi \to J\in A$$