Theorem iinglb

Description: The indexed intersection is the the greatest lower bound if it exists. (Contributed by Zhi Wang, 1-Nov-2025)

	Ref	Expression
Hypotheses	iunlub.1	$$⊢\phi \to X\in A$$
	iunlub.2	$$⊢\left(\phi \wedge x=X\right)\to B=C$$
	iinglb.3	$$⊢\left(\phi \wedge x\in A\right)\to C\subseteq B$$
Assertion	iinglb	$$⊢\phi \to \bigcap _{x\in A}B=C$$

Proof

Step	Hyp	Ref	Expression
1		iunlub.1	$$⊢\phi \to X\in A$$
2		iunlub.2	$$⊢\left(\phi \wedge x=X\right)\to B=C$$
3		iinglb.3	$$⊢\left(\phi \wedge x\in A\right)\to C\subseteq B$$
4	2	sseq1d	$$⊢\left(\phi \wedge x=X\right)\to \left(B\subseteq C\leftrightarrow C\subseteq C\right)$$
5		ssidd	$$⊢\phi \to C\subseteq C$$
6	1 4 5	rspcedvd	$$⊢\phi \to \exists x\in AB\subseteq C$$
7		iinss	$$⊢\exists x\in AB\subseteq C\to \bigcap _{x\in A}B\subseteq C$$
8	6 7	syl	$$⊢\phi \to \bigcap _{x\in A}B\subseteq C$$
9	3	ralrimiva	$$⊢\phi \to \forall x\in AC\subseteq B$$
10		ssiin	$$⊢C\subseteq \bigcap _{x\in A}B\leftrightarrow \forall x\in AC\subseteq B$$
11	9 10	sylibr	$$⊢\phi \to C\subseteq \bigcap _{x\in A}B$$
12	8 11	eqssd	$$⊢\phi \to \bigcap _{x\in A}B=C$$